selberg

Description: Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that sum_ n <_ x , Lam ( n ) log n + sum_ m x. n <_ x , Lam ( m ) Lam ( n ) = 2 x log x + O ( x ) . Equation 10.4.10 of Shapiro, p. 419. (Contributed by Mario Carneiro, 23-May-2016)

		Ref	Expression
	Assertion	selberg	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑛 = 𝑑 → ( Λ ‘ 𝑛 ) = ( Λ ‘ 𝑑 ) )
2		oveq2	⊢ ( 𝑛 = 𝑑 → ( 𝑥 / 𝑛 ) = ( 𝑥 / 𝑑 ) )
3	2	fveq2d	⊢ ( 𝑛 = 𝑑 → ( ψ ‘ ( 𝑥 / 𝑛 ) ) = ( ψ ‘ ( 𝑥 / 𝑑 ) ) )
4	1 3	oveq12d	⊢ ( 𝑛 = 𝑑 → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) )
5	4	cbvsumv	⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) )
6		fzfid	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ Fin )
7		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
8	7	adantl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
9		vmacl	⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
10	8 9	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
11	10	recnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℂ )
12		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
13	12	adantl	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
14		vmacl	⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
15	13 14	syl	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
16	15	recnd	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
17	6 11 16	fsummulc2	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( Λ ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ 𝑚 ) ) )
18	7	nnrpd	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ⁺ )
19		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺ ) → ( 𝑥 / 𝑑 ) ∈ ℝ⁺ )
20	18 19	sylan2	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ⁺ )
21	20	rpred	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
22		chpval	⊢ ( ( 𝑥 / 𝑑 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑑 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( Λ ‘ 𝑚 ) )
23	21 22	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑑 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( Λ ‘ 𝑚 ) )
24	23	oveq2d	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( Λ ‘ 𝑚 ) ) )
25	13	nncnd	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
26	7	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℕ )
27	26	nncnd	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
28	26	nnne0d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
29	25 27 28	divcan3d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑑 · 𝑚 ) / 𝑑 ) = 𝑚 )
30	29	fveq2d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) = ( Λ ‘ 𝑚 ) )
31	30	oveq2d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ 𝑚 ) ) )
32	31	sumeq2dv	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ 𝑚 ) ) )
33	17 24 32	3eqtr4d	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
34	33	sumeq2dv	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
35	5 34	syl5eq	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
36		fvoveq1	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( Λ ‘ ( 𝑛 / 𝑑 ) ) = ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) )
37	36	oveq2d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
38		rpre	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ )
39		ssrab2	⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ℕ
40		simprr	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
41	39 40	sselid	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ ℕ )
42	41	anassrs	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → 𝑑 ∈ ℕ )
43	42 9	syl	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
44		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
45	44	adantl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
46		dvdsdivcl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑑 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
47	45 46	sylan	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑑 ) ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
48	39 47	sselid	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( 𝑛 / 𝑑 ) ∈ ℕ )
49		vmacl	⊢ ( ( 𝑛 / 𝑑 ) ∈ ℕ → ( Λ ‘ ( 𝑛 / 𝑑 ) ) ∈ ℝ )
50	48 49	syl	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( Λ ‘ ( 𝑛 / 𝑑 ) ) ∈ ℝ )
51	43 50	remulcld	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℝ )
52	51	recnd	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
53	52	anasss	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
54	37 38 53	dvdsflsumcom	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
55	35 54	eqtr4d	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) )
56	55	oveq1d	⊢ ( 𝑥 ∈ ℝ⁺ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
57		fzfid	⊢ ( 𝑥 ∈ ℝ⁺ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
58		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
59	45 58	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
60	59	recnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
61	44	nnrpd	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ⁺ )
62		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺ ) → ( 𝑥 / 𝑛 ) ∈ ℝ⁺ )
63	61 62	sylan2	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ⁺ )
64	63	rpred	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
65		chpcl	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
66	64 65	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
67	66	recnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
68	60 67	mulcld	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
69	45	nnrpd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ⁺ )
70		relogcl	⊢ ( 𝑛 ∈ ℝ⁺ → ( log ‘ 𝑛 ) ∈ ℝ )
71	69 70	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
72	71	recnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
73	60 72	mulcld	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
74	57 68 73	fsumadd	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
75		fzfid	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
76		dvdsssfz1	⊢ ( 𝑛 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
77	45 76	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
78	75 77	ssfid	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ∈ Fin )
79	78 51	fsumrecl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℝ )
80	79	recnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
81	57 80 73	fsumadd	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
82	56 74 81	3eqtr4d	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
83	72 67	addcomd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( log ‘ 𝑛 ) ) )
84	83	oveq2d	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( log ‘ 𝑛 ) ) ) )
85	60 67 72	adddid	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( log ‘ 𝑛 ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
86	84 85	eqtrd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
87	86	sumeq2dv	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
88		logsqvma2	⊢ ( 𝑛 ∈ ℕ → Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = ( Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
89	45 88	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = ( Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
90	89	sumeq2dv	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( Λ ‘ 𝑑 ) · ( Λ ‘ ( 𝑛 / 𝑑 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
91	82 87 90	3eqtr4d	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) )
92		fvoveq1	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( log ‘ ( 𝑛 / 𝑑 ) ) = ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) )
93	92	oveq1d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) = ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) )
94	93	oveq2d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) )
95		mucl	⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
96	41 95	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
97	96	zcnd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
98	61	ad2antrl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑛 ∈ ℝ⁺ )
99	41	nnrpd	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ ℝ⁺ )
100	98 99	rpdivcld	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( 𝑛 / 𝑑 ) ∈ ℝ⁺ )
101		relogcl	⊢ ( ( 𝑛 / 𝑑 ) ∈ ℝ⁺ → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℝ )
102	101	recnd	⊢ ( ( 𝑛 / 𝑑 ) ∈ ℝ⁺ → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
103	100 102	syl	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
104	103	sqcld	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ∈ ℂ )
105	97 104	mulcld	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) ∈ ℂ )
106	94 38 105	dvdsflsumcom	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) )
107	29	fveq2d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) = ( log ‘ 𝑚 ) )
108	107	oveq1d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) = ( ( log ‘ 𝑚 ) ↑ 2 ) )
109	108	oveq2d	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
110	109	sumeq2dv	⊢ ( ( 𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
111	110	sumeq2dv	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
112	91 106 111	3eqtrd	⊢ ( 𝑥 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
113	112	oveq1d	⊢ ( 𝑥 ∈ ℝ⁺ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) )
114	113	oveq1d	⊢ ( 𝑥 ∈ ℝ⁺ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
115	114	mpteq2ia	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
116		eqid	⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑑 ) ) ) ) ) / 𝑑 ) = ( ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑑 ) ) ) ) ) / 𝑑 )
117	116	selberglem2	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
118	115 117	eqeltri	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Metamath Proof Explorer

Theorem selberg

Proof