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