| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | perfectlem.2 | . . . 4
⊢ (𝜑 → 𝐵 ∈ ℕ) | 
| 2 |  | 1red 11262 | . . . . 5
⊢ (𝜑 → 1 ∈
ℝ) | 
| 3 |  | perfectlem.1 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℕ) | 
| 4 |  | perfectlem.3 | . . . . . . . 8
⊢ (𝜑 → ¬ 2 ∥ 𝐵) | 
| 5 |  | perfectlem.4 | . . . . . . . 8
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) | 
| 6 | 3, 1, 4, 5 | perfectlem1 27273 | . . . . . . 7
⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧
((2↑(𝐴 + 1)) −
1) ∈ ℕ ∧ (𝐵
/ ((2↑(𝐴 + 1)) −
1)) ∈ ℕ)) | 
| 7 | 6 | simp3d 1145 | . . . . . 6
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℕ) | 
| 8 | 7 | nnred 12281 | . . . . 5
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℝ) | 
| 9 | 1 | nnred 12281 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 10 | 7 | nnge1d 12314 | . . . . 5
⊢ (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 11 |  | 2cn 12341 | . . . . . . . . . . 11
⊢ 2 ∈
ℂ | 
| 12 |  | exp1 14108 | . . . . . . . . . . 11
⊢ (2 ∈
ℂ → (2↑1) = 2) | 
| 13 | 11, 12 | ax-mp 5 | . . . . . . . . . 10
⊢
(2↑1) = 2 | 
| 14 |  | df-2 12329 | . . . . . . . . . 10
⊢ 2 = (1 +
1) | 
| 15 | 13, 14 | eqtri 2765 | . . . . . . . . 9
⊢
(2↑1) = (1 + 1) | 
| 16 |  | 2re 12340 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ | 
| 17 | 16 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ) | 
| 18 |  | 1zzd 12648 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) | 
| 19 | 3 | peano2nnd 12283 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) | 
| 20 | 19 | nnzd 12640 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 1) ∈ ℤ) | 
| 21 |  | 1lt2 12437 | . . . . . . . . . . 11
⊢ 1 <
2 | 
| 22 | 21 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 1 < 2) | 
| 23 |  | 1re 11261 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ | 
| 24 | 3 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 25 |  | ltaddrp 13072 | . . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ+) → 1 < (1 + 𝐴)) | 
| 26 | 23, 24, 25 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → 1 < (1 + 𝐴)) | 
| 27 |  | ax-1cn 11213 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 28 | 3 | nncnd 12282 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 29 |  | addcom 11447 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 + 𝐴) = (𝐴 + 1)) | 
| 30 | 27, 28, 29 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → (1 + 𝐴) = (𝐴 + 1)) | 
| 31 | 26, 30 | breqtrd 5169 | . . . . . . . . . 10
⊢ (𝜑 → 1 < (𝐴 + 1)) | 
| 32 |  | ltexp2a 14206 | . . . . . . . . . 10
⊢ (((2
∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧
1 < (𝐴 + 1))) →
(2↑1) < (2↑(𝐴
+ 1))) | 
| 33 | 17, 18, 20, 22, 31, 32 | syl32anc 1380 | . . . . . . . . 9
⊢ (𝜑 → (2↑1) <
(2↑(𝐴 +
1))) | 
| 34 | 15, 33 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (𝜑 → (1 + 1) <
(2↑(𝐴 +
1))) | 
| 35 | 6 | simp1d 1143 | . . . . . . . . . 10
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ) | 
| 36 | 35 | nnred 12281 | . . . . . . . . 9
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ) | 
| 37 | 2, 2, 36 | ltaddsubd 11863 | . . . . . . . 8
⊢ (𝜑 → ((1 + 1) <
(2↑(𝐴 + 1)) ↔ 1
< ((2↑(𝐴 + 1))
− 1))) | 
| 38 | 34, 37 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → 1 < ((2↑(𝐴 + 1)) −
1)) | 
| 39 |  | 0lt1 11785 | . . . . . . . . 9
⊢ 0 <
1 | 
| 40 | 39 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 < 1) | 
| 41 |  | peano2rem 11576 | . . . . . . . . 9
⊢
((2↑(𝐴 + 1))
∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈
ℝ) | 
| 42 | 36, 41 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℝ) | 
| 43 |  | expgt1 14141 | . . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (𝐴 +
1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1))) | 
| 44 | 16, 19, 22, 43 | mp3an2i 1468 | . . . . . . . . 9
⊢ (𝜑 → 1 < (2↑(𝐴 + 1))) | 
| 45 |  | posdif 11756 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 <
(2↑(𝐴 + 1)) ↔ 0
< ((2↑(𝐴 + 1))
− 1))) | 
| 46 | 23, 36, 45 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 <
((2↑(𝐴 + 1)) −
1))) | 
| 47 | 44, 46 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → 0 < ((2↑(𝐴 + 1)) −
1)) | 
| 48 | 1 | nngt0d 12315 | . . . . . . . 8
⊢ (𝜑 → 0 < 𝐵) | 
| 49 |  | ltdiv2 12154 | . . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0
< ((2↑(𝐴 + 1))
− 1)) ∧ (𝐵 ∈
ℝ ∧ 0 < 𝐵))
→ (1 < ((2↑(𝐴
+ 1)) − 1) ↔ (𝐵
/ ((2↑(𝐴 + 1)) −
1)) < (𝐵 /
1))) | 
| 50 | 2, 40, 42, 47, 9, 48, 49 | syl222anc 1388 | . . . . . . 7
⊢ (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))) | 
| 51 | 38, 50 | mpbid 232 | . . . . . 6
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)) | 
| 52 | 1 | nncnd 12282 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 53 | 52 | div1d 12035 | . . . . . 6
⊢ (𝜑 → (𝐵 / 1) = 𝐵) | 
| 54 | 51, 53 | breqtrd 5169 | . . . . 5
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵) | 
| 55 | 2, 8, 9, 10, 54 | lelttrd 11419 | . . . 4
⊢ (𝜑 → 1 < 𝐵) | 
| 56 |  | eluz2b2 12963 | . . . 4
⊢ (𝐵 ∈
(ℤ≥‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵)) | 
| 57 | 1, 55, 56 | sylanbrc 583 | . . 3
⊢ (𝜑 → 𝐵 ∈
(ℤ≥‘2)) | 
| 58 |  | fzfid 14014 | . . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐵) ∈ Fin) | 
| 59 |  | dvdsssfz1 16355 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) | 
| 60 | 1, 59 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) | 
| 61 | 58, 60 | ssfid 9301 | . . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin) | 
| 63 |  | ssrab2 4080 | . . . . . . . . . . . . 13
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ | 
| 64 | 63 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ) | 
| 65 | 64 | sselda 3983 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ) | 
| 66 | 65 | nnred 12281 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ) | 
| 67 | 65 | nnnn0d 12587 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ0) | 
| 68 | 67 | nn0ge0d 12590 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘) | 
| 69 |  | df-tp 4631 | . . . . . . . . . . . 12
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) | 
| 70 | 7, 1 | prssd 4822 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ) | 
| 71 | 70 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ) | 
| 72 |  | simplrl 777 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ) | 
| 73 | 72 | snssd 4809 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ) | 
| 74 | 71, 73 | unssd 4192 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ) | 
| 75 | 69, 74 | eqsstrid 4022 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ) | 
| 76 | 6 | simp2d 1144 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℕ) | 
| 77 | 76 | nnzd 12640 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℤ) | 
| 78 | 7 | nnzd 12640 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℤ) | 
| 79 |  | dvdsmul2 16316 | . . . . . . . . . . . . . . . . 17
⊢
((((2↑(𝐴 + 1))
− 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) →
(𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥
(((2↑(𝐴 + 1)) −
1) · (𝐵 /
((2↑(𝐴 + 1)) −
1)))) | 
| 80 | 77, 78, 79 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) | 
| 81 | 76 | nncnd 12282 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℂ) | 
| 82 | 76 | nnne0d 12316 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠
0) | 
| 83 | 52, 81, 82 | divcan2d 12045 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵) | 
| 84 | 80, 83 | breqtrd 5169 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵) | 
| 85 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥 ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)) | 
| 86 | 84, 85 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵)) | 
| 87 | 86 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵)) | 
| 88 | 1 | nnzd 12640 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 89 |  | iddvds 16307 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℤ → 𝐵 ∥ 𝐵) | 
| 90 | 88, 89 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∥ 𝐵) | 
| 91 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐵 → (𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵)) | 
| 92 | 90, 91 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵)) | 
| 93 | 92 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵)) | 
| 94 |  | simplrr 778 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∥ 𝐵) | 
| 95 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵)) | 
| 96 | 94, 95 | syl5ibrcom 247 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛 → 𝑥 ∥ 𝐵)) | 
| 97 | 87, 93, 96 | 3jaod 1431 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛) → 𝑥 ∥ 𝐵)) | 
| 98 |  | eltpi 4688 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛)) | 
| 99 | 97, 98 | impel 505 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥 ∥ 𝐵) | 
| 100 | 75, 99 | ssrabdv 4074 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) | 
| 101 | 62, 66, 68, 100 | fsumless 15832 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) | 
| 102 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) | 
| 103 |  | disjsn 4711 | . . . . . . . . . . . 12
⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) | 
| 104 | 102, 103 | sylibr 234 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅) | 
| 105 | 69 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})) | 
| 106 |  | tpfi 9365 | . . . . . . . . . . . 12
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin | 
| 107 | 106 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin) | 
| 108 | 75 | sselda 3983 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ) | 
| 109 | 108 | nncnd 12282 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ) | 
| 110 | 104, 105,
107, 109 | fsumsplit 15777 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘)) | 
| 111 | 7 | nncnd 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℂ) | 
| 112 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 113 | 112 | sumsn 15782 | . . . . . . . . . . . . . . 15
⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧
(𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℂ) → Σ𝑘
∈ {(𝐵 /
((2↑(𝐴 + 1)) −
1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 114 | 7, 111, 113 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 115 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝐵 → 𝑘 = 𝐵) | 
| 116 | 115 | sumsn 15782 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
Σ𝑘 ∈ {𝐵}𝑘 = 𝐵) | 
| 117 | 1, 52, 116 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵) | 
| 118 | 114, 117 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) | 
| 119 |  | incom 4209 | . . . . . . . . . . . . . . 15
⊢ ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) | 
| 120 | 8, 54 | gtned 11396 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 121 |  | disjsn2 4712 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) =
∅) | 
| 122 | 120, 121 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) =
∅) | 
| 123 | 119, 122 | eqtr3id 2791 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅) | 
| 124 |  | df-pr 4629 | . . . . . . . . . . . . . . 15
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}) | 
| 125 | 124 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})) | 
| 126 |  | prfi 9363 | . . . . . . . . . . . . . . 15
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin | 
| 127 | 126 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin) | 
| 128 | 70 | sselda 3983 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ) | 
| 129 | 128 | nncnd 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ) | 
| 130 | 123, 125,
127, 129 | fsumsplit 15777 | . . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘)) | 
| 131 | 81, 52 | mulcld 11281 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈
ℂ) | 
| 132 | 52, 131, 81, 82 | divdird 12081 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))) | 
| 133 | 35 | nncnd 12282 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ) | 
| 134 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) | 
| 135 | 133, 134,
52 | subdird 11720 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵))) | 
| 136 | 52 | mullidd 11279 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝐵) = 𝐵) | 
| 137 | 136 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) | 
| 138 | 135, 137 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) | 
| 139 | 138 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))) | 
| 140 | 133, 52 | mulcld 11281 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈
ℂ) | 
| 141 | 52, 140 | pncan3d 11623 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵)) | 
| 142 | 139, 141 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵)) | 
| 143 | 142 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) | 
| 144 | 133, 52, 81, 82 | divassd 12078 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 145 | 143, 144 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 146 | 52, 81, 82 | divcan3d 12048 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵) | 
| 147 | 146 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) | 
| 148 | 132, 145,
147 | 3eqtr3d 2785 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) | 
| 149 | 118, 130,
148 | 3eqtr4d 2787 | . . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 150 | 149 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 151 | 72 | nncnd 12282 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ) | 
| 152 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) | 
| 153 | 152 | sumsn 15782 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
Σ𝑘 ∈ {𝑛}𝑘 = 𝑛) | 
| 154 | 151, 151,
153 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛) | 
| 155 | 150, 154 | oveq12d 7449 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) | 
| 156 | 110, 155 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) | 
| 157 | 3 | nnnn0d 12587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈
ℕ0) | 
| 158 |  | expp1 14109 | . . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) | 
| 159 | 11, 157, 158 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) | 
| 160 |  | 2nn 12339 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ | 
| 161 |  | nnexpcl 14115 | . . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ0) → (2↑𝐴) ∈ ℕ) | 
| 162 | 160, 157,
161 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2↑𝐴) ∈ ℕ) | 
| 163 | 162 | nncnd 12282 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2↑𝐴) ∈ ℂ) | 
| 164 |  | mulcom 11241 | . . . . . . . . . . . . . . . . 17
⊢
(((2↑𝐴) ∈
ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) | 
| 165 | 163, 11, 164 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) | 
| 166 | 159, 165 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴))) | 
| 167 | 166 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵)) | 
| 168 |  | 2cnd 12344 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) | 
| 169 | 168, 163,
52 | mulassd 11284 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵))) | 
| 170 |  | 2prm 16729 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℙ | 
| 171 |  | coprm 16748 | . . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℙ ∧ 𝐵
∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) | 
| 172 | 170, 88, 171 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) | 
| 173 | 4, 172 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 gcd 𝐵) = 1) | 
| 174 |  | 2z 12649 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ | 
| 175 |  | rpexp1i 16760 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 𝐵
∈ ℤ ∧ 𝐴
∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) | 
| 176 | 174, 88, 157, 175 | mp3an2i 1468 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) | 
| 177 | 173, 176 | mpd 15 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1) | 
| 178 |  | sgmmul 27245 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) | 
| 179 | 134, 162,
1, 177, 178 | syl13anc 1374 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) | 
| 180 |  | pncan 11514 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) | 
| 181 | 28, 27, 180 | sylancl 586 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴) | 
| 182 | 181 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) =
(2↑𝐴)) | 
| 183 | 182 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ
(2↑𝐴))) | 
| 184 |  | 1sgm2ppw 27244 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 + 1) ∈ ℕ → (1
σ (2↑((𝐴 + 1)
− 1))) = ((2↑(𝐴
+ 1)) − 1)) | 
| 185 | 19, 184 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) =
((2↑(𝐴 + 1)) −
1)) | 
| 186 | 183, 185 | eqtr3d 2779 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1)) | 
| 187 | 186 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵))) | 
| 188 | 179, 5, 187 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) | 
| 189 | 167, 169,
188 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) | 
| 190 | 189 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵)) /
((2↑(𝐴 + 1)) −
1))) | 
| 191 |  | 1nn0 12542 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 | 
| 192 |  | sgmnncl 27190 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈
ℕ) | 
| 193 | 191, 1, 192 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 σ 𝐵) ∈
ℕ) | 
| 194 | 193 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 σ 𝐵) ∈
ℂ) | 
| 195 | 194, 81, 82 | divcan3d 12048 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵)) /
((2↑(𝐴 + 1)) −
1)) = (1 σ 𝐵)) | 
| 196 | 190, 144,
195 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵)) | 
| 197 |  | sgmval 27185 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐵
∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1)) | 
| 198 | 27, 1, 197 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1)) | 
| 199 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) | 
| 200 | 63, 199 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ) | 
| 201 | 200 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℂ) | 
| 202 | 201 | cxp1d 26748 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → (𝑘↑𝑐1) = 𝑘) | 
| 203 | 202 | sumeq2dv 15738 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) | 
| 204 | 196, 198,
203 | 3eqtrrd 2782 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 205 | 204 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 206 | 101, 156,
205 | 3brtr3d 5174 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 207 | 36, 8 | remulcld 11291 | . . . . . . . . . . 11
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈
ℝ) | 
| 208 | 207 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈
ℝ) | 
| 209 | 72 | nnrpd 13075 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ+) | 
| 210 | 208, 209 | ltaddrpd 13110 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) | 
| 211 | 72 | nnred 12281 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ) | 
| 212 | 208, 211 | readdcld 11290 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ) | 
| 213 | 208, 212 | ltnled 11408 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))) | 
| 214 | 210, 213 | mpbid 232 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 215 | 206, 214 | condan 818 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) | 
| 216 |  | elpri 4649 | . . . . . . 7
⊢ (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) | 
| 217 | 215, 216 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) | 
| 218 | 217 | expr 456 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) | 
| 219 | 218 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) | 
| 220 | 2, 55 | gtned 11396 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 1) | 
| 221 | 220 | necomd 2996 | . . . . . . . . 9
⊢ (𝜑 → 1 ≠ 𝐵) | 
| 222 |  | 1dvds 16308 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → 1 ∥
𝐵) | 
| 223 | 88, 222 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∥ 𝐵) | 
| 224 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵)) | 
| 225 |  | eqeq1 2741 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 226 |  | eqeq1 2741 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵)) | 
| 227 | 225, 226 | orbi12d 919 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))) | 
| 228 | 224, 227 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑛 = 1 → ((𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))) | 
| 229 |  | 1nn 12277 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ | 
| 230 | 229 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℕ) | 
| 231 | 228, 219,
230 | rspcdva 3623 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))) | 
| 232 | 223, 231 | mpd 15 | . . . . . . . . . . 11
⊢ (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)) | 
| 233 | 232 | ord 865 | . . . . . . . . . 10
⊢ (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵)) | 
| 234 | 233 | necon1ad 2957 | . . . . . . . . 9
⊢ (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 235 | 221, 234 | mpd 15 | . . . . . . . 8
⊢ (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 236 | 235 | eqeq2d 2748 | . . . . . . 7
⊢ (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 237 | 236 | orbi1d 917 | . . . . . 6
⊢ (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) | 
| 238 | 237 | imbi2d 340 | . . . . 5
⊢ (𝜑 → ((𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))) | 
| 239 | 238 | ralbidv 3178 | . . . 4
⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))) | 
| 240 | 219, 239 | mpbird 257 | . . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))) | 
| 241 |  | isprm2 16719 | . . 3
⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈
(ℤ≥‘2) ∧ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))) | 
| 242 | 57, 240, 241 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐵 ∈ ℙ) | 
| 243 | 207 | ltp1d 12198 | . . . 4
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) | 
| 244 |  | peano2re 11434 | . . . . . 6
⊢
(((2↑(𝐴 + 1))
· (𝐵 /
((2↑(𝐴 + 1)) −
1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈
ℝ) | 
| 245 | 207, 244 | syl 17 | . . . . 5
⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈
ℝ) | 
| 246 | 207, 245 | ltnled 11408 | . . . 4
⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬
(((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1))))) | 
| 247 | 243, 246 | mpbid 232 | . . 3
⊢ (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) | 
| 248 | 200 | nnred 12281 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ) | 
| 249 | 200 | nnnn0d 12587 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ0) | 
| 250 | 249 | nn0ge0d 12590 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘) | 
| 251 |  | df-tp 4631 | . . . . . . . . . 10
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) | 
| 252 |  | snssi 4808 | . . . . . . . . . . . 12
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) | 
| 253 | 229, 252 | mp1i 13 | . . . . . . . . . . 11
⊢ (𝜑 → {1} ⊆
ℕ) | 
| 254 | 70, 253 | unssd 4192 | . . . . . . . . . 10
⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆
ℕ) | 
| 255 | 251, 254 | eqsstrid 4022 | . . . . . . . . 9
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ) | 
| 256 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵)) | 
| 257 | 223, 256 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 = 1 → 𝑥 ∥ 𝐵)) | 
| 258 | 86, 92, 257 | 3jaod 1431 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1) → 𝑥 ∥ 𝐵)) | 
| 259 |  | eltpi 4688 | . . . . . . . . . 10
⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1)) | 
| 260 | 258, 259 | impel 505 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥 ∥ 𝐵) | 
| 261 | 255, 260 | ssrabdv 4074 | . . . . . . . 8
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) | 
| 262 | 61, 248, 250, 261 | fsumless 15832 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) | 
| 263 | 262 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) | 
| 264 | 52, 81, 82 | diveq1ad 12052 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | 
| 265 | 264 | necon3bid 2985 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) −
1))) | 
| 266 | 265 | biimpar 477 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1) | 
| 267 | 266 | necomd 2996 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1))) | 
| 268 | 221 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵) | 
| 269 | 267, 268 | nelprd 4657 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈
{(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) | 
| 270 |  | disjsn 4711 | . . . . . . . . 9
⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈
{(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) | 
| 271 | 269, 270 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅) | 
| 272 | 251 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})) | 
| 273 |  | tpfi 9365 | . . . . . . . . 9
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin | 
| 274 | 273 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin) | 
| 275 | 255 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ) | 
| 276 | 275 | sselda 3983 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ) | 
| 277 | 276 | nncnd 12282 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ) | 
| 278 | 271, 272,
274, 277 | fsumsplit 15777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘)) | 
| 279 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑘 = 1 → 𝑘 = 1) | 
| 280 | 279 | sumsn 15782 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1) | 
| 281 | 2, 27, 280 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1) | 
| 282 | 149, 281 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) | 
| 283 | 282 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) | 
| 284 | 278, 283 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) | 
| 285 | 204 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) | 
| 286 | 263, 284,
285 | 3brtr3d 5174 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) | 
| 287 | 286 | ex 412 | . . . 4
⊢ (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1))))) | 
| 288 | 287 | necon1bd 2958 | . . 3
⊢ (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1))) | 
| 289 | 247, 288 | mpd 15 | . 2
⊢ (𝜑 → 𝐵 = ((2↑(𝐴 + 1)) − 1)) | 
| 290 | 242, 289 | jca 511 | 1
⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) |