Theorem elzdif0

Description: Lemma for qqhval2 . (Contributed by Thierry Arnoux, 29-Oct-2017)

	Ref	Expression
Assertion	elzdif0	|- ( M e. ( ZZ \ { 0 } ) -> ( M e. NN \/ -u M e. NN ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsnneq	|- ( M e. ( ZZ \ { 0 } ) -> -. M = 0 )
2		eldifi	|- ( M e. ( ZZ \ { 0 } ) -> M e. ZZ )
3		elz	|- ( M e. ZZ <-> ( M e. RR /\ ( M = 0 \/ M e. NN \/ -u M e. NN ) ) )
4	2 3	sylib	|- ( M e. ( ZZ \ { 0 } ) -> ( M e. RR /\ ( M = 0 \/ M e. NN \/ -u M e. NN ) ) )
5	4	simprd	|- ( M e. ( ZZ \ { 0 } ) -> ( M = 0 \/ M e. NN \/ -u M e. NN ) )
6		3orass	|- ( ( M = 0 \/ M e. NN \/ -u M e. NN ) <-> ( M = 0 \/ ( M e. NN \/ -u M e. NN ) ) )
7	5 6	sylib	|- ( M e. ( ZZ \ { 0 } ) -> ( M = 0 \/ ( M e. NN \/ -u M e. NN ) ) )
8		orel1	|- ( -. M = 0 -> ( ( M = 0 \/ ( M e. NN \/ -u M e. NN ) ) -> ( M e. NN \/ -u M e. NN ) ) )
9	1 7 8	sylc	|- ( M e. ( ZZ \ { 0 } ) -> ( M e. NN \/ -u M e. NN ) )