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	⊢ ¬ 𝐵 ∈ ( 𝐴 ..^ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 < 𝐵 )
2		elfzoel2	⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℤ )
3	2	zred	⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℝ )
4	3	ltnrd	⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝐵 < 𝐵 )
5	1 4	pm2.65i	⊢ ¬ 𝐵 ∈ ( 𝐴 ..^ 𝐵 )