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