Proof of Theorem perfect
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simplr 768 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 2 ∥ 𝑁) | 
| 2 |  | 2prm 16730 | . . . . . . . 8
⊢ 2 ∈
ℙ | 
| 3 |  | simpll 766 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℕ) | 
| 4 |  | pcelnn 16909 | . . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2 ∥ 𝑁)) | 
| 5 | 2, 3, 4 | sylancr 587 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2
∥ 𝑁)) | 
| 6 | 1, 5 | mpbird 257 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ) | 
| 7 | 6 | nnzd 12642 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℤ) | 
| 8 | 7 | peano2zd 12727 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) + 1) ∈
ℤ) | 
| 9 |  | pcdvds 16903 | . . . . . . . . 9
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) | 
| 10 | 2, 3, 9 | sylancr 587 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) | 
| 11 |  | 2nn 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℕ | 
| 12 | 6 | nnnn0d 12589 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ0) | 
| 13 |  | nnexpcl 14116 | . . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (2 pCnt 𝑁) ∈ ℕ0) →
(2↑(2 pCnt 𝑁)) ∈
ℕ) | 
| 14 | 11, 12, 13 | sylancr 587 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℕ) | 
| 15 |  | nndivdvds 16300 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (2↑(2
pCnt 𝑁)) ∈ ℕ)
→ ((2↑(2 pCnt 𝑁))
∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈
ℕ)) | 
| 16 | 3, 14, 15 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) ∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ)) | 
| 17 | 10, 16 | mpbid 232 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ) | 
| 18 |  | pcndvds2 16907 | . . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) | 
| 19 | 2, 3, 18 | sylancr 587 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) | 
| 20 |  | simpr 484 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ 𝑁) = (2 · 𝑁)) | 
| 21 |  | nncn 12275 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 22 | 21 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℂ) | 
| 23 | 14 | nncnd 12283 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℂ) | 
| 24 | 14 | nnne0d 12317 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ≠ 0) | 
| 25 | 22, 23, 24 | divcan2d 12046 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = 𝑁) | 
| 26 | 25 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (1 σ 𝑁)) | 
| 27 | 25 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 ·
((2↑(2 pCnt 𝑁))
· (𝑁 / (2↑(2
pCnt 𝑁))))) = (2 ·
𝑁)) | 
| 28 | 20, 26, 27 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (2 · ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))))) | 
| 29 | 6, 17, 19, 28 | perfectlem2 27275 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ ∧ (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1))) | 
| 30 | 29 | simprd 495 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1)) | 
| 31 | 29 | simpld 494 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ) | 
| 32 | 30, 31 | eqeltrrd 2841 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑((2 pCnt
𝑁) + 1)) − 1) ∈
ℙ) | 
| 33 | 6 | nncnd 12283 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℂ) | 
| 34 |  | ax-1cn 11214 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 35 |  | pncan 11515 | . . . . . . . . 9
⊢ (((2 pCnt
𝑁) ∈ ℂ ∧ 1
∈ ℂ) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt 𝑁)) | 
| 36 | 33, 34, 35 | sylancl 586 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt
𝑁)) | 
| 37 | 36 | eqcomd 2742 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) = (((2 pCnt 𝑁) + 1) − 1)) | 
| 38 | 37 | oveq2d 7448 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) | 
| 39 | 38, 30 | oveq12d 7450 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) | 
| 40 | 25, 39 | eqtr3d 2778 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) | 
| 41 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑𝑝) = (2↑((2 pCnt 𝑁) + 1))) | 
| 42 | 41 | oveq1d 7447 | . . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑𝑝) − 1) = ((2↑((2 pCnt 𝑁) + 1)) −
1)) | 
| 43 | 42 | eleq1d 2825 | . . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (((2↑𝑝) − 1) ∈ ℙ ↔
((2↑((2 pCnt 𝑁) + 1))
− 1) ∈ ℙ)) | 
| 44 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑝 − 1) = (((2 pCnt 𝑁) + 1) − 1)) | 
| 45 | 44 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑(𝑝 − 1)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) | 
| 46 | 45, 42 | oveq12d 7450 | . . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) = ((2↑(((2
pCnt 𝑁) + 1) − 1))
· ((2↑((2 pCnt 𝑁) + 1)) − 1))) | 
| 47 | 46 | eqeq2d 2747 | . . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) ↔ 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) ·
((2↑((2 pCnt 𝑁) + 1))
− 1)))) | 
| 48 | 43, 47 | anbi12d 632 | . . . . 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 3621 | . . . 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 412 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) → ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) | 
| 52 |  | perfect1 27273 | . . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = ((2↑𝑝) · ((2↑𝑝) − 1))) | 
| 53 |  | 2cn 12342 | . . . . . . . . 9
⊢ 2 ∈
ℂ | 
| 54 |  | mersenne 27272 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℙ) | 
| 55 |  | prmnn 16712 | . . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℕ) | 
| 57 |  | expm1t 14132 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝑝
∈ ℕ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) | 
| 58 | 53, 56, 57 | sylancr 587 | . . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) | 
| 59 |  | nnm1nn0 12569 | . . . . . . . . . . 11
⊢ (𝑝 ∈ ℕ → (𝑝 − 1) ∈
ℕ0) | 
| 60 | 56, 59 | syl 17 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑝
− 1) ∈ ℕ0) | 
| 61 |  | expcl 14121 | . . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝑝
− 1) ∈ ℕ0) → (2↑(𝑝 − 1)) ∈ ℂ) | 
| 62 | 53, 60, 61 | sylancr 587 | . . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑(𝑝 − 1)) ∈ ℂ) | 
| 63 |  | mulcom 11242 | . . . . . . . . 9
⊢
(((2↑(𝑝 −
1)) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) | 
| 64 | 62, 53, 63 | sylancl 586 | . . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) | 
| 65 | 58, 64 | eqtrd 2776 | . . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = (2 · (2↑(𝑝 − 1)))) | 
| 66 | 65 | oveq1d 7447 | . . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) · ((2↑𝑝) − 1)) = ((2 · (2↑(𝑝 − 1))) ·
((2↑𝑝) −
1))) | 
| 67 |  | 2cnd 12345 | . . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 2 ∈ ℂ) | 
| 68 |  | prmnn 16712 | . . . . . . . . 9
⊢
(((2↑𝑝) −
1) ∈ ℙ → ((2↑𝑝) − 1) ∈ ℕ) | 
| 69 | 68 | adantl 481 | . . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℕ) | 
| 70 | 69 | nncnd 12283 | . . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℂ) | 
| 71 | 67, 62, 70 | mulassd 11285 | . . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2 · (2↑(𝑝 − 1))) · ((2↑𝑝) − 1)) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) | 
| 72 | 52, 66, 71 | 3eqtrd 2780 | . . . . 5
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) | 
| 73 |  | oveq2 7440 | . . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (1 σ
𝑁) = (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) | 
| 74 |  | oveq2 7440 | . . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (2 ·
𝑁) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) | 
| 75 | 73, 74 | eqeq12d 2752 | . . . . 5
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → ((1 σ
𝑁) = (2 · 𝑁) ↔ (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1))) = (2 · ((2↑(𝑝 − 1)) · ((2↑𝑝) −
1))))) | 
| 76 | 72, 75 | syl5ibrcom 247 | . . . 4
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)) → (1 σ 𝑁) = (2 · 𝑁))) | 
| 77 | 76 | impr 454 | . . 3
⊢ ((𝑝 ∈ ℤ ∧
(((2↑𝑝) − 1)
∈ ℙ ∧ 𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) → (1 σ 𝑁) = (2 · 𝑁)) | 
| 78 | 77 | rexlimiva 3146 | . 2
⊢
(∃𝑝 ∈
ℤ (((2↑𝑝)
− 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) → (1 σ
𝑁) = (2 · 𝑁)) | 
| 79 | 51, 78 | impbid1 225 | 1
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) |