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 ) |
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 ) |