| Step | Hyp | Ref
| Expression |
| 1 | | zeo 12704 |
. . . 4
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ∨
((𝑁 + 1) / 2) ∈
ℤ)) |
| 2 | | zre 12617 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 3 | | 2rp 13039 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
| 4 | | mod0 13916 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
ℝ+) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ)) |
| 5 | 2, 3, 4 | sylancl 586 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈
ℤ)) |
| 6 | 5 | biimpar 477 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
(𝑁 mod 2) =
0) |
| 7 | | eqeq1 2741 |
. . . . . . . 8
⊢ ((𝑁 mod 2) = 0 → ((𝑁 mod 2) = 1 ↔ 0 =
1)) |
| 8 | | 0ne1 12337 |
. . . . . . . . 9
⊢ 0 ≠
1 |
| 9 | | eqneqall 2951 |
. . . . . . . . 9
⊢ (0 = 1
→ (0 ≠ 1 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
| 10 | 8, 9 | mpi 20 |
. . . . . . . 8
⊢ (0 = 1
→ ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁) |
| 11 | 7, 10 | biimtrdi 253 |
. . . . . . 7
⊢ ((𝑁 mod 2) = 0 → ((𝑁 mod 2) = 1 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
| 12 | 6, 11 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
| 13 | 12 | expcom 413 |
. . . . 5
⊢ ((𝑁 / 2) ∈ ℤ →
(𝑁 ∈ ℤ →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁))) |
| 14 | | peano2zm 12660 |
. . . . . . . . 9
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(((𝑁 + 1) / 2) − 1)
∈ ℤ) |
| 15 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 16 | | xp1d2m1eqxm1d2 12520 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
| 18 | 17 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((((𝑁 + 1) / 2) − 1) ∈
ℤ ↔ ((𝑁 −
1) / 2) ∈ ℤ)) |
| 19 | 18 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((((𝑁 + 1) / 2) − 1) ∈
ℤ → ((𝑁 −
1) / 2) ∈ ℤ)) |
| 20 | 14, 19 | mpan9 506 |
. . . . . . . 8
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
((𝑁 − 1) / 2) ∈
ℤ) |
| 21 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑛 = ((𝑁 − 1) / 2) → (2 · 𝑛) = (2 · ((𝑁 − 1) /
2))) |
| 22 | 21 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
(2 · 𝑛) = (2
· ((𝑁 − 1) /
2))) |
| 23 | 22 | oveq1d 7446 |
. . . . . . . . 9
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · 𝑛) + 1) = ((2
· ((𝑁 − 1) /
2)) + 1)) |
| 24 | | peano2zm 12660 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
| 25 | 24 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℂ) |
| 26 | | 2cnd 12344 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) |
| 27 | | 2ne0 12370 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
| 28 | 27 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 2 ≠
0) |
| 29 | 25, 26, 28 | divcan2d 12045 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (2
· ((𝑁 − 1) /
2)) = (𝑁 −
1)) |
| 30 | 29 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((2
· ((𝑁 − 1) /
2)) + 1) = ((𝑁 − 1) +
1)) |
| 31 | | npcan1 11688 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 32 | 15, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) + 1) = 𝑁) |
| 33 | 30, 32 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((2
· ((𝑁 − 1) /
2)) + 1) = 𝑁) |
| 34 | 33 | ad2antlr 727 |
. . . . . . . . 9
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · ((𝑁 − 1)
/ 2)) + 1) = 𝑁) |
| 35 | 23, 34 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((𝑁 + 1) / 2)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ 𝑛 =
((𝑁 − 1) / 2)) →
((2 · 𝑛) + 1) =
𝑁) |
| 36 | 20, 35 | rspcedeq1vd 3629 |
. . . . . . 7
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
| 37 | 36 | a1d 25 |
. . . . . 6
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
𝑁 ∈ ℤ) →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
| 38 | 37 | ex 412 |
. . . . 5
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(𝑁 ∈ ℤ →
((𝑁 mod 2) = 1 →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁))) |
| 39 | 13, 38 | jaoi 858 |
. . . 4
⊢ (((𝑁 / 2) ∈ ℤ ∨
((𝑁 + 1) / 2) ∈
ℤ) → (𝑁 ∈
ℤ → ((𝑁 mod 2) =
1 → ∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁))) |
| 40 | 1, 39 | mpcom 38 |
. . 3
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
| 41 | | oveq1 7438 |
. . . . . 6
⊢ (𝑁 = ((2 · 𝑛) + 1) → (𝑁 mod 2) = (((2 · 𝑛) + 1) mod 2)) |
| 42 | 41 | eqcoms 2745 |
. . . . 5
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑁 mod 2) = (((2 · 𝑛) + 1) mod 2)) |
| 43 | | 2cnd 12344 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
| 44 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 45 | 43, 44 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) = (𝑛 · 2)) |
| 46 | 45 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) mod 2) =
((𝑛 · 2) mod
2)) |
| 47 | | mulmod0 13917 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 2 ∈
ℝ+) → ((𝑛 · 2) mod 2) = 0) |
| 48 | 3, 47 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((𝑛 · 2) mod 2) =
0) |
| 49 | 46, 48 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) mod 2) =
0) |
| 50 | 49 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) mod 2) + 1) =
(0 + 1)) |
| 51 | | 0p1e1 12388 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 52 | 50, 51 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) mod 2) + 1) =
1) |
| 53 | 52 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) mod 2) + 1) mod
2) = (1 mod 2)) |
| 54 | | 2z 12649 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
| 56 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
| 57 | 55, 56 | zmulcld 12728 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
| 58 | 57 | zred 12722 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℝ) |
| 59 | | 1red 11262 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 1 ∈
ℝ) |
| 60 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 2 ∈
ℝ+) |
| 61 | | modaddmod 13950 |
. . . . . . . 8
⊢ (((2
· 𝑛) ∈ ℝ
∧ 1 ∈ ℝ ∧ 2 ∈ ℝ+) → ((((2
· 𝑛) mod 2) + 1) mod
2) = (((2 · 𝑛) + 1)
mod 2)) |
| 62 | 58, 59, 60, 61 | syl3anc 1373 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) mod 2) + 1) mod
2) = (((2 · 𝑛) + 1)
mod 2)) |
| 63 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 64 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 65 | 63, 64 | pm3.2i 470 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 1 < 2) |
| 66 | | 1mod 13943 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 1 < 2) → (1 mod 2) = 1) |
| 67 | 65, 66 | mp1i 13 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → (1 mod 2)
= 1) |
| 68 | 53, 62, 67 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) mod 2) =
1) |
| 69 | 68 | adantl 481 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) mod 2) =
1) |
| 70 | 42, 69 | sylan9eqr 2799 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ((2
· 𝑛) + 1) = 𝑁) → (𝑁 mod 2) = 1) |
| 71 | 70 | rexlimdva2 3157 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑁 mod 2) = 1)) |
| 72 | 40, 71 | impbid 212 |
. 2
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
| 73 | | odd2np1 16378 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
| 74 | 72, 73 | bitr4d 282 |
1
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2
∥ 𝑁)) |