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 )