Step | Hyp | Ref
| Expression |
1 | | zeo 12149 |
. . . 4
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ∨
((𝑁 + 1) / 2) ∈
ℤ)) |
2 | | zre 12066 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
3 | | 2rp 12477 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
4 | | mod0 13335 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
ℝ+) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ)) |
5 | 2, 3, 4 | sylancl 589 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈
ℤ)) |
6 | 5 | biimpar 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
(𝑁 mod 2) =
0) |
7 | | eqeq1 2742 |
. . . . . . . 8
⊢ ((𝑁 mod 2) = 0 → ((𝑁 mod 2) = 1 ↔ 0 =
1)) |
8 | | 0ne1 11787 |
. . . . . . . . 9
⊢ 0 ≠
1 |
9 | | eqneqall 2945 |
. . . . . . . . 9
⊢ (0 = 1
→ (0 ≠ 1 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
10 | 8, 9 | mpi 20 |
. . . . . . . 8
⊢ (0 = 1
→ ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁) |
11 | 7, 10 | syl6bi 256 |
. . . . . . 7
⊢ ((𝑁 mod 2) = 0 → ((𝑁 mod 2) = 1 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
12 | 6, 11 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
13 | 12 | expcom 417 |
. . . . 5
⊢ ((𝑁 / 2) ∈ ℤ →
(𝑁 ∈ ℤ →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁))) |
14 | | peano2zm 12106 |
. . . . . . . . 9
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(((𝑁 + 1) / 2) − 1)
∈ ℤ) |
15 | | zcn 12067 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
16 | | xp1d2m1eqxm1d2 11970 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
18 | 17 | eleq1d 2817 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((((𝑁 + 1) / 2) − 1) ∈
ℤ ↔ ((𝑁 −
1) / 2) ∈ ℤ)) |
19 | 18 | biimpd 232 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((((𝑁 + 1) / 2) − 1) ∈
ℤ → ((𝑁 −
1) / 2) ∈ ℤ)) |
20 | 14, 19 | mpan9 510 |
. . . . . . . 8
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
((𝑁 − 1) / 2) ∈
ℤ) |
21 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑛 = ((𝑁 − 1) / 2) → (2 · 𝑛) = (2 · ((𝑁 − 1) /
2))) |
22 | 21 | adantl 485 |
. . . . . . . . . 10
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
(2 · 𝑛) = (2
· ((𝑁 − 1) /
2))) |
23 | 22 | oveq1d 7185 |
. . . . . . . . 9
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · 𝑛) + 1) = ((2
· ((𝑁 − 1) /
2)) + 1)) |
24 | | peano2zm 12106 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
25 | 24 | zcnd 12169 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℂ) |
26 | | 2cnd 11794 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) |
27 | | 2ne0 11820 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 2 ≠
0) |
29 | 25, 26, 28 | divcan2d 11496 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (2
· ((𝑁 − 1) /
2)) = (𝑁 −
1)) |
30 | 29 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((2
· ((𝑁 − 1) /
2)) + 1) = ((𝑁 − 1) +
1)) |
31 | | npcan1 11143 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
32 | 15, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) + 1) = 𝑁) |
33 | 30, 32 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((2
· ((𝑁 − 1) /
2)) + 1) = 𝑁) |
34 | 33 | ad2antlr 727 |
. . . . . . . . 9
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · ((𝑁 − 1)
/ 2)) + 1) = 𝑁) |
35 | 23, 34 | eqtrd 2773 |
. . . . . . . 8
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · 𝑛) + 1) =
𝑁) |
36 | 20, 35 | rspcedeq1vd 3532 |
. . . . . . 7
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
37 | 36 | a1d 25 |
. . . . . 6
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
38 | 37 | ex 416 |
. . . . 5
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(𝑁 ∈ ℤ →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁))) |
39 | 13, 38 | jaoi 856 |
. . . 4
⊢ (((𝑁 / 2) ∈ ℤ ∨
((𝑁 + 1) / 2) ∈
ℤ) → (𝑁 ∈
ℤ → ((𝑁 mod 2) =
1 → ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁))) |
40 | 1, 39 | mpcom 38 |
. . 3
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
41 | | oveq1 7177 |
. . . . . 6
⊢ (𝑁 = ((2 · 𝑛) + 1) → (𝑁 mod 2) = (((2 · 𝑛) + 1) mod 2)) |
42 | 41 | eqcoms 2746 |
. . . . 5
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑁 mod 2) = (((2 · 𝑛) + 1) mod 2)) |
43 | | 2cnd 11794 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
44 | | zcn 12067 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
45 | 43, 44 | mulcomd 10740 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) = (𝑛 · 2)) |
46 | 45 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) mod 2) =
((𝑛 · 2) mod
2)) |
47 | | mulmod0 13336 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 2 ∈
ℝ+) → ((𝑛 · 2) mod 2) = 0) |
48 | 3, 47 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((𝑛 · 2) mod 2) =
0) |
49 | 46, 48 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) mod 2) =
0) |
50 | 49 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) mod 2) + 1) =
(0 + 1)) |
51 | | 0p1e1 11838 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
52 | 50, 51 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) mod 2) + 1) =
1) |
53 | 52 | oveq1d 7185 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) mod 2) + 1) mod
2) = (1 mod 2)) |
54 | | 2z 12095 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
56 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
57 | 55, 56 | zmulcld 12174 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
58 | 57 | zred 12168 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℝ) |
59 | | 1red 10720 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 1 ∈
ℝ) |
60 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 2 ∈
ℝ+) |
61 | | modaddmod 13369 |
. . . . . . . 8
⊢ (((2
· 𝑛) ∈ ℝ
∧ 1 ∈ ℝ ∧ 2 ∈ ℝ+) → ((((2
· 𝑛) mod 2) + 1) mod
2) = (((2 · 𝑛) + 1)
mod 2)) |
62 | 58, 59, 60, 61 | syl3anc 1372 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) mod 2) + 1) mod
2) = (((2 · 𝑛) + 1)
mod 2)) |
63 | | 2re 11790 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
64 | | 1lt2 11887 |
. . . . . . . . 9
⊢ 1 <
2 |
65 | 63, 64 | pm3.2i 474 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 1 < 2) |
66 | | 1mod 13362 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 1 < 2) → (1 mod 2) = 1) |
67 | 65, 66 | mp1i 13 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → (1 mod 2)
= 1) |
68 | 53, 62, 67 | 3eqtr3d 2781 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) mod 2) =
1) |
69 | 68 | adantl 485 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) mod 2) =
1) |
70 | 42, 69 | sylan9eqr 2795 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ((2
· 𝑛) + 1) = 𝑁) → (𝑁 mod 2) = 1) |
71 | 70 | rexlimdva2 3197 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑁 mod 2) = 1)) |
72 | 40, 71 | impbid 215 |
. 2
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
73 | | odd2np1 15786 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
74 | 72, 73 | bitr4d 285 |
1
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2
∥ 𝑁)) |