Proof of Theorem proththdlem
| Step | Hyp | Ref
| Expression |
| 1 | | proththd.p |
. 2
⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) |
| 2 | | proththd.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 3 | | 2nn 12339 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
| 4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℕ) |
| 5 | | proththd.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 6 | 5 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 7 | 4, 6 | nnexpcld 14284 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
| 8 | 2, 7 | nnmulcld 12319 |
. . . . 5
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℕ) |
| 9 | 8 | peano2nnd 12283 |
. . . 4
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) ∈ ℕ) |
| 10 | | 1m1e0 12338 |
. . . . . 6
⊢ (1
− 1) = 0 |
| 11 | 8 | nngt0d 12315 |
. . . . . 6
⊢ (𝜑 → 0 < (𝐾 · (2↑𝑁))) |
| 12 | 10, 11 | eqbrtrid 5178 |
. . . . 5
⊢ (𝜑 → (1 − 1) < (𝐾 · (2↑𝑁))) |
| 13 | | 1red 11262 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
| 14 | 8 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℝ) |
| 15 | 13, 13, 14 | ltsubaddd 11859 |
. . . . 5
⊢ (𝜑 → ((1 − 1) < (𝐾 · (2↑𝑁)) ↔ 1 < ((𝐾 · (2↑𝑁)) + 1))) |
| 16 | 12, 15 | mpbid 232 |
. . . 4
⊢ (𝜑 → 1 < ((𝐾 · (2↑𝑁)) + 1)) |
| 17 | 8 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℂ) |
| 18 | | pncan1 11687 |
. . . . . . 7
⊢ ((𝐾 · (2↑𝑁)) ∈ ℂ →
(((𝐾 · (2↑𝑁)) + 1) − 1) = (𝐾 · (2↑𝑁))) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐾 · (2↑𝑁)) + 1) − 1) = (𝐾 · (2↑𝑁))) |
| 20 | 19 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) = ((𝐾 · (2↑𝑁)) / 2)) |
| 21 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
| 23 | 2 | nnzd 12640 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 24 | 7 | nnzd 12640 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) |
| 25 | 22, 23, 24 | 3jca 1129 |
. . . . . . 7
⊢ (𝜑 → (2 ∈ ℤ ∧
𝐾 ∈ ℤ ∧
(2↑𝑁) ∈
ℤ)) |
| 26 | | iddvdsexp 16317 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℕ) → 2 ∥ (2↑𝑁)) |
| 27 | 22, 5, 26 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 2 ∥ (2↑𝑁)) |
| 28 | | dvdsmultr2 16335 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ ∧ (2↑𝑁) ∈ ℤ) → (2 ∥
(2↑𝑁) → 2 ∥
(𝐾 · (2↑𝑁)))) |
| 29 | 25, 27, 28 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 2 ∥ (𝐾 · (2↑𝑁))) |
| 30 | | nndivdvds 16299 |
. . . . . . 7
⊢ (((𝐾 · (2↑𝑁)) ∈ ℕ ∧ 2 ∈
ℕ) → (2 ∥ (𝐾 · (2↑𝑁)) ↔ ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ)) |
| 31 | 8, 4, 30 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (2 ∥ (𝐾 · (2↑𝑁)) ↔ ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ)) |
| 32 | 29, 31 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ) |
| 33 | 20, 32 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) ∈
ℕ) |
| 34 | 9, 16, 33 | 3jca 1129 |
. . 3
⊢ (𝜑 → (((𝐾 · (2↑𝑁)) + 1) ∈ ℕ ∧ 1 < ((𝐾 · (2↑𝑁)) + 1) ∧ ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) ∈
ℕ)) |
| 35 | | eleq1 2829 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 ∈ ℕ ↔ ((𝐾 · (2↑𝑁)) + 1) ∈ ℕ)) |
| 36 | | breq2 5147 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (1 < 𝑃 ↔ 1 < ((𝐾 · (2↑𝑁)) + 1))) |
| 37 | | oveq1 7438 |
. . . . . 6
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 − 1) = (((𝐾 · (2↑𝑁)) + 1) − 1)) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → ((𝑃 − 1) / 2) = ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2)) |
| 39 | 38 | eleq1d 2826 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (((𝑃 − 1) / 2) ∈ ℕ ↔
((((𝐾 ·
(2↑𝑁)) + 1) − 1)
/ 2) ∈ ℕ)) |
| 40 | 35, 36, 39 | 3anbi123d 1438 |
. . 3
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → ((𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) ↔
(((𝐾 · (2↑𝑁)) + 1) ∈ ℕ ∧ 1
< ((𝐾 ·
(2↑𝑁)) + 1) ∧
((((𝐾 ·
(2↑𝑁)) + 1) − 1)
/ 2) ∈ ℕ))) |
| 41 | 34, 40 | syl5ibrcom 247 |
. 2
⊢ (𝜑 → (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ))) |
| 42 | 1, 41 | mpd 15 |
1
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ)) |