| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvdsfi 16827 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ∈ Fin) | 
| 2 |  | ssrab2 4079 | . . . . . . . . . . . 12
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ⊆ ℕ | 
| 3 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) | 
| 4 | 2, 3 | sselid 3980 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → 𝑑 ∈ ℕ) | 
| 5 |  | vmacl 27162 | . . . . . . . . . . 11
⊢ (𝑑 ∈ ℕ →
(Λ‘𝑑) ∈
ℝ) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (Λ‘𝑑) ∈ ℝ) | 
| 7 |  | dvdsdivcl 16354 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (𝑘 / 𝑑) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) | 
| 8 | 2, 7 | sselid 3980 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (𝑘 / 𝑑) ∈ ℕ) | 
| 9 |  | vmacl 27162 | . . . . . . . . . . 11
⊢ ((𝑘 / 𝑑) ∈ ℕ →
(Λ‘(𝑘 / 𝑑)) ∈
ℝ) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (Λ‘(𝑘 / 𝑑)) ∈ ℝ) | 
| 11 | 6, 10 | remulcld 11292 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) ∈ ℝ) | 
| 12 | 1, 11 | fsumrecl 15771 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) ∈ ℝ) | 
| 13 |  | vmacl 27162 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) | 
| 14 |  | nnrp 13047 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) | 
| 15 | 14 | relogcld 26666 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(log‘𝑘) ∈
ℝ) | 
| 16 | 13, 15 | remulcld 11292 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ →
((Λ‘𝑘)
· (log‘𝑘))
∈ ℝ) | 
| 17 | 12, 16 | readdcld 11291 | . . . . . . 7
⊢ (𝑘 ∈ ℕ →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℝ) | 
| 18 | 17 | recnd 11290 | . . . . . 6
⊢ (𝑘 ∈ ℕ →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℂ) | 
| 19 | 18 | adantl 481 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℂ) | 
| 20 | 19 | fmpttd 7134 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))):ℕ⟶ℂ) | 
| 21 |  | ssrab2 4079 | . . . . . . . . 9
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ ℕ | 
| 22 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) | 
| 23 | 21, 22 | sselid 3980 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → 𝑚 ∈ ℕ) | 
| 24 |  | breq2 5146 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑚)) | 
| 25 | 24 | rabbidv 3443 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) | 
| 26 |  | fvoveq1 7455 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (Λ‘(𝑘 / 𝑑)) = (Λ‘(𝑚 / 𝑑))) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) | 
| 28 | 27 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑘 = 𝑚 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) | 
| 29 | 25, 28 | sumeq12dv 15743 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) | 
| 30 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (Λ‘𝑘) = (Λ‘𝑚)) | 
| 31 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (log‘𝑘) = (log‘𝑚)) | 
| 32 | 30, 31 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑚) · (log‘𝑚))) | 
| 33 | 29, 32 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑘 = 𝑚 → (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) | 
| 34 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) = (𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) | 
| 35 |  | ovex 7465 | . . . . . . . . 9
⊢
(Σ𝑑 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑘} ((Λ‘𝑑) ·
(Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ V | 
| 36 | 33, 34, 35 | fvmpt3i 7020 | . . . . . . . 8
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) | 
| 37 | 23, 36 | syl 17 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) | 
| 38 | 37 | sumeq2dv 15739 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) | 
| 39 |  | logsqvma 27587 | . . . . . . 7
⊢ (𝑛 ∈ ℕ →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚))) = ((log‘𝑛)↑2)) | 
| 40 | 39 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚))) = ((log‘𝑛)↑2)) | 
| 41 | 38, 40 | eqtr2d 2777 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
((log‘𝑛)↑2) =
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚)) | 
| 42 | 41 | mpteq2dva 5241 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) =
(𝑛 ∈ ℕ ↦
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚))) | 
| 43 | 20, 42 | muinv 27237 | . . 3
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) = (𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))) | 
| 44 | 43 | fveq1d 6907 | . 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑁) = ((𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))‘𝑁)) | 
| 45 |  | breq2 5146 | . . . . . 6
⊢ (𝑘 = 𝑁 → (𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑁)) | 
| 46 | 45 | rabbidv 3443 | . . . . 5
⊢ (𝑘 = 𝑁 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) | 
| 47 |  | fvoveq1 7455 | . . . . . . 7
⊢ (𝑘 = 𝑁 → (Λ‘(𝑘 / 𝑑)) = (Λ‘(𝑁 / 𝑑))) | 
| 48 | 47 | oveq2d 7448 | . . . . . 6
⊢ (𝑘 = 𝑁 → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) | 
| 49 | 48 | adantr 480 | . . . . 5
⊢ ((𝑘 = 𝑁 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) | 
| 50 | 46, 49 | sumeq12dv 15743 | . . . 4
⊢ (𝑘 = 𝑁 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) | 
| 51 |  | fveq2 6905 | . . . . 5
⊢ (𝑘 = 𝑁 → (Λ‘𝑘) = (Λ‘𝑁)) | 
| 52 |  | fveq2 6905 | . . . . 5
⊢ (𝑘 = 𝑁 → (log‘𝑘) = (log‘𝑁)) | 
| 53 | 51, 52 | oveq12d 7450 | . . . 4
⊢ (𝑘 = 𝑁 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑁) · (log‘𝑁))) | 
| 54 | 50, 53 | oveq12d 7450 | . . 3
⊢ (𝑘 = 𝑁 → (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) | 
| 55 | 54, 34, 35 | fvmpt3i 7020 | . 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑁) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) | 
| 56 |  | fveq2 6905 | . . . . . 6
⊢ (𝑗 = 𝑑 → (μ‘𝑗) = (μ‘𝑑)) | 
| 57 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑗 = 𝑑 → (𝑖 / 𝑗) = (𝑖 / 𝑑)) | 
| 58 | 57 | fveq2d 6909 | . . . . . . 7
⊢ (𝑗 = 𝑑 → (log‘(𝑖 / 𝑗)) = (log‘(𝑖 / 𝑑))) | 
| 59 | 58 | oveq1d 7447 | . . . . . 6
⊢ (𝑗 = 𝑑 → ((log‘(𝑖 / 𝑗))↑2) = ((log‘(𝑖 / 𝑑))↑2)) | 
| 60 | 56, 59 | oveq12d 7450 | . . . . 5
⊢ (𝑗 = 𝑑 → ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2))) | 
| 61 | 60 | cbvsumv 15733 | . . . 4
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) | 
| 62 |  | breq2 5146 | . . . . . 6
⊢ (𝑖 = 𝑁 → (𝑥 ∥ 𝑖 ↔ 𝑥 ∥ 𝑁)) | 
| 63 | 62 | rabbidv 3443 | . . . . 5
⊢ (𝑖 = 𝑁 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) | 
| 64 |  | fvoveq1 7455 | . . . . . . . 8
⊢ (𝑖 = 𝑁 → (log‘(𝑖 / 𝑑)) = (log‘(𝑁 / 𝑑))) | 
| 65 | 64 | oveq1d 7447 | . . . . . . 7
⊢ (𝑖 = 𝑁 → ((log‘(𝑖 / 𝑑))↑2) = ((log‘(𝑁 / 𝑑))↑2)) | 
| 66 | 65 | oveq2d 7448 | . . . . . 6
⊢ (𝑖 = 𝑁 → ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) | 
| 67 | 66 | adantr 480 | . . . . 5
⊢ ((𝑖 = 𝑁 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) | 
| 68 | 63, 67 | sumeq12dv 15743 | . . . 4
⊢ (𝑖 = 𝑁 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) | 
| 69 | 61, 68 | eqtrid 2788 | . . 3
⊢ (𝑖 = 𝑁 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) | 
| 70 |  | ssrab2 4079 | . . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ⊆ ℕ | 
| 71 |  | dvdsdivcl 16354 | . . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → (𝑖 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) | 
| 72 | 70, 71 | sselid 3980 | . . . . . . 7
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → (𝑖 / 𝑗) ∈ ℕ) | 
| 73 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑛 = (𝑖 / 𝑗) → (log‘𝑛) = (log‘(𝑖 / 𝑗))) | 
| 74 | 73 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑛 = (𝑖 / 𝑗) → ((log‘𝑛)↑2) = ((log‘(𝑖 / 𝑗))↑2)) | 
| 75 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) =
(𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) | 
| 76 |  | ovex 7465 | . . . . . . . 8
⊢
((log‘𝑛)↑2) ∈ V | 
| 77 | 74, 75, 76 | fvmpt3i 7020 | . . . . . . 7
⊢ ((𝑖 / 𝑗) ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)) = ((log‘(𝑖 / 𝑗))↑2)) | 
| 78 | 72, 77 | syl 17 | . . . . . 6
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)) = ((log‘(𝑖 / 𝑗))↑2)) | 
| 79 | 78 | oveq2d 7448 | . . . . 5
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))) = ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) | 
| 80 | 79 | sumeq2dv 15739 | . . . 4
⊢ (𝑖 ∈ ℕ →
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))) = Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) | 
| 81 | 80 | mpteq2ia 5244 | . . 3
⊢ (𝑖 ∈ ℕ ↦
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)))) = (𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) | 
| 82 |  | sumex 15725 | . . 3
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) ∈ V | 
| 83 | 69, 81, 82 | fvmpt3i 7020 | . 2
⊢ (𝑁 ∈ ℕ → ((𝑖 ∈ ℕ ↦
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))‘𝑁) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) | 
| 84 | 44, 55, 83 | 3eqtr3rd 2785 | 1
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) |