Theorem eldmgm

Description: Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014)

	Ref	Expression
Assertion	eldmgm	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. A e. ( ZZ \ NN ) ) )
2		eldif	|- ( A e. ( ZZ \ NN ) <-> ( A e. ZZ /\ -. A e. NN ) )
3		elznn	|- ( A e. ZZ <-> ( A e. RR /\ ( A e. NN \/ -u A e. NN0 ) ) )
4	3	simprbi	|- ( A e. ZZ -> ( A e. NN \/ -u A e. NN0 ) )
5	4	orcanai	|- ( ( A e. ZZ /\ -. A e. NN ) -> -u A e. NN0 )
6		negneg	|- ( A e. CC -> -u -u A = A )
7	6	adantr	|- ( ( A e. CC /\ -u A e. NN0 ) -> -u -u A = A )
8		nn0negz	|- ( -u A e. NN0 -> -u -u A e. ZZ )
9	8	adantl	|- ( ( A e. CC /\ -u A e. NN0 ) -> -u -u A e. ZZ )
10	7 9	eqeltrrd	|- ( ( A e. CC /\ -u A e. NN0 ) -> A e. ZZ )
11	10	ex	|- ( A e. CC -> ( -u A e. NN0 -> A e. ZZ ) )
12		nngt0	|- ( A e. NN -> 0 < A )
13		nnre	|- ( A e. NN -> A e. RR )
14	13	lt0neg2d	|- ( A e. NN -> ( 0 < A <-> -u A < 0 ) )
15	12 14	mpbid	|- ( A e. NN -> -u A < 0 )
16	13	renegcld	|- ( A e. NN -> -u A e. RR )
17		0re	|- 0 e. RR
18		ltnle	|- ( ( -u A e. RR /\ 0 e. RR ) -> ( -u A < 0 <-> -. 0 <_ -u A ) )
19	16 17 18	sylancl	|- ( A e. NN -> ( -u A < 0 <-> -. 0 <_ -u A ) )
20	15 19	mpbid	|- ( A e. NN -> -. 0 <_ -u A )
21		nn0ge0	|- ( -u A e. NN0 -> 0 <_ -u A )
22	20 21	nsyl3	|- ( -u A e. NN0 -> -. A e. NN )
23	11 22	jca2	|- ( A e. CC -> ( -u A e. NN0 -> ( A e. ZZ /\ -. A e. NN ) ) )
24	5 23	impbid2	|- ( A e. CC -> ( ( A e. ZZ /\ -. A e. NN ) <-> -u A e. NN0 ) )
25	2 24	bitrid	|- ( A e. CC -> ( A e. ( ZZ \ NN ) <-> -u A e. NN0 ) )
26	25	notbid	|- ( A e. CC -> ( -. A e. ( ZZ \ NN ) <-> -. -u A e. NN0 ) )
27	26	pm5.32i	|- ( ( A e. CC /\ -. A e. ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )
28	1 27	bitri	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )