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\in \mathbb{N}\to B-1\in \left(0..^B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lbfzo0	$$⊢0\in \left(0..^B\right)\leftrightarrow B\in \mathbb{N}$$
2		fzoend	$$⊢0\in \left(0..^B\right)\to B-1\in \left(0..^B\right)$$
3	1 2	sylbir	$$⊢B\in \mathbb{N}\to B-1\in \left(0..^B\right)$$