Proof of Theorem perfect
Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 2 ∥ 𝑁) |
2 | | 2prm 15405 |
. . . . . . . 8
⊢ 2 ∈
ℙ |
3 | | simpll 790 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℕ) |
4 | | pcelnn 15574 |
. . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2 ∥ 𝑁)) |
5 | 2, 3, 4 | sylancr 695 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) ∈ ℕ ↔ 2
∥ 𝑁)) |
6 | 1, 5 | mpbird 247 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ) |
7 | 6 | nnzd 11481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℤ) |
8 | 7 | peano2zd 11485 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2 pCnt 𝑁) + 1) ∈
ℤ) |
9 | | pcdvds 15568 |
. . . . . . . . 9
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) |
10 | 2, 3, 9 | sylancr 695 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∥ 𝑁) |
11 | | 2nn 11185 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
12 | 6 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℕ0) |
13 | | nnexpcl 12873 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (2 pCnt 𝑁) ∈ ℕ0) →
(2↑(2 pCnt 𝑁)) ∈
ℕ) |
14 | 11, 12, 13 | sylancr 695 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℕ) |
15 | | nndivdvds 14989 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (2↑(2
pCnt 𝑁)) ∈ ℕ)
→ ((2↑(2 pCnt 𝑁))
∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈
ℕ)) |
16 | 3, 14, 15 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) ∥ 𝑁 ↔ (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ)) |
17 | 10, 16 | mpbid 222 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℕ) |
18 | | pcndvds2 15572 |
. . . . . . . 8
⊢ ((2
∈ ℙ ∧ 𝑁
∈ ℕ) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) |
19 | 2, 3, 18 | sylancr 695 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ¬ 2 ∥ (𝑁 / (2↑(2 pCnt 𝑁)))) |
20 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ 𝑁) = (2 · 𝑁)) |
21 | | nncn 11028 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | 21 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 ∈ ℂ) |
23 | 14 | nncnd 11036 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ∈
ℂ) |
24 | 14 | nnne0d 11065 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) ≠ 0) |
25 | 22, 23, 24 | divcan2d 10803 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = 𝑁) |
26 | 25 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (1 σ 𝑁)) |
27 | 25 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 ·
((2↑(2 pCnt 𝑁))
· (𝑁 / (2↑(2
pCnt 𝑁))))) = (2 ·
𝑁)) |
28 | 20, 26, 27 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (1 σ ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁))))) = (2 · ((2↑(2
pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))))) |
29 | 6, 17, 19, 28 | perfectlem2 24955 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ ∧ (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1))) |
30 | 29 | simprd 479 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) = ((2↑((2 pCnt 𝑁) + 1)) − 1)) |
31 | 29 | simpld 475 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (𝑁 / (2↑(2 pCnt 𝑁))) ∈ ℙ) |
32 | 30, 31 | eqeltrrd 2702 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑((2 pCnt
𝑁) + 1)) − 1) ∈
ℙ) |
33 | 6 | nncnd 11036 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) ∈
ℂ) |
34 | | ax-1cn 9994 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
35 | | pncan 10287 |
. . . . . . . . 9
⊢ (((2 pCnt
𝑁) ∈ ℂ ∧ 1
∈ ℂ) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt 𝑁)) |
36 | 33, 34, 35 | sylancl 694 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (((2 pCnt 𝑁) + 1) − 1) = (2 pCnt
𝑁)) |
37 | 36 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2 pCnt 𝑁) = (((2 pCnt 𝑁) + 1) − 1)) |
38 | 37 | oveq2d 6666 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → (2↑(2 pCnt 𝑁)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) |
39 | 38, 30 | oveq12d 6668 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ((2↑(2 pCnt 𝑁)) · (𝑁 / (2↑(2 pCnt 𝑁)))) = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) |
40 | 25, 39 | eqtr3d 2658 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) · ((2↑((2
pCnt 𝑁) + 1)) −
1))) |
41 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑𝑝) = (2↑((2 pCnt 𝑁) + 1))) |
42 | 41 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑𝑝) − 1) = ((2↑((2 pCnt 𝑁) + 1)) −
1)) |
43 | 42 | eleq1d 2686 |
. . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (((2↑𝑝) − 1) ∈ ℙ ↔
((2↑((2 pCnt 𝑁) + 1))
− 1) ∈ ℙ)) |
44 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑝 − 1) = (((2 pCnt 𝑁) + 1) − 1)) |
45 | 44 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (2↑(𝑝 − 1)) = (2↑(((2 pCnt 𝑁) + 1) −
1))) |
46 | 45, 42 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) = ((2↑(((2
pCnt 𝑁) + 1) − 1))
· ((2↑((2 pCnt 𝑁) + 1)) − 1))) |
47 | 46 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑝 = ((2 pCnt 𝑁) + 1) → (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) ↔ 𝑁 = ((2↑(((2 pCnt 𝑁) + 1) − 1)) ·
((2↑((2 pCnt 𝑁) + 1))
− 1)))) |
48 | 43, 47 | anbi12d 747 |
. . . . 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 3309 |
. . . 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 1324 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) ∧ (1 σ 𝑁) = (2 · 𝑁)) → ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1)))) |
51 | 50 | ex 450 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) → ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) |
52 | | perfect1 24953 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = ((2↑𝑝) · ((2↑𝑝) − 1))) |
53 | | 2cn 11091 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
54 | | mersenne 24952 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℙ) |
55 | | prmnn 15388 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 𝑝
∈ ℕ) |
57 | | expm1t 12888 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝑝
∈ ℕ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) |
58 | 53, 56, 57 | sylancr 695 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = ((2↑(𝑝 − 1)) · 2)) |
59 | | nnm1nn0 11334 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℕ → (𝑝 − 1) ∈
ℕ0) |
60 | 56, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑝
− 1) ∈ ℕ0) |
61 | | expcl 12878 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝑝
− 1) ∈ ℕ0) → (2↑(𝑝 − 1)) ∈ ℂ) |
62 | 53, 60, 61 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑(𝑝 − 1)) ∈ ℂ) |
63 | | mulcom 10022 |
. . . . . . . . 9
⊢
(((2↑(𝑝 −
1)) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) |
64 | 62, 53, 63 | sylancl 694 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑(𝑝 − 1)) · 2) = (2 ·
(2↑(𝑝 −
1)))) |
65 | 58, 64 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (2↑𝑝) = (2 · (2↑(𝑝 − 1)))) |
66 | 65 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) · ((2↑𝑝) − 1)) = ((2 · (2↑(𝑝 − 1))) ·
((2↑𝑝) −
1))) |
67 | | 2cnd 11093 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → 2 ∈ ℂ) |
68 | | prmnn 15388 |
. . . . . . . . 9
⊢
(((2↑𝑝) −
1) ∈ ℙ → ((2↑𝑝) − 1) ∈ ℕ) |
69 | 68 | adantl 482 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℕ) |
70 | 69 | nncnd 11036 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2↑𝑝) − 1) ∈ ℂ) |
71 | 67, 62, 70 | mulassd 10063 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → ((2 · (2↑(𝑝 − 1))) · ((2↑𝑝) − 1)) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
72 | 52, 66, 71 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (1 σ ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
73 | | oveq2 6658 |
. . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (1 σ
𝑁) = (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
74 | | oveq2 6658 |
. . . . . 6
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → (2 ·
𝑁) = (2 ·
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) |
75 | 73, 74 | eqeq12d 2637 |
. . . . 5
⊢ (𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1)) → ((1 σ
𝑁) = (2 · 𝑁) ↔ (1 σ
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1))) = (2 · ((2↑(𝑝 − 1)) · ((2↑𝑝) −
1))))) |
76 | 72, 75 | syl5ibrcom 237 |
. . . 4
⊢ ((𝑝 ∈ ℤ ∧
((2↑𝑝) − 1)
∈ ℙ) → (𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)) → (1 σ 𝑁) = (2 · 𝑁))) |
77 | 76 | impr 649 |
. . 3
⊢ ((𝑝 ∈ ℤ ∧
(((2↑𝑝) − 1)
∈ ℙ ∧ 𝑁 =
((2↑(𝑝 − 1))
· ((2↑𝑝)
− 1)))) → (1 σ 𝑁) = (2 · 𝑁)) |
78 | 77 | rexlimiva 3028 |
. 2
⊢
(∃𝑝 ∈
ℤ (((2↑𝑝)
− 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))) → (1 σ
𝑁) = (2 · 𝑁)) |
79 | 51, 78 | impbid1 215 |
1
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥
𝑁) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ
∧ 𝑁 = ((2↑(𝑝 − 1)) ·
((2↑𝑝) −
1))))) |