Metamath Proof Explorer

Theorem lzenom

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

Ref Expression
Assertion lzenom ⊢N∈ℤ→ℤ∖ℤ≥N+1≈ω

Proof

Step Hyp Ref Expression
1 zex ⊢ℤ∈V
2 difexg ⊢ℤ∈V→ℤ∖ℤ≥N+1∈V
3 1 2 mp1i ⊢N∈ℤ→ℤ∖ℤ≥N+1∈V
4 nnex ⊢ℕ∈V
5 4 a1i ⊢N∈ℤ→ℕ∈V
6 ovex ⊢N+1-a∈V
7 6 2a1i ⊢N∈ℤ→a∈ℤ∖ℤ≥N+1→N+1-a∈V
8 ovex ⊢N+1-b∈V
9 8 2a1i ⊢N∈ℤ→b∈ℕ→N+1-b∈V
10 simpl ⊢N∈ℤ∧a∈ℤ∧a≤N→N∈ℤ
11 10 peano2zd ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1∈ℤ
12 simprl ⊢N∈ℤ∧a∈ℤ∧a≤N→a∈ℤ
13 11 12 zsubcld ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1-a∈ℤ
14 zre ⊢a∈ℤ→a∈ℝ
15 14 ad2antrl ⊢N∈ℤ∧a∈ℤ∧a≤N→a∈ℝ
16 11 zred ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1∈ℝ
17 1red ⊢N∈ℤ∧a∈ℤ∧a≤N→1∈ℝ
18 simprr ⊢N∈ℤ∧a∈ℤ∧a≤N→a≤N
19 zcn ⊢N∈ℤ→N∈ℂ
20 19 adantr ⊢N∈ℤ∧a∈ℤ∧a≤N→N∈ℂ
21 ax-1cn ⊢1∈ℂ
22 pncan ⊢N∈ℂ∧1∈ℂ→N+1-1=N
23 20 21 22 sylancl ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1-1=N
24 18 23 breqtrrd ⊢N∈ℤ∧a∈ℤ∧a≤N→a≤N+1-1
25 15 16 17 24 lesubd ⊢N∈ℤ∧a∈ℤ∧a≤N→1≤N+1-a
26 11 zcnd ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1∈ℂ
27 zcn ⊢a∈ℤ→a∈ℂ
28 27 ad2antrl ⊢N∈ℤ∧a∈ℤ∧a≤N→a∈ℂ
29 26 28 nncand ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1-N+1-a=a
30 29 eqcomd ⊢N∈ℤ∧a∈ℤ∧a≤N→a=N+1-N+1-a
31 13 25 30 jca31 ⊢N∈ℤ∧a∈ℤ∧a≤N→N+1-a∈ℤ∧1≤N+1-a∧a=N+1-N+1-a
32 31 adantrr ⊢N∈ℤ∧a∈ℤ∧a≤N∧b=N+1-a→N+1-a∈ℤ∧1≤N+1-a∧a=N+1-N+1-a
33 eleq1 ⊢b=N+1-a→b∈ℤ↔N+1-a∈ℤ
34 breq2 ⊢b=N+1-a→1≤b↔1≤N+1-a
35 33 34 anbi12d ⊢b=N+1-a→b∈ℤ∧1≤b↔N+1-a∈ℤ∧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∈ℤ∧1≤b∧a=N+1-b↔N+1-a∈ℤ∧1≤N+1-a∧a=N+1-N+1-a
39 38 ad2antll ⊢N∈ℤ∧a∈ℤ∧a≤N∧b=N+1-a→b∈ℤ∧1≤b∧a=N+1-b↔N+1-a∈ℤ∧1≤N+1-a∧a=N+1-N+1-a
40 32 39 mpbird ⊢N∈ℤ∧a∈ℤ∧a≤N∧b=N+1-a→b∈ℤ∧1≤b∧a=N+1-b
41 simpl ⊢N∈ℤ∧b∈ℤ∧1≤b→N∈ℤ
42 41 peano2zd ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1∈ℤ
43 simprl ⊢N∈ℤ∧b∈ℤ∧1≤b→b∈ℤ
44 42 43 zsubcld ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-b∈ℤ
45 42 zred ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1∈ℝ
46 zre ⊢N∈ℤ→N∈ℝ
47 46 adantr ⊢N∈ℤ∧b∈ℤ∧1≤b→N∈ℝ
48 zre ⊢b∈ℤ→b∈ℝ
49 48 ad2antrl ⊢N∈ℤ∧b∈ℤ∧1≤b→b∈ℝ
50 47 recnd ⊢N∈ℤ∧b∈ℤ∧1≤b→N∈ℂ
51 pncan2 ⊢N∈ℂ∧1∈ℂ→N+1-N=1
52 50 21 51 sylancl ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-N=1
53 simprr ⊢N∈ℤ∧b∈ℤ∧1≤b→1≤b
54 52 53 eqbrtrd ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-N≤b
55 45 47 49 54 subled ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-b≤N
56 42 zcnd ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1∈ℂ
57 zcn ⊢b∈ℤ→b∈ℂ
58 57 ad2antrl ⊢N∈ℤ∧b∈ℤ∧1≤b→b∈ℂ
59 56 58 nncand ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-N+1-b=b
60 59 eqcomd ⊢N∈ℤ∧b∈ℤ∧1≤b→b=N+1-N+1-b
61 44 55 60 jca31 ⊢N∈ℤ∧b∈ℤ∧1≤b→N+1-b∈ℤ∧N+1-b≤N∧b=N+1-N+1-b
62 61 adantrr ⊢N∈ℤ∧b∈ℤ∧1≤b∧a=N+1-b→N+1-b∈ℤ∧N+1-b≤N∧b=N+1-N+1-b
63 eleq1 ⊢a=N+1-b→a∈ℤ↔N+1-b∈ℤ
64 breq1 ⊢a=N+1-b→a≤N↔N+1-b≤N
65 63 64 anbi12d ⊢a=N+1-b→a∈ℤ∧a≤N↔N+1-b∈ℤ∧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∈ℤ∧a≤N∧b=N+1-a↔N+1-b∈ℤ∧N+1-b≤N∧b=N+1-N+1-b
69 68 ad2antll ⊢N∈ℤ∧b∈ℤ∧1≤b∧a=N+1-b→a∈ℤ∧a≤N∧b=N+1-a↔N+1-b∈ℤ∧N+1-b≤N∧b=N+1-N+1-b
70 62 69 mpbird ⊢N∈ℤ∧b∈ℤ∧1≤b∧a=N+1-b→a∈ℤ∧a≤N∧b=N+1-a
71 40 70 impbida ⊢N∈ℤ→a∈ℤ∧a≤N∧b=N+1-a↔b∈ℤ∧1≤b∧a=N+1-b
72 ellz1 ⊢N∈ℤ→a∈ℤ∖ℤ≥N+1↔a∈ℤ∧a≤N
73 72 anbi1d ⊢N∈ℤ→a∈ℤ∖ℤ≥N+1∧b=N+1-a↔a∈ℤ∧a≤N∧b=N+1-a
74 elnnz1 ⊢b∈ℕ↔b∈ℤ∧1≤b
75 74 a1i ⊢N∈ℤ→b∈ℕ↔b∈ℤ∧1≤b
76 75 anbi1d ⊢N∈ℤ→b∈ℕ∧a=N+1-b↔b∈ℤ∧1≤b∧a=N+1-b
77 71 73 76 3bitr4d ⊢N∈ℤ→a∈ℤ∖ℤ≥N+1∧b=N+1-a↔b∈ℕ∧a=N+1-b
78 3 5 7 9 77 en2d ⊢N∈ℤ→ℤ∖ℤ≥N+1≈ℕ
79 nnenom ⊢ℕ≈ω
80 entr ⊢ℤ∖ℤ≥N+1≈ℕ∧ℕ≈ω→ℤ∖ℤ≥N+1≈ω
81 78 79 80 sylancl ⊢N∈ℤ→ℤ∖ℤ≥N+1≈ω