Theorem selbergr

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of Shapiro, p. 428. (Contributed by Mario Carneiro, 16-Apr-2016)

	Ref	Expression
Hypothesis	pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion	selbergr	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		reex	⊢ ℝ ∈ V
3		rpssre	⊢ ℝ+ ⊆ ℝ
4	2 3	ssexi	⊢ ℝ+ ∈ V
5	4	a1i	⊢ ( ⊤ → ℝ+ ∈ V )
6		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ V )
7		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ∈ V )
8		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
9		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
10	5 6 7 8 9	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) )
11	10	mptru	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
12	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
13	12	ffvelcdmi	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
14	13	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
15		relogcl	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
16	15	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
17	14 16	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
18		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
20	19	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
21		vmacl	⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
22	20 21	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
23	22	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℂ )
24		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
25		nndivre	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
26	24 19 25	syl2an	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
27		chpcl	⊢ ( ( 𝑥 / 𝑑 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ )
28	26 27	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ )
29	28	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℂ )
30	23 29	mulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ ℂ )
31	18 30	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ ℂ )
32	17 31	addcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ )
33		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
34		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
35	32 33 34	divcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ∈ ℂ )
36	22 20	nndivred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
37	36	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
38	18 37	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
39	35 38 16	nnncan2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
40		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
41	24 40	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
42	41	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℂ )
43	42 16	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
44	43 31	addcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ )
45	44 33 34	divcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ∈ ℂ )
46	45 16 16	subsub4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) ) )
47	1	pntrval	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) = ( ( ψ ‘ 𝑥 ) − 𝑥 ) )
48	47	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) · ( log ‘ 𝑥 ) ) )
49	42 33 16	subdird	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
50	48 49	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
51	50	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
52	33 16	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
53	43 31 52	addsubd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
54	51 53	eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
55	54	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
56		rpcnne0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
57		divsubdir	⊢ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ ∧ ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) )
58	44 52 56 57	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) )
59	16 33 34	divcan3d	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) = ( log ‘ 𝑥 ) )
60	59	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) )
61	55 58 60	3eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) )
62	61	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( log ‘ 𝑥 ) ) )
63	16	2timesd	⊢ ( 𝑥 ∈ ℝ+ → ( 2 · ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) )
64	63	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) ) )
65	46 62 64	3eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
66	65	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
67	33 38	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
68		divsubdir	⊢ ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ ∧ ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) )
69	32 67 56 68	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) )
70	17 31 67	addsubassd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) ) )
71	33	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
72	71 37	mulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
73	18 30 72	fsumsub	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
74	26	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℂ )
75	23 29 74	subdid	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) ) )
76	19	nnrpd	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
77		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
78	76 77	sylan2	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
79	1	pntrval	⊢ ( ( 𝑥 / 𝑑 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) )
80	78 79	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) )
81	80	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) ) )
82	20	nnrpd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
83		rpcnne0	⊢ ( 𝑑 ∈ ℝ+ → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
84	82 83	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
85		div12	⊢ ( ( 𝑥 ∈ ℂ ∧ ( Λ ‘ 𝑑 ) ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) )
86	71 23 84 85	syl3anc	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) )
87	86	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) ) )
88	75 81 87	3eqtr4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
89	88	sumeq2dv	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
90	18 33 37	fsummulc2	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
91	90	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
92	73 89 91	3eqtr4rd	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) )
93	92	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) )
94	70 93	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) )
95	94	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
96	38 33 34	divcan3d	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) )
97	96	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
98	69 95 97	3eqtr3rd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
99	39 66 98	3eqtr3d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
100	99	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
101	11 100	eqtri	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
102		selberg2	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
103		vmadivsum	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
104		o1sub	⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
105	102 103 104	mp2an	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
106	101 105	eqeltrri	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)