| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℤ) |
| 2 | | 2nn0 12543 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
| 3 | 2 | numexp1 17114 |
. . . . . 6
⊢
(2↑1) = 2 |
| 4 | | df-2 12329 |
. . . . . 6
⊢ 2 = (1 +
1) |
| 5 | 3, 4 | eqtri 2765 |
. . . . 5
⊢
(2↑1) = (1 + 1) |
| 6 | | prmuz2 16733 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
| 8 | | eluz2gt1 12962 |
. . . . . . 7
⊢
(((2↑𝑃) −
1) ∈ (ℤ≥‘2) → 1 < ((2↑𝑃) − 1)) |
| 9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < ((2↑𝑃) − 1)) |
| 10 | | 1red 11262 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℝ) |
| 11 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 12 | 11 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ∈ ℝ) |
| 13 | | 2ne0 12370 |
. . . . . . . . 9
⊢ 2 ≠
0 |
| 14 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ≠ 0) |
| 15 | 12, 14, 1 | reexpclzd 14288 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℝ) |
| 16 | 10, 10, 15 | ltaddsubd 11863 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((1 + 1) < (2↑𝑃) ↔ 1 < ((2↑𝑃) − 1))) |
| 17 | 9, 16 | mpbird 257 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 + 1) < (2↑𝑃)) |
| 18 | 5, 17 | eqbrtrid 5178 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑1) < (2↑𝑃)) |
| 19 | | 1zzd 12648 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℤ) |
| 20 | | 1lt2 12437 |
. . . . . 6
⊢ 1 <
2 |
| 21 | 20 | a1i 11 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < 2) |
| 22 | 12, 19, 1, 21 | ltexp2d 14290 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 < 𝑃 ↔ (2↑1) < (2↑𝑃))) |
| 23 | 18, 22 | mpbird 257 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < 𝑃) |
| 24 | | eluz2b1 12961 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℤ ∧ 1 < 𝑃)) |
| 25 | 1, 23, 24 | sylanbrc 583 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ (ℤ≥‘2)) |
| 26 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℙ) |
| 27 | | prmnn 16711 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℕ) |
| 28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℕ) |
| 29 | 28 | nncnd 12282 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℂ) |
| 30 | | 2nn 12339 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
| 31 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈
(ℤ≥‘2)) |
| 32 | 31 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈
(ℤ≥‘2)) |
| 33 | | eluz2nn 12924 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ) |
| 35 | 34 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ0) |
| 36 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) |
| 37 | 30, 35, 36 | sylancr 587 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℕ) |
| 38 | 37 | nnzd 12640 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℤ) |
| 39 | | peano2zm 12660 |
. . . . . . . . 9
⊢
((2↑𝑘) ∈
ℤ → ((2↑𝑘)
− 1) ∈ ℤ) |
| 40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℤ) |
| 41 | 40 | zred 12722 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℝ) |
| 42 | 41 | recnd 11289 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℂ) |
| 43 | | 0red 11264 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 ∈
ℝ) |
| 44 | | 1red 11262 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 ∈
ℝ) |
| 45 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 46 | 45 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 <
1) |
| 47 | | eluz2gt1 12962 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘2) → 1 < 𝑘) |
| 48 | 32, 47 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < 𝑘) |
| 49 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 2 ∈
ℝ) |
| 50 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 ∈
ℤ) |
| 51 | | elfzelz 13564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈ ℤ) |
| 52 | 51 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℤ) |
| 53 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 <
2) |
| 54 | 49, 50, 52, 53 | ltexp2d 14290 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 < 𝑘 ↔ (2↑1) <
(2↑𝑘))) |
| 55 | 48, 54 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑1) <
(2↑𝑘)) |
| 56 | 5, 55 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 + 1) <
(2↑𝑘)) |
| 57 | 37 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℝ) |
| 58 | 44, 44, 57 | ltaddsubd 11863 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((1 + 1) <
(2↑𝑘) ↔ 1 <
((2↑𝑘) −
1))) |
| 59 | 56, 58 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < ((2↑𝑘) − 1)) |
| 60 | 43, 44, 41, 46, 59 | lttrd 11422 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 0 < ((2↑𝑘) − 1)) |
| 61 | | elnnz 12623 |
. . . . . . . 8
⊢
(((2↑𝑘) −
1) ∈ ℕ ↔ (((2↑𝑘) − 1) ∈ ℤ ∧ 0 <
((2↑𝑘) −
1))) |
| 62 | 40, 60, 61 | sylanbrc 583 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
ℕ) |
| 63 | 62 | nnne0d 12316 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ≠
0) |
| 64 | 29, 42, 63 | divcan2d 12045 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1))) =
((2↑𝑃) −
1)) |
| 65 | 64, 26 | eqeltrd 2841 |
. . . 4
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1)))
∈ ℙ) |
| 66 | | eluz2b2 12963 |
. . . . . 6
⊢
(((2↑𝑘) −
1) ∈ (ℤ≥‘2) ↔ (((2↑𝑘) − 1) ∈ ℕ ∧ 1 <
((2↑𝑘) −
1))) |
| 67 | 62, 59, 66 | sylanbrc 583 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈
(ℤ≥‘2)) |
| 68 | 37 | nncnd 12282 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈
ℂ) |
| 69 | | ax-1cn 11213 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
| 70 | | subeq0 11535 |
. . . . . . . . . . . 12
⊢
(((2↑𝑘) ∈
ℂ ∧ 1 ∈ ℂ) → (((2↑𝑘) − 1) = 0 ↔ (2↑𝑘) = 1)) |
| 71 | 68, 69, 70 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) = 0 ↔
(2↑𝑘) =
1)) |
| 72 | 71 | necon3bid 2985 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) ≠ 0 ↔
(2↑𝑘) ≠
1)) |
| 73 | 63, 72 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ≠ 1) |
| 74 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∥ 𝑃) |
| 75 | | eluz2nn 12924 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
| 76 | 25, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ) |
| 77 | 76 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℕ) |
| 78 | | nndivdvds 16299 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ)) |
| 79 | 77, 34, 78 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ)) |
| 80 | 74, 79 | mpbid 232 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈ ℕ) |
| 81 | 80 | nnnn0d 12587 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈
ℕ0) |
| 82 | 68, 73, 81 | geoser 15903 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = ((1 − ((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘)))) |
| 83 | 15 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈
ℝ) |
| 84 | 83 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈
ℂ) |
| 85 | | negsubdi2 11568 |
. . . . . . . . . . 11
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → -((2↑𝑃) − 1) = (1 − (2↑𝑃))) |
| 86 | 84, 69, 85 | sylancl 586 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 −
(2↑𝑃))) |
| 87 | 77 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℂ) |
| 88 | 34 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℂ) |
| 89 | 34 | nnne0d 12316 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 ≠ 0) |
| 90 | 87, 88, 89 | divcan2d 12045 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 · (𝑃 / 𝑘)) = 𝑃) |
| 91 | 90 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = (2↑𝑃)) |
| 92 | 49 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 2 ∈
ℂ) |
| 93 | 92, 81, 35 | expmuld 14189 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = ((2↑𝑘)↑(𝑃 / 𝑘))) |
| 94 | 91, 93 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑃) = ((2↑𝑘)↑(𝑃 / 𝑘))) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 −
(2↑𝑃)) = (1 −
((2↑𝑘)↑(𝑃 / 𝑘)))) |
| 96 | 86, 95 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 −
((2↑𝑘)↑(𝑃 / 𝑘)))) |
| 97 | | negsubdi2 11568 |
. . . . . . . . . 10
⊢
(((2↑𝑘) ∈
ℂ ∧ 1 ∈ ℂ) → -((2↑𝑘) − 1) = (1 − (2↑𝑘))) |
| 98 | 68, 69, 97 | sylancl 586 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → -((2↑𝑘) − 1) = (1 −
(2↑𝑘))) |
| 99 | 96, 98 | oveq12d 7449 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = ((1 −
((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘)))) |
| 100 | 29, 42, 63 | div2negd 12058 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
| 101 | 82, 99, 100 | 3eqtr2d 2783 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
| 102 | | fzfid 14014 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (0...((𝑃 / 𝑘) − 1)) ∈ Fin) |
| 103 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...((𝑃 / 𝑘) − 1)) → 𝑛 ∈ ℕ0) |
| 104 | | zexpcl 14117 |
. . . . . . . . 9
⊢
(((2↑𝑘) ∈
ℤ ∧ 𝑛 ∈
ℕ0) → ((2↑𝑘)↑𝑛) ∈ ℤ) |
| 105 | 38, 103, 104 | syl2an 596 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℤ ∧ ((2↑𝑃)
− 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) ∧ 𝑛 ∈ (0...((𝑃 / 𝑘) − 1))) → ((2↑𝑘)↑𝑛) ∈ ℤ) |
| 106 | 102, 105 | fsumzcl 15771 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) ∈ ℤ) |
| 107 | 101, 106 | eqeltrrd 2842 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
ℤ) |
| 108 | 42 | mullidd 11279 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 ·
((2↑𝑘) − 1)) =
((2↑𝑘) −
1)) |
| 109 | | 2z 12649 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
| 110 | | elfzm11 13635 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝑃
∈ ℤ) → (𝑘
∈ (2...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
| 111 | 109, 1, 110 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (𝑘
∈ (2...(𝑃 − 1))
↔ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃))) |
| 112 | 111 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ (𝑘 ∈ ℤ
∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃)) |
| 113 | 112 | simp3d 1145 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ 𝑘 < 𝑃) |
| 114 | 113 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑘 < 𝑃) |
| 115 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℤ) |
| 116 | 49, 52, 115, 53 | ltexp2d 14290 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (𝑘 < 𝑃 ↔ (2↑𝑘) < (2↑𝑃))) |
| 117 | 114, 116 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (2↑𝑘) < (2↑𝑃)) |
| 118 | 57, 83, 44, 117 | ltsub1dd 11875 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) < ((2↑𝑃) − 1)) |
| 119 | 108, 118 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) −
1)) |
| 120 | 28 | nnred 12281 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈
ℝ) |
| 121 | | ltmuldiv 12141 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ ((2↑𝑃) − 1) ∈ ℝ ∧
(((2↑𝑘) − 1)
∈ ℝ ∧ 0 < ((2↑𝑘) − 1))) → ((1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) − 1)
↔ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
| 122 | 44, 120, 41, 60, 121 | syl112anc 1376 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ((1 ·
((2↑𝑘) − 1))
< ((2↑𝑃) − 1)
↔ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
| 123 | 119, 122 | mpbid 232 |
. . . . . 6
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) |
| 124 | | eluz2b1 12961 |
. . . . . 6
⊢
((((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)) ∈ (ℤ≥‘2) ↔ ((((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ ℤ
∧ 1 < (((2↑𝑃)
− 1) / ((2↑𝑘)
− 1)))) |
| 125 | 107, 123,
124 | sylanbrc 583 |
. . . . 5
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
(ℤ≥‘2)) |
| 126 | | nprm 16725 |
. . . . 5
⊢
((((2↑𝑘)
− 1) ∈ (ℤ≥‘2) ∧ (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈
(ℤ≥‘2)) → ¬ (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) ∈
ℙ) |
| 127 | 67, 125, 126 | syl2anc 584 |
. . . 4
⊢ ((((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
∧ 𝑘 ∥ 𝑃) → ¬ (((2↑𝑘) − 1) ·
(((2↑𝑃) − 1) /
((2↑𝑘) − 1)))
∈ ℙ) |
| 128 | 65, 127 | pm2.65da 817 |
. . 3
⊢ (((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) ∧ 𝑘
∈ (2...(𝑃 − 1)))
→ ¬ 𝑘 ∥
𝑃) |
| 129 | 128 | ralrimiva 3146 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃) |
| 130 | | isprm3 16720 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃)) |
| 131 | 25, 129, 130 | sylanbrc 583 |
1
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℙ) |