Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
(1...𝑘) ∈
Fin) |
2 | | dvdsssfz1 15040 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ⊆ (1...𝑘)) |
3 | | ssfi 8180 |
. . . . . . . . . 10
⊢
(((1...𝑘) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑘} ⊆ (1...𝑘)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ∈ Fin) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ∈ Fin) |
5 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ⊆ ℕ |
6 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) |
7 | 5, 6 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → 𝑑 ∈ ℕ) |
8 | | vmacl 24844 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ ℕ →
(Λ‘𝑑) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (Λ‘𝑑) ∈ ℝ) |
10 | | dvdsdivcl 15038 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (𝑘 / 𝑑) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) |
11 | 5, 10 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (𝑘 / 𝑑) ∈ ℕ) |
12 | | vmacl 24844 |
. . . . . . . . . . 11
⊢ ((𝑘 / 𝑑) ∈ ℕ →
(Λ‘(𝑘 / 𝑑)) ∈
ℝ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → (Λ‘(𝑘 / 𝑑)) ∈ ℝ) |
14 | 9, 13 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) ∈ ℝ) |
15 | 4, 14 | fsumrecl 14465 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) ∈ ℝ) |
16 | | vmacl 24844 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
17 | | nnrp 11842 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
18 | 17 | relogcld 24369 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(log‘𝑘) ∈
ℝ) |
19 | 16, 18 | remulcld 10070 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ →
((Λ‘𝑘)
· (log‘𝑘))
∈ ℝ) |
20 | 15, 19 | readdcld 10069 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℝ) |
21 | 20 | recnd 10068 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℂ) |
22 | 21 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) →
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ ℂ) |
23 | | eqid 2622 |
. . . . 5
⊢ (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) = (𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) |
24 | 22, 23 | fmptd 6385 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))):ℕ⟶ℂ) |
25 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ ℕ |
26 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) |
27 | 25, 26 | sseldi 3601 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → 𝑚 ∈ ℕ) |
28 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑚)) |
29 | 28 | rabbidv 3189 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) |
30 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (𝑘 / 𝑑) = (𝑚 / 𝑑)) |
31 | 30 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (Λ‘(𝑘 / 𝑑)) = (Λ‘(𝑚 / 𝑑))) |
32 | 31 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) |
33 | 32 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑚 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) |
34 | 29, 33 | sumeq12dv 14437 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑)))) |
35 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (Λ‘𝑘) = (Λ‘𝑚)) |
36 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (log‘𝑘) = (log‘𝑚)) |
37 | 35, 36 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑚) · (log‘𝑚))) |
38 | 34, 37 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) |
39 | | ovex 6678 |
. . . . . . . . 9
⊢
(Σ𝑑 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑘} ((Λ‘𝑑) ·
(Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) ∈ V |
40 | 38, 23, 39 | fvmpt3i 6287 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) |
41 | 27, 40 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) → ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) |
42 | 41 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚) = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚)))) |
43 | | logsqvma 25231 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚))) = ((log‘𝑛)↑2)) |
44 | 43 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((Λ‘𝑑) · (Λ‘(𝑚 / 𝑑))) + ((Λ‘𝑚) · (log‘𝑚))) = ((log‘𝑛)↑2)) |
45 | 42, 44 | eqtr2d 2657 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
((log‘𝑛)↑2) =
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚)) |
46 | 45 | mpteq2dva 4744 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) =
(𝑛 ∈ ℕ ↦
Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((𝑘 ∈ ℕ ↦ (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑚))) |
47 | 24, 46 | muinv 24919 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘)))) = (𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))) |
48 | 47 | fveq1d 6193 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑁) = ((𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))‘𝑁)) |
49 | | breq2 4657 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑁)) |
50 | 49 | rabbidv 3189 |
. . . . 5
⊢ (𝑘 = 𝑁 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
51 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝑘 / 𝑑) = (𝑁 / 𝑑)) |
52 | 51 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (Λ‘(𝑘 / 𝑑)) = (Λ‘(𝑁 / 𝑑))) |
53 | 52 | oveq2d 6666 |
. . . . . 6
⊢ (𝑘 = 𝑁 → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) |
54 | 53 | adantr 481 |
. . . . 5
⊢ ((𝑘 = 𝑁 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘}) → ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) |
55 | 50, 54 | sumeq12dv 14437 |
. . . 4
⊢ (𝑘 = 𝑁 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑)))) |
56 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 𝑁 → (Λ‘𝑘) = (Λ‘𝑁)) |
57 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 𝑁 → (log‘𝑘) = (log‘𝑁)) |
58 | 56, 57 | oveq12d 6668 |
. . . 4
⊢ (𝑘 = 𝑁 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑁) · (log‘𝑁))) |
59 | 55, 58 | oveq12d 6668 |
. . 3
⊢ (𝑘 = 𝑁 → (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) |
60 | 59, 23, 39 | fvmpt3i 6287 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘} ((Λ‘𝑑) · (Λ‘(𝑘 / 𝑑))) + ((Λ‘𝑘) · (log‘𝑘))))‘𝑁) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) |
61 | | fveq2 6191 |
. . . . . 6
⊢ (𝑗 = 𝑑 → (μ‘𝑗) = (μ‘𝑑)) |
62 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑗 = 𝑑 → (𝑖 / 𝑗) = (𝑖 / 𝑑)) |
63 | 62 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑗 = 𝑑 → (log‘(𝑖 / 𝑗)) = (log‘(𝑖 / 𝑑))) |
64 | 63 | oveq1d 6665 |
. . . . . 6
⊢ (𝑗 = 𝑑 → ((log‘(𝑖 / 𝑗))↑2) = ((log‘(𝑖 / 𝑑))↑2)) |
65 | 61, 64 | oveq12d 6668 |
. . . . 5
⊢ (𝑗 = 𝑑 → ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2))) |
66 | 65 | cbvsumv 14426 |
. . . 4
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) |
67 | | breq2 4657 |
. . . . . 6
⊢ (𝑖 = 𝑁 → (𝑥 ∥ 𝑖 ↔ 𝑥 ∥ 𝑁)) |
68 | 67 | rabbidv 3189 |
. . . . 5
⊢ (𝑖 = 𝑁 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
69 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑖 = 𝑁 → (𝑖 / 𝑑) = (𝑁 / 𝑑)) |
70 | 69 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑖 = 𝑁 → (log‘(𝑖 / 𝑑)) = (log‘(𝑁 / 𝑑))) |
71 | 70 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑖 = 𝑁 → ((log‘(𝑖 / 𝑑))↑2) = ((log‘(𝑁 / 𝑑))↑2)) |
72 | 71 | oveq2d 6666 |
. . . . . 6
⊢ (𝑖 = 𝑁 → ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) |
73 | 72 | adantr 481 |
. . . . 5
⊢ ((𝑖 = 𝑁 ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) |
74 | 68, 73 | sumeq12dv 14437 |
. . . 4
⊢ (𝑖 = 𝑁 → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑑) · ((log‘(𝑖 / 𝑑))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) |
75 | 66, 74 | syl5eq 2668 |
. . 3
⊢ (𝑖 = 𝑁 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) |
76 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ⊆ ℕ |
77 | | dvdsdivcl 15038 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → (𝑖 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) |
78 | 76, 77 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → (𝑖 / 𝑗) ∈ ℕ) |
79 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑛 = (𝑖 / 𝑗) → (log‘𝑛) = (log‘(𝑖 / 𝑗))) |
80 | 79 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑛 = (𝑖 / 𝑗) → ((log‘𝑛)↑2) = ((log‘(𝑖 / 𝑗))↑2)) |
81 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) =
(𝑛 ∈ ℕ ↦
((log‘𝑛)↑2)) |
82 | | ovex 6678 |
. . . . . . . 8
⊢
((log‘𝑛)↑2) ∈ V |
83 | 80, 81, 82 | fvmpt3i 6287 |
. . . . . . 7
⊢ ((𝑖 / 𝑗) ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)) = ((log‘(𝑖 / 𝑗))↑2)) |
84 | 78, 83 | syl 17 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)) = ((log‘(𝑖 / 𝑗))↑2)) |
85 | 84 | oveq2d 6666 |
. . . . 5
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖}) → ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))) = ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) |
86 | 85 | sumeq2dv 14433 |
. . . 4
⊢ (𝑖 ∈ ℕ →
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))) = Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) |
87 | 86 | mpteq2ia 4740 |
. . 3
⊢ (𝑖 ∈ ℕ ↦
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗)))) = (𝑖 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2))) |
88 | | sumex 14418 |
. . 3
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑖} ((μ‘𝑗) · ((log‘(𝑖 / 𝑗))↑2)) ∈ V |
89 | 75, 87, 88 | fvmpt3i 6287 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑖 ∈ ℕ ↦
Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖} ((μ‘𝑗) · ((𝑛 ∈ ℕ ↦ ((log‘𝑛)↑2))‘(𝑖 / 𝑗))))‘𝑁) = Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2))) |
90 | 48, 60, 89 | 3eqtr3rd 2665 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) |