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	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
Assertion	selbergr	$$⊢\left(x\in {ℝ}^{+}⟼\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
2		reex	$$⊢ℝ\in \mathrm{V}$$
3		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
4	2 3	ssexi	$$⊢{ℝ}^{+}\in \mathrm{V}$$
5	4	a1i	$$⊢\top \to {ℝ}^{+}\in \mathrm{V}$$
6		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\in \mathrm{V}$$
7		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\in \mathrm{V}$$
8		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right)$$
9		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)$$
10	5 6 7 8 9	offval2	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\right)$$
11	10	mptru	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\right)$$
12	1	pntrf	$$⊢R:{ℝ}^{+}⟶ℝ$$
13	12	ffvelcdmi	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\in ℝ$$
14	13	recnd	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\in ℂ$$
15		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
16	15	recnd	$$⊢x\in {ℝ}^{+}\to \log x\in ℂ$$
17	14 16	mulcld	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x\in ℂ$$
18		fzfid	$$⊢x\in {ℝ}^{+}\to \left(1\dots ⌊x⌋\right)\in \mathrm{Fin}$$
19		elfznn	$$⊢d\in \left(1\dots ⌊x⌋\right)\to d\in \mathbb{N}$$
20	19	adantl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to d\in \mathbb{N}$$
21		vmacl	$$⊢d\in \mathbb{N}\to \Lambda \left(d\right)\in ℝ$$
22	20 21	syl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)\in ℝ$$
23	22	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)\in ℂ$$
24		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
25		nndivre	$$⊢\left(x\in ℝ\wedge d\in \mathbb{N}\right)\to \frac{x}{d}\in ℝ$$
26	24 19 25	syl2an	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{d}\in ℝ$$
27		chpcl	$$⊢\frac{x}{d}\in ℝ\to \psi \left(\frac{x}{d}\right)\in ℝ$$
28	26 27	syl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \psi \left(\frac{x}{d}\right)\in ℝ$$
29	28	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \psi \left(\frac{x}{d}\right)\in ℂ$$
30	23 29	mulcld	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ$$
31	18 30	fsumcl	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ$$
32	17 31	addcld	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ$$
33		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
34		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
35	32 33 34	divcld	$$⊢x\in {ℝ}^{+}\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\in ℂ$$
36	22 20	nndivred	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \frac{\Lambda \left(d\right)}{d}\in ℝ$$
37	36	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \frac{\Lambda \left(d\right)}{d}\in ℂ$$
38	18 37	fsumcl	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)\in ℂ$$
39	35 38 16	nnncan2d	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)$$
40		chpcl	$$⊢x\in ℝ\to \psi \left(x\right)\in ℝ$$
41	24 40	syl	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\in ℝ$$
42	41	recnd	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\in ℂ$$
43	42 16	mulcld	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\log x\in ℂ$$
44	43 31	addcld	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ$$
45	44 33 34	divcld	$$⊢x\in {ℝ}^{+}\to \frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\in ℂ$$
46	45 16 16	subsub4d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x-\log x=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\log x+\log x\right)$$
47	1	pntrval	$$⊢x\in {ℝ}^{+}\to R\left(x\right)=\psi \left(x\right)-x$$
48	47	oveq1d	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x=\left(\psi \left(x\right)-x\right)\log x$$
49	42 33 16	subdird	$$⊢x\in {ℝ}^{+}\to \left(\psi \left(x\right)-x\right)\log x=\psi \left(x\right)\log x-x\log x$$
50	48 49	eqtrd	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x=\psi \left(x\right)\log x-x\log x$$
51	50	oveq1d	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)=\psi \left(x\right)\log x-x\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)$$
52	33 16	mulcld	$$⊢x\in {ℝ}^{+}\to x\log x\in ℂ$$
53	43 31 52	addsubd	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\log x=\psi \left(x\right)\log x-x\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)$$
54	51 53	eqtr4d	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)=\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\log x$$
55	54	oveq1d	$$⊢x\in {ℝ}^{+}\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}=\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\log x}{x}$$
56		rpcnne0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℂ\wedge x\ne 0\right)$$
57		divsubdir	$$⊢\left(\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ\wedge x\log x\in ℂ\wedge \left(x\in ℂ\wedge x\ne 0\right)\right)\to \frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\log x}{x}=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\log x}{x}\right)$$
58	44 52 56 57	syl3anc	$$⊢x\in {ℝ}^{+}\to \frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\log x}{x}=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\log x}{x}\right)$$
59	16 33 34	divcan3d	$$⊢x\in {ℝ}^{+}\to \frac{x\log x}{x}=\log x$$
60	59	oveq2d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\log x}{x}\right)=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x$$
61	55 58 60	3eqtrd	$$⊢x\in {ℝ}^{+}\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x$$
62	61	oveq1d	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x-\log x$$
63	16	2timesd	$$⊢x\in {ℝ}^{+}\to 2\log x=\log x+\log x$$
64	63	oveq2d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\log x+\log x\right)$$
65	46 62 64	3eqtr4d	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x$$
66	65	oveq1d	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)$$
67	33 38	mulcld	$$⊢x\in {ℝ}^{+}\to x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)\in ℂ$$
68		divsubdir	$$⊢\left(R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)\in ℂ\wedge x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)\in ℂ\wedge \left(x\in ℂ\wedge x\ne 0\right)\right)\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}=\left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}\right)$$
69	32 67 56 68	syl3anc	$$⊢x\in {ℝ}^{+}\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}=\left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}\right)$$
70	17 31 67	addsubassd	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)$$
71	33	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to x\in ℂ$$
72	71 37	mulcld	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to x\left(\frac{\Lambda \left(d\right)}{d}\right)\in ℂ$$
73	18 30 72	fsumsub	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\left(\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\left(\frac{\Lambda \left(d\right)}{d}\right)\right)=\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-\sum _{d=1}^{⌊x⌋}x\left(\frac{\Lambda \left(d\right)}{d}\right)$$
74	26	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{d}\in ℂ$$
75	23 29 74	subdid	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)\left(\psi \left(\frac{x}{d}\right)-\left(\frac{x}{d}\right)\right)=\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-\Lambda \left(d\right)\left(\frac{x}{d}\right)$$
76	19	nnrpd	$$⊢d\in \left(1\dots ⌊x⌋\right)\to d\in {ℝ}^{+}$$
77		rpdivcl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in {ℝ}^{+}\right)\to \frac{x}{d}\in {ℝ}^{+}$$
78	76 77	sylan2	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{d}\in {ℝ}^{+}$$
79	1	pntrval	$$⊢\frac{x}{d}\in {ℝ}^{+}\to R\left(\frac{x}{d}\right)=\psi \left(\frac{x}{d}\right)-\left(\frac{x}{d}\right)$$
80	78 79	syl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to R\left(\frac{x}{d}\right)=\psi \left(\frac{x}{d}\right)-\left(\frac{x}{d}\right)$$
81	80	oveq2d	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)R\left(\frac{x}{d}\right)=\Lambda \left(d\right)\left(\psi \left(\frac{x}{d}\right)-\left(\frac{x}{d}\right)\right)$$
82	20	nnrpd	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to d\in {ℝ}^{+}$$
83		rpcnne0	$$⊢d\in {ℝ}^{+}\to \left(d\in ℂ\wedge d\ne 0\right)$$
84	82 83	syl	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \left(d\in ℂ\wedge d\ne 0\right)$$
85		div12	$$⊢\left(x\in ℂ\wedge \Lambda \left(d\right)\in ℂ\wedge \left(d\in ℂ\wedge d\ne 0\right)\right)\to x\left(\frac{\Lambda \left(d\right)}{d}\right)=\Lambda \left(d\right)\left(\frac{x}{d}\right)$$
86	71 23 84 85	syl3anc	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to x\left(\frac{\Lambda \left(d\right)}{d}\right)=\Lambda \left(d\right)\left(\frac{x}{d}\right)$$
87	86	oveq2d	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\left(\frac{\Lambda \left(d\right)}{d}\right)=\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-\Lambda \left(d\right)\left(\frac{x}{d}\right)$$
88	75 81 87	3eqtr4d	$$⊢\left(x\in {ℝ}^{+}\wedge d\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(d\right)R\left(\frac{x}{d}\right)=\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\left(\frac{\Lambda \left(d\right)}{d}\right)$$
89	88	sumeq2dv	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)=\sum _{d=1}^{⌊x⌋}\left(\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\left(\frac{\Lambda \left(d\right)}{d}\right)\right)$$
90	18 33 37	fsummulc2	$$⊢x\in {ℝ}^{+}\to x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=\sum _{d=1}^{⌊x⌋}x\left(\frac{\Lambda \left(d\right)}{d}\right)$$
91	90	oveq2d	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-\sum _{d=1}^{⌊x⌋}x\left(\frac{\Lambda \left(d\right)}{d}\right)$$
92	73 89 91	3eqtr4rd	$$⊢x\in {ℝ}^{+}\to \sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)$$
93	92	oveq2d	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)$$
94	70 93	eqtrd	$$⊢x\in {ℝ}^{+}\to R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)$$
95	94	oveq1d	$$⊢x\in {ℝ}^{+}\to \frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)-x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}=\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}$$
96	38 33 34	divcan3d	$$⊢x\in {ℝ}^{+}\to \frac{x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}=\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)$$
97	96	oveq2d	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\left(\frac{x\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)}{x}\right)=\left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)$$
98	69 95 97	3eqtr3rd	$$⊢x\in {ℝ}^{+}\to \left(\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)=\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}$$
99	39 66 98	3eqtr3d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}$$
100	99	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x-\left(\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\right)=\left(x\in {ℝ}^{+}⟼\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}\right)$$
101	11 100	eqtri	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)=\left(x\in {ℝ}^{+}⟼\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}\right)$$
102		selberg2	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$
103		vmadivsum	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\in 𝑂\left(1\right)$$
104		o1sub	$$⊢\left(\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)\wedge \left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\in 𝑂\left(1\right)\right)\to \left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\in 𝑂\left(1\right)$$
105	102 103 104	mp2an	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)\psi \left(\frac{x}{d}\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\sum _{d=1}^{⌊x⌋}\left(\frac{\Lambda \left(d\right)}{d}\right)-\log x\right)\in 𝑂\left(1\right)$$
106	101 105	eqeltrri	$$⊢\left(x\in {ℝ}^{+}⟼\frac{R\left(x\right)\log x+\sum _{d=1}^{⌊x⌋}\Lambda \left(d\right)R\left(\frac{x}{d}\right)}{x}\right)\in 𝑂\left(1\right)$$