Proof of Theorem perfectlem1
Step | Hyp | Ref
| Expression |
1 | | 2nn 11448 |
. . 3
⊢ 2 ∈
ℕ |
2 | | perfectlem.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℕ) |
3 | 2 | nnnn0d 11702 |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
4 | | peano2nn0 11684 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ (𝐴 + 1) ∈
ℕ0) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 + 1) ∈
ℕ0) |
6 | | nnexpcl 13191 |
. . 3
⊢ ((2
∈ ℕ ∧ (𝐴 +
1) ∈ ℕ0) → (2↑(𝐴 + 1)) ∈ ℕ) |
7 | 1, 5, 6 | sylancr 581 |
. 2
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ) |
8 | | 2re 11449 |
. . . . 5
⊢ 2 ∈
ℝ |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℝ) |
10 | 2 | peano2nnd 11393 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) |
11 | | 1lt2 11553 |
. . . . 5
⊢ 1 <
2 |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 < 2) |
13 | | expgt1 13216 |
. . . 4
⊢ ((2
∈ ℝ ∧ (𝐴 +
1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1))) |
14 | 9, 10, 12, 13 | syl3anc 1439 |
. . 3
⊢ (𝜑 → 1 < (2↑(𝐴 + 1))) |
15 | | 1nn 11387 |
. . . 4
⊢ 1 ∈
ℕ |
16 | | nnsub 11419 |
. . . 4
⊢ ((1
∈ ℕ ∧ (2↑(𝐴 + 1)) ∈ ℕ) → (1 <
(2↑(𝐴 + 1)) ↔
((2↑(𝐴 + 1)) −
1) ∈ ℕ)) |
17 | 15, 7, 16 | sylancr 581 |
. . 3
⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ ((2↑(𝐴 + 1)) − 1) ∈
ℕ)) |
18 | 14, 17 | mpbid 224 |
. 2
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℕ) |
19 | 7 | nnzd 11833 |
. . . . . . 7
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℤ) |
20 | | peano2zm 11772 |
. . . . . . 7
⊢
((2↑(𝐴 + 1))
∈ ℤ → ((2↑(𝐴 + 1)) − 1) ∈
ℤ) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℤ) |
22 | | 1nn0 11660 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
23 | | perfectlem.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℕ) |
24 | | sgmnncl 25325 |
. . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈
ℕ) |
25 | 22, 23, 24 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (1 σ 𝐵) ∈
ℕ) |
26 | 25 | nnzd 11833 |
. . . . . 6
⊢ (𝜑 → (1 σ 𝐵) ∈
ℤ) |
27 | | dvdsmul1 15410 |
. . . . . 6
⊢
((((2↑(𝐴 + 1))
− 1) ∈ ℤ ∧ (1 σ 𝐵) ∈ ℤ) → ((2↑(𝐴 + 1)) − 1) ∥
(((2↑(𝐴 + 1)) −
1) · (1 σ 𝐵))) |
28 | 21, 26, 27 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∥
(((2↑(𝐴 + 1)) −
1) · (1 σ 𝐵))) |
29 | | 2cn 11450 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
30 | | expp1 13185 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
31 | 29, 3, 30 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
32 | | nnexpcl 13191 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ0) → (2↑𝐴) ∈ ℕ) |
33 | 1, 3, 32 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝐴) ∈ ℕ) |
34 | 33 | nncnd 11392 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐴) ∈ ℂ) |
35 | | mulcom 10358 |
. . . . . . . . 9
⊢
(((2↑𝐴) ∈
ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) |
36 | 34, 29, 35 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) |
37 | 31, 36 | eqtrd 2814 |
. . . . . . 7
⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴))) |
38 | 37 | oveq1d 6937 |
. . . . . 6
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵)) |
39 | 29 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℂ) |
40 | 23 | nncnd 11392 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
41 | 39, 34, 40 | mulassd 10400 |
. . . . . 6
⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵))) |
42 | | ax-1cn 10330 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
44 | | perfectlem.3 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 2 ∥ 𝐵) |
45 | | 2prm 15810 |
. . . . . . . . . . 11
⊢ 2 ∈
ℙ |
46 | 23 | nnzd 11833 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
47 | | coprm 15827 |
. . . . . . . . . . 11
⊢ ((2
∈ ℙ ∧ 𝐵
∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) |
48 | 45, 46, 47 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) |
49 | 44, 48 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → (2 gcd 𝐵) = 1) |
50 | | 2z 11761 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℤ) |
52 | | rpexp1i 15837 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝐵
∈ ℤ ∧ 𝐴
∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) |
53 | 51, 46, 3, 52 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) |
54 | 49, 53 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1) |
55 | | sgmmul 25378 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) |
56 | 43, 33, 23, 54, 55 | syl13anc 1440 |
. . . . . . 7
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) |
57 | | perfectlem.4 |
. . . . . . 7
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) |
58 | 2 | nncnd 11392 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
59 | | pncan 10628 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
60 | 58, 42, 59 | sylancl 580 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴) |
61 | 60 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) =
(2↑𝐴)) |
62 | 61 | oveq2d 6938 |
. . . . . . . . 9
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ
(2↑𝐴))) |
63 | | 1sgm2ppw 25377 |
. . . . . . . . . 10
⊢ ((𝐴 + 1) ∈ ℕ → (1
σ (2↑((𝐴 + 1)
− 1))) = ((2↑(𝐴
+ 1)) − 1)) |
64 | 10, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) =
((2↑(𝐴 + 1)) −
1)) |
65 | 62, 64 | eqtr3d 2816 |
. . . . . . . 8
⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1)) |
66 | 65 | oveq1d 6937 |
. . . . . . 7
⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵))) |
67 | 56, 57, 66 | 3eqtr3d 2822 |
. . . . . 6
⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) |
68 | 38, 41, 67 | 3eqtrd 2818 |
. . . . 5
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) |
69 | 28, 68 | breqtrrd 4914 |
. . . 4
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∥
((2↑(𝐴 + 1)) ·
𝐵)) |
70 | | gcdcom 15641 |
. . . . . 6
⊢
((((2↑(𝐴 + 1))
− 1) ∈ ℤ ∧ (2↑(𝐴 + 1)) ∈ ℤ) →
(((2↑(𝐴 + 1)) −
1) gcd (2↑(𝐴 + 1))) =
((2↑(𝐴 + 1)) gcd
((2↑(𝐴 + 1)) −
1))) |
71 | 21, 19, 70 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) gcd
(2↑(𝐴 + 1))) =
((2↑(𝐴 + 1)) gcd
((2↑(𝐴 + 1)) −
1))) |
72 | | iddvdsexp 15412 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ (𝐴 +
1) ∈ ℕ) → 2 ∥ (2↑(𝐴 + 1))) |
73 | 50, 10, 72 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → 2 ∥ (2↑(𝐴 + 1))) |
74 | | n2dvds1 15496 |
. . . . . . . . . 10
⊢ ¬ 2
∥ 1 |
75 | | 1zzd 11760 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) |
76 | 51, 19, 75 | 3jca 1119 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ∈ ℤ ∧
(2↑(𝐴 + 1)) ∈
ℤ ∧ 1 ∈ ℤ)) |
77 | | dvdssub2 15430 |
. . . . . . . . . . 11
⊢ (((2
∈ ℤ ∧ (2↑(𝐴 + 1)) ∈ ℤ ∧ 1 ∈
ℤ) ∧ 2 ∥ ((2↑(𝐴 + 1)) − 1)) → (2 ∥
(2↑(𝐴 + 1)) ↔ 2
∥ 1)) |
78 | 76, 77 | sylan 575 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 2 ∥ ((2↑(𝐴 + 1)) − 1)) → (2
∥ (2↑(𝐴 + 1))
↔ 2 ∥ 1)) |
79 | 74, 78 | mtbiri 319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ ((2↑(𝐴 + 1)) − 1)) → ¬
2 ∥ (2↑(𝐴 +
1))) |
80 | 79 | ex 403 |
. . . . . . . 8
⊢ (𝜑 → (2 ∥ ((2↑(𝐴 + 1)) − 1) → ¬ 2
∥ (2↑(𝐴 +
1)))) |
81 | 73, 80 | mt2d 134 |
. . . . . . 7
⊢ (𝜑 → ¬ 2 ∥
((2↑(𝐴 + 1)) −
1)) |
82 | | coprm 15827 |
. . . . . . . 8
⊢ ((2
∈ ℙ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℤ) →
(¬ 2 ∥ ((2↑(𝐴 + 1)) − 1) ↔ (2 gcd
((2↑(𝐴 + 1)) −
1)) = 1)) |
83 | 45, 21, 82 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (¬ 2 ∥
((2↑(𝐴 + 1)) −
1) ↔ (2 gcd ((2↑(𝐴 + 1)) − 1)) = 1)) |
84 | 81, 83 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → (2 gcd ((2↑(𝐴 + 1)) − 1)) =
1) |
85 | | rpexp1i 15837 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧
(𝐴 + 1) ∈
ℕ0) → ((2 gcd ((2↑(𝐴 + 1)) − 1)) = 1 →
((2↑(𝐴 + 1)) gcd
((2↑(𝐴 + 1)) −
1)) = 1)) |
86 | 51, 21, 5, 85 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → ((2 gcd ((2↑(𝐴 + 1)) − 1)) = 1 →
((2↑(𝐴 + 1)) gcd
((2↑(𝐴 + 1)) −
1)) = 1)) |
87 | 84, 86 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((2↑(𝐴 + 1)) gcd ((2↑(𝐴 + 1)) − 1)) =
1) |
88 | 71, 87 | eqtrd 2814 |
. . . 4
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) gcd
(2↑(𝐴 + 1))) =
1) |
89 | | coprmdvds 15772 |
. . . . 5
⊢
((((2↑(𝐴 + 1))
− 1) ∈ ℤ ∧ (2↑(𝐴 + 1)) ∈ ℤ ∧ 𝐵 ∈ ℤ) →
((((2↑(𝐴 + 1)) −
1) ∥ ((2↑(𝐴 +
1)) · 𝐵) ∧
(((2↑(𝐴 + 1)) −
1) gcd (2↑(𝐴 + 1))) =
1) → ((2↑(𝐴 + 1))
− 1) ∥ 𝐵)) |
90 | 21, 19, 46, 89 | syl3anc 1439 |
. . . 4
⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) ∥
((2↑(𝐴 + 1)) ·
𝐵) ∧ (((2↑(𝐴 + 1)) − 1) gcd
(2↑(𝐴 + 1))) = 1)
→ ((2↑(𝐴 + 1))
− 1) ∥ 𝐵)) |
91 | 69, 88, 90 | mp2and 689 |
. . 3
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∥ 𝐵) |
92 | | nndivdvds 15396 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∧
((2↑(𝐴 + 1)) −
1) ∈ ℕ) → (((2↑(𝐴 + 1)) − 1) ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℕ)) |
93 | 23, 18, 92 | syl2anc 579 |
. . 3
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℕ)) |
94 | 91, 93 | mpbid 224 |
. 2
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℕ) |
95 | 7, 18, 94 | 3jca 1119 |
1
⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧
((2↑(𝐴 + 1)) −
1) ∈ ℕ ∧ (𝐵
/ ((2↑(𝐴 + 1)) −
1)) ∈ ℕ)) |