Proof of Theorem perfect1
| Step | Hyp | Ref
| Expression |
| 1 | | mersenne 27271 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℙ) |
| 2 | | prmnn 16711 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ) |
| 4 | | 1sgm2ppw 27244 |
. . . 4
⊢ (𝑃 ∈ ℕ → (1
σ (2↑(𝑃 −
1))) = ((2↑𝑃) −
1)) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ (2↑(𝑃 − 1))) = ((2↑𝑃) − 1)) |
| 6 | | 1sgmprm 27243 |
. . . . 5
⊢
(((2↑𝑃) −
1) ∈ ℙ → (1 σ ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) + 1)) |
| 7 | 6 | adantl 481 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) + 1)) |
| 8 | | 2nn 12339 |
. . . . . . 7
⊢ 2 ∈
ℕ |
| 9 | 3 | nnnn0d 12587 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ0) |
| 10 | | nnexpcl 14115 |
. . . . . . 7
⊢ ((2
∈ ℕ ∧ 𝑃
∈ ℕ0) → (2↑𝑃) ∈ ℕ) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℕ) |
| 12 | 11 | nncnd 12282 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℂ) |
| 13 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 14 | | npcan 11517 |
. . . . 5
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → (((2↑𝑃) − 1) + 1) = (2↑𝑃)) |
| 15 | 12, 13, 14 | sylancl 586 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) + 1) = (2↑𝑃)) |
| 16 | 7, 15 | eqtrd 2777 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑𝑃) − 1)) = (2↑𝑃)) |
| 17 | 5, 16 | oveq12d 7449 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((1 σ (2↑(𝑃 − 1))) · (1 σ
((2↑𝑃) − 1))) =
(((2↑𝑃) − 1)
· (2↑𝑃))) |
| 18 | 13 | a1i 11 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℂ) |
| 19 | | nnm1nn0 12567 |
. . . . 5
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 20 | 3, 19 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (𝑃
− 1) ∈ ℕ0) |
| 21 | | nnexpcl 14115 |
. . . 4
⊢ ((2
∈ ℕ ∧ (𝑃
− 1) ∈ ℕ0) → (2↑(𝑃 − 1)) ∈
ℕ) |
| 22 | 8, 20, 21 | sylancr 587 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑(𝑃 − 1)) ∈
ℕ) |
| 23 | | prmnn 16711 |
. . . 4
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℕ) |
| 24 | 23 | adantl 481 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℕ) |
| 25 | 22 | nnzd 12640 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑(𝑃 − 1)) ∈
ℤ) |
| 26 | | prmz 16712 |
. . . . . 6
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℤ) |
| 27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℤ) |
| 28 | 25, 27 | gcdcomd 16551 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) gcd ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) gcd (2↑(𝑃 − 1)))) |
| 29 | | iddvds 16307 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℤ → ((2↑𝑃) − 1) ∥ ((2↑𝑃) − 1)) |
| 30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∥ ((2↑𝑃) − 1)) |
| 31 | | prmuz2 16733 |
. . . . . . . . . 10
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
| 32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
| 33 | | eluz2gt1 12962 |
. . . . . . . . 9
⊢
(((2↑𝑃) −
1) ∈ (ℤ≥‘2) → 1 < ((2↑𝑃) − 1)) |
| 34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < ((2↑𝑃) − 1)) |
| 35 | | ndvdsp1 16448 |
. . . . . . . 8
⊢
((((2↑𝑃)
− 1) ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℕ ∧ 1 <
((2↑𝑃) − 1))
→ (((2↑𝑃) −
1) ∥ ((2↑𝑃)
− 1) → ¬ ((2↑𝑃) − 1) ∥ (((2↑𝑃) − 1) +
1))) |
| 36 | 27, 24, 34, 35 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ ((2↑𝑃) − 1) → ¬
((2↑𝑃) − 1)
∥ (((2↑𝑃)
− 1) + 1))) |
| 37 | 30, 36 | mpd 15 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ¬ ((2↑𝑃) − 1) ∥ (((2↑𝑃) − 1) +
1)) |
| 38 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 39 | 38 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ∈ ℤ) |
| 40 | | dvdsmultr1 16333 |
. . . . . . . 8
⊢
((((2↑𝑃)
− 1) ∈ ℤ ∧ (2↑(𝑃 − 1)) ∈ ℤ ∧ 2 ∈
ℤ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ ((2↑(𝑃 −
1)) · 2))) |
| 41 | 27, 25, 39, 40 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ ((2↑(𝑃 −
1)) · 2))) |
| 42 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 43 | | expm1t 14131 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 𝑃
∈ ℕ) → (2↑𝑃) = ((2↑(𝑃 − 1)) · 2)) |
| 44 | 42, 3, 43 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) = ((2↑(𝑃 − 1)) · 2)) |
| 45 | 15, 44 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) · 2) = (((2↑𝑃) − 1) +
1)) |
| 46 | 45 | breq2d 5155 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ ((2↑(𝑃 − 1)) · 2) ↔
((2↑𝑃) − 1)
∥ (((2↑𝑃)
− 1) + 1))) |
| 47 | 41, 46 | sylibd 239 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ (((2↑𝑃)
− 1) + 1))) |
| 48 | 37, 47 | mtod 198 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ¬ ((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1))) |
| 49 | | simpr 484 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℙ) |
| 50 | | coprm 16748 |
. . . . . 6
⊢
((((2↑𝑃)
− 1) ∈ ℙ ∧ (2↑(𝑃 − 1)) ∈ ℤ) → (¬
((2↑𝑃) − 1)
∥ (2↑(𝑃 −
1)) ↔ (((2↑𝑃)
− 1) gcd (2↑(𝑃
− 1))) = 1)) |
| 51 | 49, 25, 50 | syl2anc 584 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (¬ ((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) ↔
(((2↑𝑃) − 1) gcd
(2↑(𝑃 − 1))) =
1)) |
| 52 | 48, 51 | mpbid 232 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) gcd (2↑(𝑃 − 1))) = 1) |
| 53 | 28, 52 | eqtrd 2777 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) gcd ((2↑𝑃) − 1)) = 1) |
| 54 | | sgmmul 27245 |
. . 3
⊢ ((1
∈ ℂ ∧ ((2↑(𝑃 − 1)) ∈ ℕ ∧
((2↑𝑃) − 1)
∈ ℕ ∧ ((2↑(𝑃 − 1)) gcd ((2↑𝑃) − 1)) = 1)) → (1 σ
((2↑(𝑃 − 1))
· ((2↑𝑃)
− 1))) = ((1 σ (2↑(𝑃 − 1))) · (1 σ
((2↑𝑃) −
1)))) |
| 55 | 18, 22, 24, 53, 54 | syl13anc 1374 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((1 σ
(2↑(𝑃 − 1)))
· (1 σ ((2↑𝑃) − 1)))) |
| 56 | | subcl 11507 |
. . . 4
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → ((2↑𝑃) − 1) ∈
ℂ) |
| 57 | 12, 13, 56 | sylancl 586 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℂ) |
| 58 | 12, 57 | mulcomd 11282 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) · ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) · (2↑𝑃))) |
| 59 | 17, 55, 58 | 3eqtr4d 2787 |
1
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((2↑𝑃) · ((2↑𝑃) − 1))) |