Metamath Proof Explorer

Theorem lzenom

Description: Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion lzenom 
|- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ _om )

Proof

Step Hyp Ref Expression
1 zex 
 |-  ZZ e. _V
2 difexg 
 |-  ( ZZ e. _V -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. _V )
3 1 2 mp1i 
 |-  ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. _V )
4 nnex 
 |-  NN e. _V
5 4 a1i 
 |-  ( N e. ZZ -> NN e. _V )
6 ovex 
 |-  ( ( N + 1 ) - a ) e. _V
7 6 2a1i 
 |-  ( N e. ZZ -> ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N + 1 ) - a ) e. _V ) )
8 ovex 
 |-  ( ( N + 1 ) - b ) e. _V
9 8 2a1i 
 |-  ( N e. ZZ -> ( b e. NN -> ( ( N + 1 ) - b ) e. _V ) )
10 simpl 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> N e. ZZ )
11 10 peano2zd 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( N + 1 ) e. ZZ )
12 simprl 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a e. ZZ )
13 11 12 zsubcld 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( ( N + 1 ) - a ) e. ZZ )
14 zre 
 |-  ( a e. ZZ -> a e. RR )
15 14 ad2antrl 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a e. RR )
16 11 zred 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( N + 1 ) e. RR )
17 1red 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> 1 e. RR )
18 simprr 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a <_ N )
19 zcn 
 |-  ( N e. ZZ -> N e. CC )
20 19 adantr 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> N e. CC )
21 ax-1cn 
 |-  1 e. CC
22 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
23 20 21 22 sylancl 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( ( N + 1 ) - 1 ) = N )
24 18 23 breqtrrd 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a <_ ( ( N + 1 ) - 1 ) )
25 15 16 17 24 lesubd 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> 1 <_ ( ( N + 1 ) - a ) )
26 11 zcnd 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( N + 1 ) e. CC )
27 zcn 
 |-  ( a e. ZZ -> a e. CC )
28 27 ad2antrl 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a e. CC )
29 26 28 nncand 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( ( N + 1 ) - ( ( N + 1 ) - a ) ) = a )
30 29 eqcomd 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) )
31 13 25 30 jca31 
 |-  ( ( N e. ZZ /\ ( a e. ZZ /\ a <_ N ) ) -> ( ( ( ( N + 1 ) - a ) e. ZZ /\ 1 <_ ( ( N + 1 ) - a ) ) /\ a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) ) )
32 31 adantrr 
 |-  ( ( N e. ZZ /\ ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) ) -> ( ( ( ( N + 1 ) - a ) e. ZZ /\ 1 <_ ( ( N + 1 ) - a ) ) /\ a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) ) )
33 eleq1 
 |-  ( b = ( ( N + 1 ) - a ) -> ( b e. ZZ <-> ( ( N + 1 ) - a ) e. ZZ ) )
34 breq2 
 |-  ( b = ( ( N + 1 ) - a ) -> ( 1 <_ b <-> 1 <_ ( ( N + 1 ) - a ) ) )
35 33 34 anbi12d 
 |-  ( b = ( ( N + 1 ) - a ) -> ( ( b e. ZZ /\ 1 <_ b ) <-> ( ( ( N + 1 ) - a ) e. ZZ /\ 1 <_ ( ( N + 1 ) - a ) ) ) )
36 oveq2 
 |-  ( b = ( ( N + 1 ) - a ) -> ( ( N + 1 ) - b ) = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) )
37 36 eqeq2d 
 |-  ( b = ( ( N + 1 ) - a ) -> ( a = ( ( N + 1 ) - b ) <-> a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) ) )
38 35 37 anbi12d 
 |-  ( b = ( ( N + 1 ) - a ) -> ( ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) <-> ( ( ( ( N + 1 ) - a ) e. ZZ /\ 1 <_ ( ( N + 1 ) - a ) ) /\ a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) ) ) )
39 38 ad2antll 
 |-  ( ( N e. ZZ /\ ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) ) -> ( ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) <-> ( ( ( ( N + 1 ) - a ) e. ZZ /\ 1 <_ ( ( N + 1 ) - a ) ) /\ a = ( ( N + 1 ) - ( ( N + 1 ) - a ) ) ) ) )
40 32 39 mpbird 
 |-  ( ( N e. ZZ /\ ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) ) -> ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) )
41 simpl 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> N e. ZZ )
42 41 peano2zd 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( N + 1 ) e. ZZ )
43 simprl 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> b e. ZZ )
44 42 43 zsubcld 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( N + 1 ) - b ) e. ZZ )
45 42 zred 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( N + 1 ) e. RR )
46 zre 
 |-  ( N e. ZZ -> N e. RR )
47 46 adantr 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> N e. RR )
48 zre 
 |-  ( b e. ZZ -> b e. RR )
49 48 ad2antrl 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> b e. RR )
50 47 recnd 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> N e. CC )
51 pncan2 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - N ) = 1 )
52 50 21 51 sylancl 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( N + 1 ) - N ) = 1 )
53 simprr 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> 1 <_ b )
54 52 53 eqbrtrd 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( N + 1 ) - N ) <_ b )
55 45 47 49 54 subled 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( N + 1 ) - b ) <_ N )
56 42 zcnd 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( N + 1 ) e. CC )
57 zcn 
 |-  ( b e. ZZ -> b e. CC )
58 57 ad2antrl 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> b e. CC )
59 56 58 nncand 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( N + 1 ) - ( ( N + 1 ) - b ) ) = b )
60 59 eqcomd 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) )
61 44 55 60 jca31 
 |-  ( ( N e. ZZ /\ ( b e. ZZ /\ 1 <_ b ) ) -> ( ( ( ( N + 1 ) - b ) e. ZZ /\ ( ( N + 1 ) - b ) <_ N ) /\ b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) ) )
62 61 adantrr 
 |-  ( ( N e. ZZ /\ ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) ) -> ( ( ( ( N + 1 ) - b ) e. ZZ /\ ( ( N + 1 ) - b ) <_ N ) /\ b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) ) )
63 eleq1 
 |-  ( a = ( ( N + 1 ) - b ) -> ( a e. ZZ <-> ( ( N + 1 ) - b ) e. ZZ ) )
64 breq1 
 |-  ( a = ( ( N + 1 ) - b ) -> ( a <_ N <-> ( ( N + 1 ) - b ) <_ N ) )
65 63 64 anbi12d 
 |-  ( a = ( ( N + 1 ) - b ) -> ( ( a e. ZZ /\ a <_ N ) <-> ( ( ( N + 1 ) - b ) e. ZZ /\ ( ( N + 1 ) - b ) <_ N ) ) )
66 oveq2 
 |-  ( a = ( ( N + 1 ) - b ) -> ( ( N + 1 ) - a ) = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) )
67 66 eqeq2d 
 |-  ( a = ( ( N + 1 ) - b ) -> ( b = ( ( N + 1 ) - a ) <-> b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) ) )
68 65 67 anbi12d 
 |-  ( a = ( ( N + 1 ) - b ) -> ( ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) <-> ( ( ( ( N + 1 ) - b ) e. ZZ /\ ( ( N + 1 ) - b ) <_ N ) /\ b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) ) ) )
69 68 ad2antll 
 |-  ( ( N e. ZZ /\ ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) ) -> ( ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) <-> ( ( ( ( N + 1 ) - b ) e. ZZ /\ ( ( N + 1 ) - b ) <_ N ) /\ b = ( ( N + 1 ) - ( ( N + 1 ) - b ) ) ) ) )
70 62 69 mpbird 
 |-  ( ( N e. ZZ /\ ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) ) -> ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) )
71 40 70 impbida 
 |-  ( N e. ZZ -> ( ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) <-> ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) ) )
72 ellz1 
 |-  ( N e. ZZ -> ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) <-> ( a e. ZZ /\ a <_ N ) ) )
73 72 anbi1d 
 |-  ( N e. ZZ -> ( ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) /\ b = ( ( N + 1 ) - a ) ) <-> ( ( a e. ZZ /\ a <_ N ) /\ b = ( ( N + 1 ) - a ) ) ) )
74 elnnz1 
 |-  ( b e. NN <-> ( b e. ZZ /\ 1 <_ b ) )
75 74 a1i 
 |-  ( N e. ZZ -> ( b e. NN <-> ( b e. ZZ /\ 1 <_ b ) ) )
76 75 anbi1d 
 |-  ( N e. ZZ -> ( ( b e. NN /\ a = ( ( N + 1 ) - b ) ) <-> ( ( b e. ZZ /\ 1 <_ b ) /\ a = ( ( N + 1 ) - b ) ) ) )
77 71 73 76 3bitr4d 
 |-  ( N e. ZZ -> ( ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) /\ b = ( ( N + 1 ) - a ) ) <-> ( b e. NN /\ a = ( ( N + 1 ) - b ) ) ) )
78 3 5 7 9 77 en2d 
 |-  ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ NN )
79 nnenom 
 |-  NN ~~ _om
80 entr 
 |-  ( ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ NN /\ NN ~~ _om ) -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ _om )
81 78 79 80 sylancl 
 |-  ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ _om )