Metamath Proof Explorer


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