Proof of Theorem perfect
Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 2 ∥ 𝑁) |
2 | | 2prm 16133 |
. . . . . . . 8
⊢ 2 ∈
ℙ |
3 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℕ) |
4 | | pcelnn 16306 |
. . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2 ∥ 𝑁)) |
5 | 2, 3, 4 | sylancr 590 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2
∥ 𝑁)) |
6 | 1, 5 | mpbird 260 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ) |
7 | 6 | nnzd 12167 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℤ) |
8 | 7 | peano2zd 12171 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) + 1) ∈
ℤ) |
9 | | pcdvds 16300 |
. . . . . . . . 9
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) |
10 | 2, 3, 9 | sylancr 590 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) |
11 | | 2nn 11789 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
12 | 6 | nnnn0d 12036 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ0) |
13 | | nnexpcl 13534 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (2 pCnt 𝑁) ∈ ℕ0) →
(2↑(2 pCnt 𝑁)) ∈
ℕ) |
14 | 11, 12, 13 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℕ) |
15 | | nndivdvds 15708 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (2↑(2
pCnt 𝑁)) ∈ ℕ)
→ ((2↑(2 pCnt 𝑁))
∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈
ℕ)) |
16 | 3, 14, 15 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) ∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ)) |
17 | 10, 16 | mpbid 235 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ) |
18 | | pcndvds2 16304 |
. . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) |
19 | 2, 3, 18 | sylancr 590 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) |
20 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ 𝑁) = (2 · 𝑁)) |
21 | | nncn 11724 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | 21 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℂ) |
23 | 14 | nncnd 11732 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℂ) |
24 | 14 | nnne0d 11766 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ≠ 0) |
25 | 22, 23, 24 | divcan2d 11496 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = 𝑁) |
26 | 25 | oveq2d 7186 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (1 σ 𝑁)) |
27 | 25 | oveq2d 7186 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 ·
((2↑(2 pCnt 𝑁))
· (𝑁 / (2↑(2
pCnt 𝑁))))) = (2 ·
𝑁)) |
28 | 20, 26, 27 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (2 · ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))))) |
29 | 6, 17, 19, 28 | perfectlem2 25966 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ ∧ (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1))) |
30 | 29 | simprd 499 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1)) |
31 | 29 | simpld 498 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ) |
32 | 30, 31 | eqeltrrd 2834 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑((2 pCnt
𝑁) + 1)) − 1) ∈
ℙ) |
33 | 6 | nncnd 11732 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℂ) |
34 | | ax-1cn 10673 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
35 | | pncan 10970 |
. . . . . . . . 9
⊢ (((2 pCnt
𝑁) ∈ ℂ ∧ 1
∈ ℂ) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt 𝑁)) |
36 | 33, 34, 35 | sylancl 589 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt
𝑁)) |
37 | 36 | eqcomd 2744 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) = (((2 pCnt 𝑁) + 1) − 1)) |
38 | 37 | oveq2d 7186 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) |
39 | 38, 30 | oveq12d 7188 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) |
40 | 25, 39 | eqtr3d 2775 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) |
41 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑𝑝) = (2↑((2 pCnt 𝑁) + 1))) |
42 | 41 | oveq1d 7185 |
. . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑𝑝) − 1) = ((2↑((2 pCnt 𝑁) + 1)) −
1)) |
43 | 42 | eleq1d 2817 |
. . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (((2↑𝑝) − 1) ∈ ℙ ↔
((2↑((2 pCnt 𝑁) + 1))
− 1) ∈ ℙ)) |
44 | | oveq1 7177 |
. . . . . . . . 9
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑝 − 1) = (((2 pCnt 𝑁) + 1) − 1)) |
45 | 44 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑(𝑝 − 1)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) |
46 | 45, 42 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) = ((2↑(((2
pCnt 𝑁) + 1) − 1))
· ((2↑((2 pCnt 𝑁) + 1)) − 1))) |
47 | 46 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) ↔ 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) ·
((2↑((2 pCnt 𝑁) + 1))
− 1)))) |
48 | 43, 47 | anbi12d 634 |
. . . . 5
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((((2↑𝑝) − 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) ↔
(((2↑((2 pCnt 𝑁) + 1))
− 1) ∈ ℙ ∧ 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))))) |
49 | 48 | rspcev 3526 |
. . . 4
⊢ ((((2
pCnt 𝑁) + 1) ∈ ℤ
∧ (((2↑((2 pCnt 𝑁)
+ 1)) − 1) ∈ ℙ ∧ 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) − 1))))
→ ∃𝑝 ∈
ℤ (((2↑𝑝)
− 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)))) |
50 | 8, 32, 40, 49 | syl12anc 836 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1)))) |
51 | 50 | ex 416 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) → ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) |
52 | | perfect1 25964 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = ((2↑𝑝) · ((2↑𝑝) − 1))) |
53 | | 2cn 11791 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
54 | | mersenne 25963 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℙ) |
55 | | prmnn 16115 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℕ) |
57 | | expm1t 13549 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝑝
∈ ℕ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) |
58 | 53, 56, 57 | sylancr 590 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) |
59 | | nnm1nn0 12017 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℕ → (𝑝 − 1) ∈
ℕ0) |
60 | 56, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑝
− 1) ∈ ℕ0) |
61 | | expcl 13539 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝑝
− 1) ∈ ℕ0) → (2↑(𝑝 − 1)) ∈ ℂ) |
62 | 53, 60, 61 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑(𝑝 − 1)) ∈ ℂ) |
63 | | mulcom 10701 |
. . . . . . . . 9
⊢
(((2↑(𝑝 −
1)) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) |
64 | 62, 53, 63 | sylancl 589 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) |
65 | 58, 64 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = (2 · (2↑(𝑝 − 1)))) |
66 | 65 | oveq1d 7185 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) · ((2↑𝑝) − 1)) = ((2 · (2↑(𝑝 − 1))) ·
((2↑𝑝) −
1))) |
67 | | 2cnd 11794 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 2 ∈ ℂ) |
68 | | prmnn 16115 |
. . . . . . . . 9
⊢
(((2↑𝑝) −
1) ∈ ℙ → ((2↑𝑝) − 1) ∈ ℕ) |
69 | 68 | adantl 485 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℕ) |
70 | 69 | nncnd 11732 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℂ) |
71 | 67, 62, 70 | mulassd 10742 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2 · (2↑(𝑝 − 1))) · ((2↑𝑝) − 1)) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
72 | 52, 66, 71 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
73 | | oveq2 7178 |
. . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (1 σ
𝑁) = (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
74 | | oveq2 7178 |
. . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (2 ·
𝑁) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
75 | 73, 74 | eqeq12d 2754 |
. . . . 5
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → ((1 σ
𝑁) = (2 · 𝑁) ↔ (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1))) = (2 · ((2↑(𝑝 − 1)) · ((2↑𝑝) −
1))))) |
76 | 72, 75 | syl5ibrcom 250 |
. . . 4
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)) → (1 σ 𝑁) = (2 · 𝑁))) |
77 | 76 | impr 458 |
. . 3
⊢ ((𝑝 ∈ ℤ ∧
(((2↑𝑝) − 1)
∈ ℙ ∧ 𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) → (1 σ 𝑁) = (2 · 𝑁)) |
78 | 77 | rexlimiva 3191 |
. 2
⊢
(∃𝑝 ∈
ℤ (((2↑𝑝)
− 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) → (1 σ
𝑁) = (2 · 𝑁)) |
79 | 51, 78 | impbid1 228 |
1
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) |