Step | Hyp | Ref
| Expression |
1 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = 0 → (((2 · 𝑛) + 1) = 𝑗 ↔ ((2 · 𝑛) + 1) = 0)) |
2 | 1 | rexbidv 2471 |
. . 3
⊢ (𝑗 = 0 → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑗 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) =
0)) |
3 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = 0 → ((𝑘 · 2) = 𝑗 ↔ (𝑘 · 2) = 0)) |
4 | 3 | rexbidv 2471 |
. . 3
⊢ (𝑗 = 0 → (∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) =
0)) |
5 | 2, 4 | orbi12d 788 |
. 2
⊢ (𝑗 = 0 → ((∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑗 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 0 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) =
0))) |
6 | | eqeq2 2180 |
. . . . 5
⊢ (𝑗 = 𝑚 → (((2 · 𝑛) + 1) = 𝑗 ↔ ((2 · 𝑛) + 1) = 𝑚)) |
7 | 6 | rexbidv 2471 |
. . . 4
⊢ (𝑗 = 𝑚 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑚)) |
8 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑛 = 𝑥 → (2 · 𝑛) = (2 · 𝑥)) |
9 | 8 | oveq1d 5868 |
. . . . . 6
⊢ (𝑛 = 𝑥 → ((2 · 𝑛) + 1) = ((2 · 𝑥) + 1)) |
10 | 9 | eqeq1d 2179 |
. . . . 5
⊢ (𝑛 = 𝑥 → (((2 · 𝑛) + 1) = 𝑚 ↔ ((2 · 𝑥) + 1) = 𝑚)) |
11 | 10 | cbvrexv 2697 |
. . . 4
⊢
(∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑚 ↔ ∃𝑥 ∈ ℤ ((2 ·
𝑥) + 1) = 𝑚) |
12 | 7, 11 | bitrdi 195 |
. . 3
⊢ (𝑗 = 𝑚 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ↔ ∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = 𝑚)) |
13 | | eqeq2 2180 |
. . . . 5
⊢ (𝑗 = 𝑚 → ((𝑘 · 2) = 𝑗 ↔ (𝑘 · 2) = 𝑚)) |
14 | 13 | rexbidv 2471 |
. . . 4
⊢ (𝑗 = 𝑚 → (∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑚)) |
15 | | oveq1 5860 |
. . . . . 6
⊢ (𝑘 = 𝑦 → (𝑘 · 2) = (𝑦 · 2)) |
16 | 15 | eqeq1d 2179 |
. . . . 5
⊢ (𝑘 = 𝑦 → ((𝑘 · 2) = 𝑚 ↔ (𝑦 · 2) = 𝑚)) |
17 | 16 | cbvrexv 2697 |
. . . 4
⊢
(∃𝑘 ∈
ℤ (𝑘 · 2) =
𝑚 ↔ ∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚) |
18 | 14, 17 | bitrdi 195 |
. . 3
⊢ (𝑗 = 𝑚 → (∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗 ↔ ∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚)) |
19 | 12, 18 | orbi12d 788 |
. 2
⊢ (𝑗 = 𝑚 → ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗) ↔ (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = 𝑚 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚))) |
20 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = (𝑚 + 1) → (((2 · 𝑛) + 1) = 𝑗 ↔ ((2 · 𝑛) + 1) = (𝑚 + 1))) |
21 | 20 | rexbidv 2471 |
. . 3
⊢ (𝑗 = (𝑚 + 1) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (𝑚 + 1))) |
22 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = (𝑚 + 1) → ((𝑘 · 2) = 𝑗 ↔ (𝑘 · 2) = (𝑚 + 1))) |
23 | 22 | rexbidv 2471 |
. . 3
⊢ (𝑗 = (𝑚 + 1) → (∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1))) |
24 | 21, 23 | orbi12d 788 |
. 2
⊢ (𝑗 = (𝑚 + 1) → ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (𝑚 + 1) ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1)))) |
25 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = 𝑁 → (((2 · 𝑛) + 1) = 𝑗 ↔ ((2 · 𝑛) + 1) = 𝑁)) |
26 | 25 | rexbidv 2471 |
. . 3
⊢ (𝑗 = 𝑁 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
27 | | eqeq2 2180 |
. . . 4
⊢ (𝑗 = 𝑁 → ((𝑘 · 2) = 𝑗 ↔ (𝑘 · 2) = 𝑁)) |
28 | 27 | rexbidv 2471 |
. . 3
⊢ (𝑗 = 𝑁 → (∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
29 | 26, 28 | orbi12d 788 |
. 2
⊢ (𝑗 = 𝑁 → ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑗 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑗) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))) |
30 | | 0z 9223 |
. . . 4
⊢ 0 ∈
ℤ |
31 | | 2cn 8949 |
. . . . 5
⊢ 2 ∈
ℂ |
32 | 31 | mul02i 8309 |
. . . 4
⊢ (0
· 2) = 0 |
33 | | oveq1 5860 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑘 · 2) = (0 ·
2)) |
34 | 33 | eqeq1d 2179 |
. . . . 5
⊢ (𝑘 = 0 → ((𝑘 · 2) = 0 ↔ (0 · 2) =
0)) |
35 | 34 | rspcev 2834 |
. . . 4
⊢ ((0
∈ ℤ ∧ (0 · 2) = 0) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 0) |
36 | 30, 32, 35 | mp2an 424 |
. . 3
⊢
∃𝑘 ∈
ℤ (𝑘 · 2) =
0 |
37 | 36 | olci 727 |
. 2
⊢
(∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 0 ∨ ∃𝑘 ∈
ℤ (𝑘 · 2) =
0) |
38 | | orcom 723 |
. . 3
⊢
((∃𝑥 ∈
ℤ ((2 · 𝑥) +
1) = 𝑚 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚) ↔ (∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚 ∨ ∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = 𝑚)) |
39 | | zcn 9217 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
40 | | mulcom 7903 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑦 ·
2) = (2 · 𝑦)) |
41 | 39, 31, 40 | sylancl 411 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ → (𝑦 · 2) = (2 · 𝑦)) |
42 | 41 | adantl 275 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑦 ∈ ℤ)
→ (𝑦 · 2) = (2
· 𝑦)) |
43 | 42 | eqeq1d 2179 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ 𝑦 ∈ ℤ)
→ ((𝑦 · 2) =
𝑚 ↔ (2 · 𝑦) = 𝑚)) |
44 | | eqid 2170 |
. . . . . . . . 9
⊢ ((2
· 𝑦) + 1) = ((2
· 𝑦) +
1) |
45 | | oveq2 5861 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → (2 · 𝑛) = (2 · 𝑦)) |
46 | 45 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑦 → ((2 · 𝑛) + 1) = ((2 · 𝑦) + 1)) |
47 | 46 | eqeq1d 2179 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (((2 · 𝑛) + 1) = ((2 · 𝑦) + 1) ↔ ((2 · 𝑦) + 1) = ((2 · 𝑦) + 1))) |
48 | 47 | rspcev 2834 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ ((2
· 𝑦) + 1) = ((2
· 𝑦) + 1)) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = ((2
· 𝑦) +
1)) |
49 | 44, 48 | mpan2 423 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = ((2
· 𝑦) +
1)) |
50 | | oveq1 5860 |
. . . . . . . . . 10
⊢ ((2
· 𝑦) = 𝑚 → ((2 · 𝑦) + 1) = (𝑚 + 1)) |
51 | 50 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((2
· 𝑦) = 𝑚 → (((2 · 𝑛) + 1) = ((2 · 𝑦) + 1) ↔ ((2 · 𝑛) + 1) = (𝑚 + 1))) |
52 | 51 | rexbidv 2471 |
. . . . . . . 8
⊢ ((2
· 𝑦) = 𝑚 → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = ((2 ·
𝑦) + 1) ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1))) |
53 | 49, 52 | syl5ibcom 154 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ → ((2
· 𝑦) = 𝑚 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1))) |
54 | 53 | adantl 275 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ 𝑦 ∈ ℤ)
→ ((2 · 𝑦) =
𝑚 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1))) |
55 | 43, 54 | sylbid 149 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ 𝑦 ∈ ℤ)
→ ((𝑦 · 2) =
𝑚 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1))) |
56 | 55 | rexlimdva 2587 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (∃𝑦 ∈
ℤ (𝑦 · 2) =
𝑚 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1))) |
57 | | peano2z 9248 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈
ℤ) |
58 | 57 | adantl 275 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (𝑥 + 1) ∈
ℤ) |
59 | | zcn 9217 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
60 | | mulcom 7903 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑥 ·
2) = (2 · 𝑥)) |
61 | 31, 60 | mpan2 423 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥 · 2) = (2 · 𝑥)) |
62 | 31 | mulid2i 7923 |
. . . . . . . . . . . . 13
⊢ (1
· 2) = 2 |
63 | 62 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (1
· 2) = 2) |
64 | 61, 63 | oveq12d 5871 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → ((𝑥 · 2) + (1 · 2)) =
((2 · 𝑥) +
2)) |
65 | | df-2 8937 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
66 | 65 | oveq2i 5864 |
. . . . . . . . . . 11
⊢ ((2
· 𝑥) + 2) = ((2
· 𝑥) + (1 +
1)) |
67 | 64, 66 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → ((𝑥 · 2) + (1 · 2)) =
((2 · 𝑥) + (1 +
1))) |
68 | | ax-1cn 7867 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
69 | | adddir 7911 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ ∧ 2 ∈ ℂ) → ((𝑥 + 1) · 2) = ((𝑥 · 2) + (1 ·
2))) |
70 | 68, 31, 69 | mp3an23 1324 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → ((𝑥 + 1) · 2) = ((𝑥 · 2) + (1 ·
2))) |
71 | | mulcl 7901 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
72 | 31, 71 | mpan 422 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
73 | | addass 7904 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑥) ∈ ℂ
∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + 1) + 1) = ((2 · 𝑥) + (1 + 1))) |
74 | 68, 68, 73 | mp3an23 1324 |
. . . . . . . . . . 11
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
1) + 1) = ((2 · 𝑥) +
(1 + 1))) |
75 | 72, 74 | syl 14 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (((2
· 𝑥) + 1) + 1) = ((2
· 𝑥) + (1 +
1))) |
76 | 67, 70, 75 | 3eqtr4d 2213 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → ((𝑥 + 1) · 2) = (((2
· 𝑥) + 1) +
1)) |
77 | 59, 76 | syl 14 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → ((𝑥 + 1) · 2) = (((2
· 𝑥) + 1) +
1)) |
78 | 77 | adantl 275 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((𝑥 + 1) · 2)
= (((2 · 𝑥) + 1) +
1)) |
79 | | oveq1 5860 |
. . . . . . . . 9
⊢ (𝑘 = (𝑥 + 1) → (𝑘 · 2) = ((𝑥 + 1) · 2)) |
80 | 79 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑘 = (𝑥 + 1) → ((𝑘 · 2) = (((2 · 𝑥) + 1) + 1) ↔ ((𝑥 + 1) · 2) = (((2
· 𝑥) + 1) +
1))) |
81 | 80 | rspcev 2834 |
. . . . . . 7
⊢ (((𝑥 + 1) ∈ ℤ ∧
((𝑥 + 1) · 2) = (((2
· 𝑥) + 1) + 1))
→ ∃𝑘 ∈
ℤ (𝑘 · 2) =
(((2 · 𝑥) + 1) +
1)) |
82 | 58, 78, 81 | syl2anc 409 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ∃𝑘 ∈
ℤ (𝑘 · 2) =
(((2 · 𝑥) + 1) +
1)) |
83 | | oveq1 5860 |
. . . . . . . 8
⊢ (((2
· 𝑥) + 1) = 𝑚 → (((2 · 𝑥) + 1) + 1) = (𝑚 + 1)) |
84 | 83 | eqeq2d 2182 |
. . . . . . 7
⊢ (((2
· 𝑥) + 1) = 𝑚 → ((𝑘 · 2) = (((2 · 𝑥) + 1) + 1) ↔ (𝑘 · 2) = (𝑚 + 1))) |
85 | 84 | rexbidv 2471 |
. . . . . 6
⊢ (((2
· 𝑥) + 1) = 𝑚 → (∃𝑘 ∈ ℤ (𝑘 · 2) = (((2 ·
𝑥) + 1) + 1) ↔
∃𝑘 ∈ ℤ
(𝑘 · 2) = (𝑚 + 1))) |
86 | 82, 85 | syl5ibcom 154 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((2 · 𝑥) +
1) = 𝑚 → ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1))) |
87 | 86 | rexlimdva 2587 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (∃𝑥 ∈
ℤ ((2 · 𝑥) +
1) = 𝑚 → ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1))) |
88 | 56, 87 | orim12d 781 |
. . 3
⊢ (𝑚 ∈ ℕ0
→ ((∃𝑦 ∈
ℤ (𝑦 · 2) =
𝑚 ∨ ∃𝑥 ∈ ℤ ((2 ·
𝑥) + 1) = 𝑚) → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1) ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1)))) |
89 | 38, 88 | syl5bi 151 |
. 2
⊢ (𝑚 ∈ ℕ0
→ ((∃𝑥 ∈
ℤ ((2 · 𝑥) +
1) = 𝑚 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = 𝑚) → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = (𝑚 + 1) ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑚 + 1)))) |
90 | 5, 19, 24, 29, 37, 89 | nn0ind 9326 |
1
⊢ (𝑁 ∈ ℕ0
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |