Theorem fzonel

Description: A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015)

	Ref	Expression
Assertion	fzonel	$$⊢\neg B\in \left(A..^B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	$$⊢B\in \left(A..^B\right)\to B<B$$
2		elfzoel2	$$⊢B\in \left(A..^B\right)\to B\in \mathbb{Z}$$
3	2	zred	$$⊢B\in \left(A..^B\right)\to B\in ℝ$$
4	3	ltnrd	$$⊢B\in \left(A..^B\right)\to \neg B<B$$
5	1 4	pm2.65i	$$⊢\neg B\in \left(A..^B\right)$$