Metamath Proof Explorer

Theorem logsqvma

Description: A formula for log ^ 2 ( N ) in terms of the primes. Equation 10.4.6 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

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

Proof

Step Hyp Ref Expression
1 dvdsfi ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
2 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... 𝑑 ) ∈ Fin )
3 elrabi ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑑 ∈ ℕ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑑 ∈ ℕ )
5 dvdsssfz1 ⊢ ( 𝑑 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ⊆ ( 1 ... 𝑑 ) )
6 4 5 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ⊆ ( 1 ... 𝑑 ) )
7 2 6 ssfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ∈ Fin )
8 elrabi ⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } → 𝑢 ∈ ℕ )
9 8 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑢 ∈ ℕ )
10 vmacl ⊢ ( 𝑢 ∈ ℕ → ( Λ ‘ 𝑢 ) ∈ ℝ )
11 9 10 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( Λ ‘ 𝑢 ) ∈ ℝ )
12 breq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ∥ 𝑑 ↔ 𝑢 ∥ 𝑑 ) )
13 12 elrab ⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ↔ ( 𝑢 ∈ ℕ ∧ 𝑢 ∥ 𝑑 ) )
14 13 simprbi ⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } → 𝑢 ∥ 𝑑 )
15 14 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑢 ∥ 𝑑 )
16 3 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑑 ∈ ℕ )
17 nndivdvds ⊢ ( ( 𝑑 ∈ ℕ ∧ 𝑢 ∈ ℕ ) → ( 𝑢 ∥ 𝑑 ↔ ( 𝑑 / 𝑢 ) ∈ ℕ ) )
18 16 9 17 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( 𝑢 ∥ 𝑑 ↔ ( 𝑑 / 𝑢 ) ∈ ℕ ) )
19 15 18 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( 𝑑 / 𝑢 ) ∈ ℕ )
20 vmacl ⊢ ( ( 𝑑 / 𝑢 ) ∈ ℕ → ( Λ ‘ ( 𝑑 / 𝑢 ) ) ∈ ℝ )
21 19 20 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( Λ ‘ ( 𝑑 / 𝑢 ) ) ∈ ℝ )
22 11 21 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
24 23 anassrs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
25 7 24 fsumcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
26 vmacl ⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
27 4 26 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
28 4 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑑 ∈ ℝ+ )
29 28 relogcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑑 ) ∈ ℝ )
30 27 29 remulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℂ )
32 1 25 31 fsumadd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
33 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
34 fvoveq1 ⊢ ( 𝑑 = ( 𝑢 · 𝑘 ) → ( Λ ‘ ( 𝑑 / 𝑢 ) ) = ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) )
35 34 oveq2d ⊢ ( 𝑑 = ( 𝑢 · 𝑘 ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
36 33 35 23 fsumdvdscom ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
37 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ℕ
38 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } )
39 37 38 sselid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ ℕ )
40 39 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ ℂ )
41 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
42 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
43 41 42 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℕ )
44 43 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℂ )
45 44 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑢 ∈ ℂ )
46 43 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ≠ 0 )
47 46 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑢 ≠ 0 )
48 40 45 47 divcan3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( ( 𝑢 · 𝑘 ) / 𝑢 ) = 𝑘 )
49 48 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = ( Λ ‘ 𝑘 ) )
50 49 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) )
51 dvdsdivcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑢 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
52 41 51 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑢 ) ∈ ℕ )
53 vmasum ⊢ ( ( 𝑁 / 𝑢 ) ∈ ℕ → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) = ( log ‘ ( 𝑁 / 𝑢 ) ) )
54 52 53 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) = ( log ‘ ( 𝑁 / 𝑢 ) ) )
55 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
56 55 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑁 ∈ ℝ+ )
57 43 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℝ+ )
58 56 57 relogdivd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ ( 𝑁 / 𝑢 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) )
59 50 54 58 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) )
60 59 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = ( ( Λ ‘ 𝑢 ) · ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) ) )
61 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... ( 𝑁 / 𝑢 ) ) ∈ Fin )
62 dvdsssfz1 ⊢ ( ( 𝑁 / 𝑢 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ( 1 ... ( 𝑁 / 𝑢 ) ) )
63 52 62 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ( 1 ... ( 𝑁 / 𝑢 ) ) )
64 61 63 ssfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ∈ Fin )
65 43 10 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑢 ) ∈ ℝ )
66 65 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑢 ) ∈ ℂ )
67 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
68 39 67 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
69 68 recnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
70 49 69 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ∈ ℂ )
71 64 66 70 fsummulc2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
72 relogcl ⊢ ( 𝑁 ∈ ℝ+ → ( log ‘ 𝑁 ) ∈ ℝ )
73 72 recnd ⊢ ( 𝑁 ∈ ℝ+ → ( log ‘ 𝑁 ) ∈ ℂ )
74 56 73 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑁 ) ∈ ℂ )
75 57 relogcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑢 ) ∈ ℝ )
76 75 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑢 ) ∈ ℂ )
77 66 74 76 subdid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) ) = ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
78 60 71 77 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
79 78 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
80 66 74 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) ∈ ℂ )
81 66 76 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ∈ ℂ )
82 1 80 81 fsumsub ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
83 55 73 syl ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℂ )
84 83 sqvald ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 𝑁 ) ↑ 2 ) = ( ( log ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) )
85 vmasum ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) = ( log ‘ 𝑁 ) )
86 85 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = ( ( log ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) )
87 1 83 66 fsummulc1 ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) )
88 84 86 87 3eqtr2rd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )
89 fveq2 ⊢ ( 𝑢 = 𝑑 → ( Λ ‘ 𝑢 ) = ( Λ ‘ 𝑑 ) )
90 fveq2 ⊢ ( 𝑢 = 𝑑 → ( log ‘ 𝑢 ) = ( log ‘ 𝑑 ) )
91 89 90 oveq12d ⊢ ( 𝑢 = 𝑑 → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) )
92 91 cbvsumv ⊢ Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) )
93 92 a1i ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) )
94 88 93 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
95 82 94 eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
96 36 79 95 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
97 96 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
98 83 sqcld ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 𝑁 ) ↑ 2 ) ∈ ℂ )
99 1 31 fsumcl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℂ )
100 98 99 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )
101 32 97 100 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )