This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zle0orge1

Description: There is no integer in the open unit interval, i.e., an integer is either less than or equal to 0 or greater than or equal to 1 . (Contributed by AV, 4-Jun-2023)

Ref Expression
Assertion zle0orge1 
|- ( Z e. ZZ -> ( Z <_ 0 \/ 1 <_ Z ) )

Proof

Step Hyp Ref Expression
1 elznn 
 |-  ( Z e. ZZ <-> ( Z e. RR /\ ( Z e. NN \/ -u Z e. NN0 ) ) )
2 nnge1 
 |-  ( Z e. NN -> 1 <_ Z )
3 2 a1i 
 |-  ( Z e. RR -> ( Z e. NN -> 1 <_ Z ) )
4 elnn0z 
 |-  ( -u Z e. NN0 <-> ( -u Z e. ZZ /\ 0 <_ -u Z ) )
5 le0neg1 
 |-  ( Z e. RR -> ( Z <_ 0 <-> 0 <_ -u Z ) )
6 5 biimprd 
 |-  ( Z e. RR -> ( 0 <_ -u Z -> Z <_ 0 ) )
7 6 adantld 
 |-  ( Z e. RR -> ( ( -u Z e. ZZ /\ 0 <_ -u Z ) -> Z <_ 0 ) )
8 4 7 biimtrid 
 |-  ( Z e. RR -> ( -u Z e. NN0 -> Z <_ 0 ) )
9 3 8 orim12d 
 |-  ( Z e. RR -> ( ( Z e. NN \/ -u Z e. NN0 ) -> ( 1 <_ Z \/ Z <_ 0 ) ) )
10 9 imp 
 |-  ( ( Z e. RR /\ ( Z e. NN \/ -u Z e. NN0 ) ) -> ( 1 <_ Z \/ Z <_ 0 ) )
11 10 orcomd 
 |-  ( ( Z e. RR /\ ( Z e. NN \/ -u Z e. NN0 ) ) -> ( Z <_ 0 \/ 1 <_ Z ) )
12 1 11 sylbi 
 |-  ( Z e. ZZ -> ( Z <_ 0 \/ 1 <_ Z ) )