Metamath Proof Explorer


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