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	eqtrid	⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 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 ‘ 𝑛 ) ) + Σ 𝑚 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑚 ) · ( Λ ‘ ( 𝑛 / 𝑚 ) ) ) ) )