Proof of Theorem proththdlem
Step | Hyp | Ref
| Expression |
1 | | proththd.p |
. 2
⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) |
2 | | proththd.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
3 | | 2nn 11062 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℕ) |
5 | | proththd.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 5 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 4, 6 | nnexpcld 12892 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
8 | 2, 7 | nnmulcld 10945 |
. . . . 5
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℕ) |
9 | 8 | peano2nnd 10914 |
. . . 4
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) ∈ ℕ) |
10 | | 1m1e0 10966 |
. . . . . 6
⊢ (1
− 1) = 0 |
11 | 8 | nngt0d 10941 |
. . . . . 6
⊢ (𝜑 → 0 < (𝐾 · (2↑𝑁))) |
12 | 10, 11 | syl5eqbr 4618 |
. . . . 5
⊢ (𝜑 → (1 − 1) < (𝐾 · (2↑𝑁))) |
13 | | 1red 9934 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
14 | 8 | nnred 10912 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℝ) |
15 | 13, 13, 14 | ltsubaddd 10502 |
. . . . 5
⊢ (𝜑 → ((1 − 1) < (𝐾 · (2↑𝑁)) ↔ 1 < ((𝐾 · (2↑𝑁)) + 1))) |
16 | 12, 15 | mpbid 221 |
. . . 4
⊢ (𝜑 → 1 < ((𝐾 · (2↑𝑁)) + 1)) |
17 | 8 | nncnd 10913 |
. . . . . . 7
⊢ (𝜑 → (𝐾 · (2↑𝑁)) ∈ ℂ) |
18 | | pncan1 10333 |
. . . . . . 7
⊢ ((𝐾 · (2↑𝑁)) ∈ ℂ →
(((𝐾 · (2↑𝑁)) + 1) − 1) = (𝐾 · (2↑𝑁))) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐾 · (2↑𝑁)) + 1) − 1) = (𝐾 · (2↑𝑁))) |
20 | 19 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) = ((𝐾 · (2↑𝑁)) / 2)) |
21 | | 2z 11286 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
23 | 2 | nnzd 11357 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
24 | 7 | nnzd 11357 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) |
25 | 22, 23, 24 | 3jca 1235 |
. . . . . . 7
⊢ (𝜑 → (2 ∈ ℤ ∧
𝐾 ∈ ℤ ∧
(2↑𝑁) ∈
ℤ)) |
26 | | iddvdsexp 14843 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℕ) → 2 ∥ (2↑𝑁)) |
27 | 22, 5, 26 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 2 ∥ (2↑𝑁)) |
28 | | dvdsmultr2 14859 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ ∧ (2↑𝑁) ∈ ℤ) → (2 ∥
(2↑𝑁) → 2 ∥
(𝐾 · (2↑𝑁)))) |
29 | 25, 27, 28 | sylc 63 |
. . . . . 6
⊢ (𝜑 → 2 ∥ (𝐾 · (2↑𝑁))) |
30 | | nndivdvds 14827 |
. . . . . . 7
⊢ (((𝐾 · (2↑𝑁)) ∈ ℕ ∧ 2 ∈
ℕ) → (2 ∥ (𝐾 · (2↑𝑁)) ↔ ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ)) |
31 | 8, 4, 30 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (2 ∥ (𝐾 · (2↑𝑁)) ↔ ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ)) |
32 | 29, 31 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) / 2) ∈ ℕ) |
33 | 20, 32 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) ∈
ℕ) |
34 | 9, 16, 33 | 3jca 1235 |
. . 3
⊢ (𝜑 → (((𝐾 · (2↑𝑁)) + 1) ∈ ℕ ∧ 1 < ((𝐾 · (2↑𝑁)) + 1) ∧ ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2) ∈
ℕ)) |
35 | | eleq1 2676 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 ∈ ℕ ↔ ((𝐾 · (2↑𝑁)) + 1) ∈ ℕ)) |
36 | | breq2 4587 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (1 < 𝑃 ↔ 1 < ((𝐾 · (2↑𝑁)) + 1))) |
37 | | oveq1 6556 |
. . . . . 6
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 − 1) = (((𝐾 · (2↑𝑁)) + 1) − 1)) |
38 | 37 | oveq1d 6564 |
. . . . 5
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → ((𝑃 − 1) / 2) = ((((𝐾 · (2↑𝑁)) + 1) − 1) / 2)) |
39 | 38 | eleq1d 2672 |
. . . 4
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (((𝑃 − 1) / 2) ∈ ℕ ↔
((((𝐾 ·
(2↑𝑁)) + 1) − 1)
/ 2) ∈ ℕ)) |
40 | 35, 36, 39 | 3anbi123d 1391 |
. . 3
⊢ (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → ((𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) ↔
(((𝐾 · (2↑𝑁)) + 1) ∈ ℕ ∧ 1
< ((𝐾 ·
(2↑𝑁)) + 1) ∧
((((𝐾 ·
(2↑𝑁)) + 1) − 1)
/ 2) ∈ ℕ))) |
41 | 34, 40 | syl5ibrcom 236 |
. 2
⊢ (𝜑 → (𝑃 = ((𝐾 · (2↑𝑁)) + 1) → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ))) |
42 | 1, 41 | mpd 15 |
1
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ)) |