Metamath Proof Explorer

Theorem logsqvma2

Description: The Möbius inverse of logsqvma . Equation 10.4.8 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Assertion logsqvma2 ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvdsfi ⊢ ( 𝑘 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ∈ Fin )
2 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ⊆ ℕ
3 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } )
4 2 3 sselid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → 𝑑 ∈ ℕ )
5 vmacl ⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
6 4 5 syl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
7 dvdsdivcl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( 𝑘 / 𝑑 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } )
8 2 7 sselid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( 𝑘 / 𝑑 ) ∈ ℕ )
9 vmacl ⊢ ( ( 𝑘 / 𝑑 ) ∈ ℕ → ( Λ ‘ ( 𝑘 / 𝑑 ) ) ∈ ℝ )
10 8 9 syl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( Λ ‘ ( 𝑘 / 𝑑 ) ) ∈ ℝ )
11 6 10 remulcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) ∈ ℝ )
12 1 11 fsumrecl ⊢ ( 𝑘 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) ∈ ℝ )
13 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
14 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
15 14 relogcld ⊢ ( 𝑘 ∈ ℕ → ( log ‘ 𝑘 ) ∈ ℝ )
16 13 15 remulcld ⊢ ( 𝑘 ∈ ℕ → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ∈ ℝ )
17 12 16 readdcld ⊢ ( 𝑘 ∈ ℕ → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ∈ ℝ )
18 17 recnd ⊢ ( 𝑘 ∈ ℕ → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ∈ ℂ )
19 18 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ∈ ℂ )
20 19 fmpttd ⊢ ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) : ℕ ⟶ ℂ )
21 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ⊆ ℕ
22 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } )
23 21 22 sselid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑚 ∈ ℕ )
24 breq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑚 ) )
25 24 rabbidv ⊢ ( 𝑘 = 𝑚 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
26 fvoveq1 ⊢ ( 𝑘 = 𝑚 → ( Λ ‘ ( 𝑘 / 𝑑 ) ) = ( Λ ‘ ( 𝑚 / 𝑑 ) ) )
27 26 oveq2d ⊢ ( 𝑘 = 𝑚 → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) )
28 27 adantr ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) )
29 25 28 sumeq12dv ⊢ ( 𝑘 = 𝑚 → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) )
30 fveq2 ⊢ ( 𝑘 = 𝑚 → ( Λ ‘ 𝑘 ) = ( Λ ‘ 𝑚 ) )
31 fveq2 ⊢ ( 𝑘 = 𝑚 → ( log ‘ 𝑘 ) = ( log ‘ 𝑚 ) )
32 30 31 oveq12d ⊢ ( 𝑘 = 𝑚 → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
33 29 32 oveq12d ⊢ ( 𝑘 = 𝑚 → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
34 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) )
35 ovex ⊢ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ∈ V
36 33 34 35 fvmpt3i ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑚 ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
37 23 36 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑚 ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
38 37 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑚 ) = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
39 logsqvma ⊢ ( 𝑛 ∈ ℕ → Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( ( log ‘ 𝑛 ) ↑ 2 ) )
40 39 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑚 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( ( log ‘ 𝑛 ) ↑ 2 ) )
41 38 40 eqtr2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( log ‘ 𝑛 ) ↑ 2 ) = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑚 ) )
42 41 mpteq2dva ⊢ ( 𝑁 ∈ ℕ → ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑚 ) ) )
43 20 42 muinv ⊢ ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) ) )
44 43 fveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑁 ) = ( ( 𝑖 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) ) ‘ 𝑁 ) )
45 breq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑥 ∥ 𝑘 ↔ 𝑥 ∥ 𝑁 ) )
46 45 rabbidv ⊢ ( 𝑘 = 𝑁 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
47 fvoveq1 ⊢ ( 𝑘 = 𝑁 → ( Λ ‘ ( 𝑘 / 𝑑 ) ) = ( Λ ‘ ( 𝑁 / 𝑑 ) ) )
48 47 oveq2d ⊢ ( 𝑘 = 𝑁 → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) )
49 48 adantr ⊢ ( ( 𝑘 = 𝑁 ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) )
50 46 49 sumeq12dv ⊢ ( 𝑘 = 𝑁 → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) )
51 fveq2 ⊢ ( 𝑘 = 𝑁 → ( Λ ‘ 𝑘 ) = ( Λ ‘ 𝑁 ) )
52 fveq2 ⊢ ( 𝑘 = 𝑁 → ( log ‘ 𝑘 ) = ( log ‘ 𝑁 ) )
53 51 52 oveq12d ⊢ ( 𝑘 = 𝑁 → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) )
54 50 53 oveq12d ⊢ ( 𝑘 = 𝑁 → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
55 54 34 35 fvmpt3i ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑘 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑘 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) ) ) ‘ 𝑁 ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
56 fveq2 ⊢ ( 𝑗 = 𝑑 → ( μ ‘ 𝑗 ) = ( μ ‘ 𝑑 ) )
57 oveq2 ⊢ ( 𝑗 = 𝑑 → ( 𝑖 / 𝑗 ) = ( 𝑖 / 𝑑 ) )
58 57 fveq2d ⊢ ( 𝑗 = 𝑑 → ( log ‘ ( 𝑖 / 𝑗 ) ) = ( log ‘ ( 𝑖 / 𝑑 ) ) )
59 58 oveq1d ⊢ ( 𝑗 = 𝑑 → ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) = ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) )
60 56 59 oveq12d ⊢ ( 𝑗 = 𝑑 → ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) ) )
61 60 cbvsumv ⊢ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) )
62 breq2 ⊢ ( 𝑖 = 𝑁 → ( 𝑥 ∥ 𝑖 ↔ 𝑥 ∥ 𝑁 ) )
63 62 rabbidv ⊢ ( 𝑖 = 𝑁 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
64 fvoveq1 ⊢ ( 𝑖 = 𝑁 → ( log ‘ ( 𝑖 / 𝑑 ) ) = ( log ‘ ( 𝑁 / 𝑑 ) ) )
65 64 oveq1d ⊢ ( 𝑖 = 𝑁 → ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) = ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) )
66 65 oveq2d ⊢ ( 𝑖 = 𝑁 → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) )
67 66 adantr ⊢ ( ( 𝑖 = 𝑁 ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) )
68 63 67 sumeq12dv ⊢ ( 𝑖 = 𝑁 → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑖 / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) )
69 61 68 eqtrid ⊢ ( 𝑖 = 𝑁 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) )
70 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ⊆ ℕ
71 dvdsdivcl ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ) → ( 𝑖 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } )
72 70 71 sselid ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ) → ( 𝑖 / 𝑗 ) ∈ ℕ )
73 fveq2 ⊢ ( 𝑛 = ( 𝑖 / 𝑗 ) → ( log ‘ 𝑛 ) = ( log ‘ ( 𝑖 / 𝑗 ) ) )
74 73 oveq1d ⊢ ( 𝑛 = ( 𝑖 / 𝑗 ) → ( ( log ‘ 𝑛 ) ↑ 2 ) = ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) )
75 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) )
76 ovex ⊢ ( ( log ‘ 𝑛 ) ↑ 2 ) ∈ V
77 74 75 76 fvmpt3i ⊢ ( ( 𝑖 / 𝑗 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) = ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) )
78 72 77 syl ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ) → ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) = ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) )
79 78 oveq2d ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ) → ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) = ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) )
80 79 sumeq2dv ⊢ ( 𝑖 ∈ ℕ → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) = Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) )
81 80 mpteq2ia ⊢ ( 𝑖 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) )
82 sumex ⊢ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( log ‘ ( 𝑖 / 𝑗 ) ) ↑ 2 ) ) ∈ V
83 69 81 82 fvmpt3i ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑖 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑖 } ( ( μ ‘ 𝑗 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( log ‘ 𝑛 ) ↑ 2 ) ) ‘ ( 𝑖 / 𝑗 ) ) ) ) ‘ 𝑁 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) )
84 44 55 83 3eqtr3rd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑁 / 𝑑 ) ) ↑ 2 ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑁 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )