Metamath Proof Explorer

Theorem fzo0end

Description: The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzo0end ⊢ B ∈ ℕ → B − 1 ∈ 0 ..^ B

Proof

Step Hyp Ref Expression
1 lbfzo0 ⊢ 0 ∈ 0 ..^ B ↔ B ∈ ℕ
2 fzoend ⊢ 0 ∈ 0 ..^ B → B − 1 ∈ 0 ..^ B
3 1 2 sylbir ⊢ B ∈ ℕ → B − 1 ∈ 0 ..^ B