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