Metamath Proof Explorer

Theorem pntsval2

Description: The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypothesis pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
Assertion pntsval2 ( 𝐴 ∈ ℝ → ( 𝑆 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2 1 pntsval ⊢ ( 𝐴 ∈ ℝ → ( 𝑆 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )
3 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
5 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
7 6 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
8 4 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ+ )
9 8 relogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
10 9 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
11 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
12 11 4 nndivred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ )
13 chpcl ⊢ ( ( 𝐴 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝐴 / 𝑛 ) ) ∈ ℝ )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ψ ‘ ( 𝐴 / 𝑛 ) ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ψ ‘ ( 𝐴 / 𝑛 ) ) ∈ ℂ )
16 7 10 15 adddid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )
17 16 sumeq2dv ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )
18 fveq2 ⊢ ( 𝑛 = 𝑚 → ( Λ ‘ 𝑛 ) = ( Λ ‘ 𝑚 ) )
19 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐴 / 𝑛 ) = ( 𝐴 / 𝑚 ) )
20 19 fveq2d ⊢ ( 𝑛 = 𝑚 → ( ψ ‘ ( 𝐴 / 𝑛 ) ) = ( ψ ‘ ( 𝐴 / 𝑚 ) ) )
21 18 20 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) ) )
22 21 cbvsumv ⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) )
23 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ∈ Fin )
24 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
25 24 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
26 vmacl ⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
27 25 26 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
28 27 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
29 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) → 𝑘 ∈ ℕ )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → 𝑘 ∈ ℕ )
31 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
32 30 31 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
34 23 28 33 fsummulc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( Λ ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) )
35 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
36 35 25 nndivred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑚 ) ∈ ℝ )
37 chpval ⊢ ( ( 𝐴 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝐴 / 𝑚 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( Λ ‘ 𝑘 ) )
38 36 37 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ψ ‘ ( 𝐴 / 𝑚 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( Λ ‘ 𝑘 ) )
39 38 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( Λ ‘ 𝑘 ) ) )
40 30 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → 𝑘 ∈ ℂ )
41 24 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → 𝑚 ∈ ℕ )
42 41 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → 𝑚 ∈ ℂ )
43 41 nnne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → 𝑚 ≠ 0 )
44 40 42 43 divcan3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( ( 𝑚 · 𝑘 ) / 𝑚 ) = 𝑘 )
45 44 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) = ( Λ ‘ 𝑘 ) )
46 45 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) )
47 46 sumeq2dv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ 𝑘 ) ) )
48 34 39 47 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) )
49 48 sumeq2dv ⊢ ( 𝐴 ∈ ℝ → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) )
50 fvoveq1 ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) = ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) )
51 50 oveq2d ⊢ ( 𝑛 = ( 𝑚 · 𝑘 ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) )
52 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
53 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ℕ
54 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
55 53 54 sselid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑚 ∈ ℕ )
56 55 26 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
57 dvdsdivcl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
58 4 57 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
59 53 58 sselid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑚 ) ∈ ℕ )
60 vmacl ⊢ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
61 59 60 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ ( 𝑛 / 𝑚 ) ) ∈ ℝ )
62 56 61 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
63 62 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
64 63 anasss ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
65 51 52 64 dvdsflsumcom ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( ( 𝑚 · 𝑘 ) / 𝑚 ) ) ) )
66 49 65 eqtr4d ⊢ ( 𝐴 ∈ ℝ → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝐴 / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
67 22 66 syl5eq ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) )
68 67 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
69 fzfid ⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
70 7 10 mulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
71 7 15 mulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ∈ ℂ )
72 69 70 71 fsumadd ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )
73 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
74 dvdsssfz1 ⊢ ( 𝑛 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
75 4 74 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
76 73 75 ssfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ∈ Fin )
77 76 62 fsumrecl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℝ )
78 77 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ∈ ℂ )
79 69 70 78 fsumadd ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
80 68 72 79 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )
81 2 17 80 3eqtrd ⊢ ( 𝐴 ∈ ℝ → ( 𝑆 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )