Metamath Proof Explorer

Theorem lzenom

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

Ref Expression
Assertion lzenom ( 𝑁 ∈ ℤ → ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ≈ ω )

Proof

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