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
|- -. B e. ( A ..^ B )

Proof

Step Hyp Ref Expression
1 elfzolt2
 |-  ( B e. ( A ..^ B ) -> B < B )
2 elfzoel2
 |-  ( B e. ( A ..^ B ) -> B e. ZZ )
3 2 zred
 |-  ( B e. ( A ..^ B ) -> B e. RR )
4 3 ltnrd
 |-  ( B e. ( A ..^ B ) -> -. B < B )
5 1 4 pm2.65i
 |-  -. B e. ( A ..^ B )