Metamath Proof Explorer

Theorem elz2

Description: Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elz2 
|- ( N e. ZZ <-> E. x e. NN E. y e. NN N = ( x - y ) )

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
2 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
3 2 adantl 
 |-  ( ( N e. RR /\ N e. NN0 ) -> ( N + 1 ) e. NN )
4 1nn 
 |-  1 e. NN
5 4 a1i 
 |-  ( ( N e. RR /\ N e. NN0 ) -> 1 e. NN )
6 recn 
 |-  ( N e. RR -> N e. CC )
7 6 adantr 
 |-  ( ( N e. RR /\ N e. NN0 ) -> N e. CC )
8 ax-1cn 
 |-  1 e. CC
9 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
10 7 8 9 sylancl 
 |-  ( ( N e. RR /\ N e. NN0 ) -> ( ( N + 1 ) - 1 ) = N )
11 10 eqcomd 
 |-  ( ( N e. RR /\ N e. NN0 ) -> N = ( ( N + 1 ) - 1 ) )
12 rspceov 
 |-  ( ( ( N + 1 ) e. NN /\ 1 e. NN /\ N = ( ( N + 1 ) - 1 ) ) -> E. x e. NN E. y e. NN N = ( x - y ) )
13 3 5 11 12 syl3anc 
 |-  ( ( N e. RR /\ N e. NN0 ) -> E. x e. NN E. y e. NN N = ( x - y ) )
14 4 a1i 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> 1 e. NN )
15 6 adantr 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> N e. CC )
16 negsub 
 |-  ( ( 1 e. CC /\ N e. CC ) -> ( 1 + -u N ) = ( 1 - N ) )
17 8 15 16 sylancr 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> ( 1 + -u N ) = ( 1 - N ) )
18 simpr 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> -u N e. NN0 )
19 nnnn0addcl 
 |-  ( ( 1 e. NN /\ -u N e. NN0 ) -> ( 1 + -u N ) e. NN )
20 4 18 19 sylancr 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> ( 1 + -u N ) e. NN )
21 17 20 eqeltrrd 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> ( 1 - N ) e. NN )
22 nncan 
 |-  ( ( 1 e. CC /\ N e. CC ) -> ( 1 - ( 1 - N ) ) = N )
23 8 15 22 sylancr 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> ( 1 - ( 1 - N ) ) = N )
24 23 eqcomd 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> N = ( 1 - ( 1 - N ) ) )
25 rspceov 
 |-  ( ( 1 e. NN /\ ( 1 - N ) e. NN /\ N = ( 1 - ( 1 - N ) ) ) -> E. x e. NN E. y e. NN N = ( x - y ) )
26 14 21 24 25 syl3anc 
 |-  ( ( N e. RR /\ -u N e. NN0 ) -> E. x e. NN E. y e. NN N = ( x - y ) )
27 13 26 jaodan 
 |-  ( ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) -> E. x e. NN E. y e. NN N = ( x - y ) )
28 nnre 
 |-  ( x e. NN -> x e. RR )
29 nnre 
 |-  ( y e. NN -> y e. RR )
30 resubcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x - y ) e. RR )
31 28 29 30 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x - y ) e. RR )
32 letric 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y <_ x \/ x <_ y ) )
33 29 28 32 syl2anr 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y <_ x \/ x <_ y ) )
34 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
35 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
36 nn0sub 
 |-  ( ( y e. NN0 /\ x e. NN0 ) -> ( y <_ x <-> ( x - y ) e. NN0 ) )
37 34 35 36 syl2anr 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y <_ x <-> ( x - y ) e. NN0 ) )
38 nn0sub 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x <_ y <-> ( y - x ) e. NN0 ) )
39 35 34 38 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x <_ y <-> ( y - x ) e. NN0 ) )
40 nncn 
 |-  ( x e. NN -> x e. CC )
41 nncn 
 |-  ( y e. NN -> y e. CC )
42 negsubdi2 
 |-  ( ( x e. CC /\ y e. CC ) -> -u ( x - y ) = ( y - x ) )
43 40 41 42 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> -u ( x - y ) = ( y - x ) )
44 43 eleq1d 
 |-  ( ( x e. NN /\ y e. NN ) -> ( -u ( x - y ) e. NN0 <-> ( y - x ) e. NN0 ) )
45 39 44 bitr4d 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x <_ y <-> -u ( x - y ) e. NN0 ) )
46 37 45 orbi12d 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( y <_ x \/ x <_ y ) <-> ( ( x - y ) e. NN0 \/ -u ( x - y ) e. NN0 ) ) )
47 33 46 mpbid 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( x - y ) e. NN0 \/ -u ( x - y ) e. NN0 ) )
48 31 47 jca 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( x - y ) e. RR /\ ( ( x - y ) e. NN0 \/ -u ( x - y ) e. NN0 ) ) )
49 eleq1 
 |-  ( N = ( x - y ) -> ( N e. RR <-> ( x - y ) e. RR ) )
50 eleq1 
 |-  ( N = ( x - y ) -> ( N e. NN0 <-> ( x - y ) e. NN0 ) )
51 negeq 
 |-  ( N = ( x - y ) -> -u N = -u ( x - y ) )
52 51 eleq1d 
 |-  ( N = ( x - y ) -> ( -u N e. NN0 <-> -u ( x - y ) e. NN0 ) )
53 50 52 orbi12d 
 |-  ( N = ( x - y ) -> ( ( N e. NN0 \/ -u N e. NN0 ) <-> ( ( x - y ) e. NN0 \/ -u ( x - y ) e. NN0 ) ) )
54 49 53 anbi12d 
 |-  ( N = ( x - y ) -> ( ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) <-> ( ( x - y ) e. RR /\ ( ( x - y ) e. NN0 \/ -u ( x - y ) e. NN0 ) ) ) )
55 48 54 syl5ibrcom 
 |-  ( ( x e. NN /\ y e. NN ) -> ( N = ( x - y ) -> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) ) )
56 55 rexlimivv 
 |-  ( E. x e. NN E. y e. NN N = ( x - y ) -> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
57 27 56 impbii 
 |-  ( ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) <-> E. x e. NN E. y e. NN N = ( x - y ) )
58 1 57 bitri 
 |-  ( N e. ZZ <-> E. x e. NN E. y e. NN N = ( x - y ) )