| Step | Hyp | Ref
| Expression |
| 1 | | odd2np1 16378 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
| 2 | | halfre 12480 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (1 / 2)
∈ ℝ) |
| 4 | | 1red 11262 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 1 ∈
ℝ) |
| 5 | | zre 12617 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
| 6 | 3, 4, 5 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
| 8 | | halflt1 12484 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
< 1 |
| 9 | | axltadd 11334 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((1 / 2) < 1
→ (𝑛 + (1 / 2)) <
(𝑛 + 1))) |
| 10 | 7, 8, 9 | mpisyl 21 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) < (𝑛 + 1)) |
| 11 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈
ℝ) |
| 13 | 5, 3 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + (1 / 2)) ∈
ℝ) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) ∈
ℝ) |
| 15 | | peano2z 12658 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℤ) |
| 16 | 15 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℝ) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + 1) ∈
ℝ) |
| 18 | | lttr 11337 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ ∧
(𝑛 + 1) ∈ ℝ)
→ ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
| 19 | 12, 14, 17, 18 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
| 20 | 10, 19 | mpan2d 694 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 < (𝑛 + 1))) |
| 21 | | zleltp1 12668 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
| 22 | 21 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
| 23 | 20, 22 | sylibrd 259 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 ≤ 𝑛)) |
| 24 | | halfgt0 12482 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
| 25 | 3, 5 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
| 27 | | ltaddpos 11753 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ) → (0 < (1 / 2) ↔ 𝑛 < (𝑛 + (1 / 2)))) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 <
(1 / 2) ↔ 𝑛 <
(𝑛 + (1 /
2)))) |
| 29 | 24, 28 | mpbii 233 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 < (𝑛 + (1 / 2))) |
| 30 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℝ) |
| 31 | | lelttr 11351 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ)
→ ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
| 32 | 12, 30, 14, 31 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
| 33 | 29, 32 | mpan2d 694 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 → 𝑀 < (𝑛 + (1 / 2)))) |
| 34 | 23, 33 | impbid 212 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) ↔ 𝑀 ≤ 𝑛)) |
| 35 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 36 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 1 ∈
ℂ) |
| 37 | | 2cnne0 12476 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
| 39 | | muldivdir 11960 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
| 40 | 35, 36, 38, 39 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
| 41 | 40 | breq2d 5155 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
| 42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
| 43 | | 2z 12649 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
| 45 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
| 46 | 44, 45 | zmulcld 12728 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
| 47 | 46 | zcnd 12723 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
· 𝑛) ∈
ℂ) |
| 49 | | pncan1 11687 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑛) ∈ ℂ
→ (((2 · 𝑛) +
1) − 1) = (2 · 𝑛)) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
| 51 | 50 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = ((2 · 𝑛) /
2)) |
| 52 | | 2cnd 12344 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
| 53 | | 2ne0 12370 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
| 54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ≠
0) |
| 55 | 35, 52, 54 | divcan3d 12048 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) / 2) = 𝑛) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2
· 𝑛) / 2) = 𝑛) |
| 57 | 51, 56 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
| 58 | 57 | breq2d 5155 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔
𝑀 ≤ 𝑛)) |
| 59 | 34, 42, 58 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) /
2))) |
| 60 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
| 61 | 60 | breq2d 5155 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑁 / 2))) |
| 62 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) − 1) = (𝑁 − 1)) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) − 1) / 2) = ((𝑁 − 1) /
2)) |
| 64 | 63 | breq2d 5155 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |
| 65 | 61, 64 | bibi12d 345 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2)) ↔ (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
| 66 | 59, 65 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
| 67 | 66 | ex 412 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
| 68 | 67 | adantl 481 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
| 69 | 68 | com23 86 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
| 70 | 69 | rexlimdva 3155 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
| 71 | 1, 70 | sylbid 240 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
| 72 | 71 | 3imp 1111 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |