# Metamath Proof Explorer

## 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)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\in \mathrm{V}$
6 ovexd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\in \mathrm{V}$
7 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right)$
8 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)\right)$
10 9 mptru ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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 ℕ$
13 12 adantl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℕ$
14 vmacl ${⊢}{n}\in ℕ\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 \mathrm{log}{n}\in ℝ$
19 17 18 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\in ℝ$
20 19 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\in ℂ$
21 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
22 nndivre ${⊢}\left({x}\in ℝ\wedge {n}\in ℕ\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 \mathrm{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(\mathrm{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(\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\in ℂ$
33 2cn ${⊢}2\in ℂ$
34 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
35 34 recnd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℂ$
36 mulcl ${⊢}\left(2\in ℂ\wedge \mathrm{log}{x}\in ℂ\right)\to 2\mathrm{log}{x}\in ℂ$
37 33 35 36 sylancr ${⊢}{x}\in {ℝ}^{+}\to 2\mathrm{log}{x}\in ℂ$
38 16 20 mulcld ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\mathrm{log}{n}\in ℂ$
39 11 38 fsumcl ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{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)\mathrm{log}{x}\in ℂ$
44 39 43 subcld ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\in ℂ$
45 44 30 31 divcld ${⊢}{x}\in {ℝ}^{+}\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\in ℂ$
46 32 37 45 sub32d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)-2\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)\in ℂ\wedge \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)-\left(\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)}{{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)$
49 29 44 47 48 syl3anc ${⊢}{x}\in {ℝ}^{+}\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)-\left(\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)}{{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)=\Lambda \left({n}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\Lambda \left({n}\right)\mathrm{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)\mathrm{log}{n}+\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)-\left(\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{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)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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)\mathrm{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)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)+\psi \left({x}\right)\mathrm{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)\mathrm{log}{x}=\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)-\left(\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)=\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)-\left(\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}\right)}{{x}}=\frac{\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\frac{\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)-2\mathrm{log}{x}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{log}{x}$
63 46 62 eqtrd ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{log}{x}$
64 63 mpteq2ia ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)$
65 10 64 eqtri ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)$
66 selberg ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
67 selberg2lem ${⊢}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)\wedge \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)\in 𝑂\left(1\right)\right)\to \left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{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(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}\right)\in 𝑂\left(1\right)$
70 65 69 eqeltrri ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$