Theorem selberg2

Description: Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

	Ref	Expression
Assertion	selberg2	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
3	1 2	ssexi	$$⊢{ℝ}^{+}\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to {ℝ}^{+}\in \mathrm{V}$$
5		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\in \mathrm{V}$$
6		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\in \mathrm{V}$$
7		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)$$
8		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)$$
9	4 5 6 7 8	offval2	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\right)$$
10	9	mptru	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\right)$$
11		fzfid	$$⊢x\in {ℝ}^{+}\to \left(1\dots ⌊x⌋\right)\in \mathrm{Fin}$$
12		elfznn	$$⊢n\in \left(1\dots ⌊x⌋\right)\to n\in \mathbb{N}$$
13	12	adantl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to n\in \mathbb{N}$$
14		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
15	13 14	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\in ℝ$$
16	15	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\in ℂ$$
17	13	nnrpd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to n\in {ℝ}^{+}$$
18		relogcl	$$⊢n\in {ℝ}^{+}\to \log n\in ℝ$$
19	17 18	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \log n\in ℝ$$
20	19	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \log n\in ℂ$$
21		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
22		nndivre	$$⊢\left(x\in ℝ\wedge n\in \mathbb{N}\right)\to \frac{x}{n}\in ℝ$$
23	21 12 22	syl2an	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{n}\in ℝ$$
24		chpcl	$$⊢\frac{x}{n}\in ℝ\to \psi \left(\frac{x}{n}\right)\in ℝ$$
25	23 24	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \psi \left(\frac{x}{n}\right)\in ℝ$$
26	25	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \psi \left(\frac{x}{n}\right)\in ℂ$$
27	20 26	addcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \log n+\psi \left(\frac{x}{n}\right)\in ℂ$$
28	16 27	mulcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)\in ℂ$$
29	11 28	fsumcl	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)\in ℂ$$
30		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
31		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
32	29 30 31	divcld	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\in ℂ$$
33		2cn	$$⊢2\in ℂ$$
34		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
35	34	recnd	$$⊢x\in {ℝ}^{+}\to \log x\in ℂ$$
36		mulcl	$$⊢\left(2\in ℂ\wedge \log x\in ℂ\right)\to 2\log x\in ℂ$$
37	33 35 36	sylancr	$$⊢x\in {ℝ}^{+}\to 2\log x\in ℂ$$
38	16 20	mulcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\log n\in ℂ$$
39	11 38	fsumcl	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n\in ℂ$$
40		chpcl	$$⊢x\in ℝ\to \psi \left(x\right)\in ℝ$$
41	21 40	syl	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\in ℝ$$
42	41	recnd	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\in ℂ$$
43	42 35	mulcld	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\log x\in ℂ$$
44	39 43	subcld	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\in ℂ$$
45	44 30 31	divcld	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\in ℂ$$
46	32 37 45	sub32d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)-2\log x$$
47		rpcnne0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℂ\wedge x\ne 0\right)$$
48		divsubdir	$$⊢\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)\in ℂ\wedge \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\in ℂ\wedge \left(x\in ℂ\wedge x\ne 0\right)\right)\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)}{x}=\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)$$
49	29 44 47 48	syl3anc	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)}{x}=\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)$$
50	16 20 26	adddid	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)=\Lambda \left(n\right)\log n+\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)$$
51	50	sumeq2dv	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)=\sum _{n=1}^{⌊x⌋}\left(\Lambda \left(n\right)\log n+\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)\right)$$
52	16 26	mulcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\psi \left(\frac{x}{n}\right)\in ℂ$$
53	11 38 52	fsumadd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\Lambda \left(n\right)\log n+\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)$$
54	51 53	eqtrd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)$$
55	54	oveq1d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)$$
56	11 52	fsumcl	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)\in ℂ$$
57	39 56 43	pnncand	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)+\psi \left(x\right)\log x$$
58	56 43	addcomd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)+\psi \left(x\right)\log x=\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)$$
59	55 57 58	3eqtrd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)=\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)$$
60	59	oveq1d	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)-\left(\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x\right)}{x}=\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}$$
61	49 60	eqtr3d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}$$
62	61	oveq1d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)-2\log x=\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x$$
63	46 62	eqtrd	$$⊢x\in {ℝ}^{+}\to \left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x$$
64	63	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x-\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x\right)$$
65	10 64	eqtri	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x\right)$$
66		selberg	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$
67		selberg2lem	$$⊢\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\in 𝑂\left(1\right)$$
68		o1sub	$$⊢\left(\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)\wedge \left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\in 𝑂\left(1\right)\right)\to \left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\in 𝑂\left(1\right)$$
69	66 67 68	mp2an	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right){-}_f\left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\log n-\psi \left(x\right)\log x}{x}\right)\in 𝑂\left(1\right)$$
70	65 69	eqeltrri	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\psi \left(x\right)\log x+\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\psi \left(\frac{x}{n}\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$