Proof of Theorem perfect1
Step | Hyp | Ref
| Expression |
1 | | mersenne 26375 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℙ) |
2 | | prmnn 16379 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ) |
4 | | 1sgm2ppw 26348 |
. . . 4
⊢ (𝑃 ∈ ℕ → (1
σ (2↑(𝑃 −
1))) = ((2↑𝑃) −
1)) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ (2↑(𝑃 − 1))) = ((2↑𝑃) − 1)) |
6 | | 1sgmprm 26347 |
. . . . 5
⊢
(((2↑𝑃) −
1) ∈ ℙ → (1 σ ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) + 1)) |
7 | 6 | adantl 482 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) + 1)) |
8 | | 2nn 12046 |
. . . . . . 7
⊢ 2 ∈
ℕ |
9 | 3 | nnnn0d 12293 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 𝑃
∈ ℕ0) |
10 | | nnexpcl 13795 |
. . . . . . 7
⊢ ((2
∈ ℕ ∧ 𝑃
∈ ℕ0) → (2↑𝑃) ∈ ℕ) |
11 | 8, 9, 10 | sylancr 587 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℕ) |
12 | 11 | nncnd 11989 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) ∈ ℂ) |
13 | | ax-1cn 10929 |
. . . . 5
⊢ 1 ∈
ℂ |
14 | | npcan 11230 |
. . . . 5
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → (((2↑𝑃) − 1) + 1) = (2↑𝑃)) |
15 | 12, 13, 14 | sylancl 586 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) + 1) = (2↑𝑃)) |
16 | 7, 15 | eqtrd 2778 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑𝑃) − 1)) = (2↑𝑃)) |
17 | 5, 16 | oveq12d 7293 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((1 σ (2↑(𝑃 − 1))) · (1 σ
((2↑𝑃) − 1))) =
(((2↑𝑃) − 1)
· (2↑𝑃))) |
18 | 13 | a1i 11 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 ∈ ℂ) |
19 | | nnm1nn0 12274 |
. . . . 5
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
20 | 3, 19 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (𝑃
− 1) ∈ ℕ0) |
21 | | nnexpcl 13795 |
. . . 4
⊢ ((2
∈ ℕ ∧ (𝑃
− 1) ∈ ℕ0) → (2↑(𝑃 − 1)) ∈
ℕ) |
22 | 8, 20, 21 | sylancr 587 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑(𝑃 − 1)) ∈
ℕ) |
23 | | prmnn 16379 |
. . . 4
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℕ) |
24 | 23 | adantl 482 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℕ) |
25 | 22 | nnzd 12425 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑(𝑃 − 1)) ∈
ℤ) |
26 | | prmz 16380 |
. . . . . 6
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
ℤ) |
27 | 26 | adantl 482 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℤ) |
28 | 25, 27 | gcdcomd 16221 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) gcd ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) gcd (2↑(𝑃 − 1)))) |
29 | | iddvds 15979 |
. . . . . . . 8
⊢
(((2↑𝑃) −
1) ∈ ℤ → ((2↑𝑃) − 1) ∥ ((2↑𝑃) − 1)) |
30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∥ ((2↑𝑃) − 1)) |
31 | | prmuz2 16401 |
. . . . . . . . . 10
⊢
(((2↑𝑃) −
1) ∈ ℙ → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
32 | 31 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
(ℤ≥‘2)) |
33 | | eluz2gt1 12660 |
. . . . . . . . 9
⊢
(((2↑𝑃) −
1) ∈ (ℤ≥‘2) → 1 < ((2↑𝑃) − 1)) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 1 < ((2↑𝑃) − 1)) |
35 | | ndvdsp1 16120 |
. . . . . . . 8
⊢
((((2↑𝑃)
− 1) ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℕ ∧ 1 <
((2↑𝑃) − 1))
→ (((2↑𝑃) −
1) ∥ ((2↑𝑃)
− 1) → ¬ ((2↑𝑃) − 1) ∥ (((2↑𝑃) − 1) +
1))) |
36 | 27, 24, 34, 35 | syl3anc 1370 |
. . . . . . 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 12352 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → 2 ∈ ℤ) |
40 | | dvdsmultr1 16005 |
. . . . . . . 8
⊢
((((2↑𝑃)
− 1) ∈ ℤ ∧ (2↑(𝑃 − 1)) ∈ ℤ ∧ 2 ∈
ℤ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ ((2↑(𝑃 −
1)) · 2))) |
41 | 27, 25, 39, 40 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ ((2↑(𝑃 −
1)) · 2))) |
42 | | 2cn 12048 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
43 | | expm1t 13811 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 𝑃
∈ ℕ) → (2↑𝑃) = ((2↑(𝑃 − 1)) · 2)) |
44 | 42, 3, 43 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (2↑𝑃) = ((2↑(𝑃 − 1)) · 2)) |
45 | 15, 44 | eqtr2d 2779 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) · 2) = (((2↑𝑃) − 1) +
1)) |
46 | 45 | breq2d 5086 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ ((2↑(𝑃 − 1)) · 2) ↔
((2↑𝑃) − 1)
∥ (((2↑𝑃)
− 1) + 1))) |
47 | 41, 46 | sylibd 238 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1)) →
((2↑𝑃) − 1)
∥ (((2↑𝑃)
− 1) + 1))) |
48 | 37, 47 | mtod 197 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ¬ ((2↑𝑃) − 1) ∥ (2↑(𝑃 − 1))) |
49 | | simpr 485 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℙ) |
50 | | coprm 16416 |
. . . . . 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 231 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (((2↑𝑃) − 1) gcd (2↑(𝑃 − 1))) = 1) |
53 | 28, 52 | eqtrd 2778 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑(𝑃 − 1)) gcd ((2↑𝑃) − 1)) = 1) |
54 | | sgmmul 26349 |
. . 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 1371 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((1 σ
(2↑(𝑃 − 1)))
· (1 σ ((2↑𝑃) − 1)))) |
56 | | subcl 11220 |
. . . 4
⊢
(((2↑𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → ((2↑𝑃) − 1) ∈
ℂ) |
57 | 12, 13, 56 | sylancl 586 |
. . 3
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) − 1) ∈
ℂ) |
58 | 12, 57 | mulcomd 10996 |
. 2
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → ((2↑𝑃) · ((2↑𝑃) − 1)) = (((2↑𝑃) − 1) · (2↑𝑃))) |
59 | 17, 55, 58 | 3eqtr4d 2788 |
1
⊢ ((𝑃 ∈ ℤ ∧
((2↑𝑃) − 1)
∈ ℙ) → (1 σ ((2↑(𝑃 − 1)) · ((2↑𝑃) − 1))) = ((2↑𝑃) · ((2↑𝑃) − 1))) |