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	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 − 1 ) ∈ ( 0 ..^ 𝐵 ) )

Proof

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