# Metamath Proof Explorer

## 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)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{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)-\mathrm{log}{x}\in \mathrm{V}$
8 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)$
9 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)$
10 5 6 7 8 9 offval2 ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\right)$
11 10 mptru ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\right)$
12 1 pntrf ${⊢}{R}:{ℝ}^{+}⟶ℝ$
13 12 ffvelrni ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\in ℝ$
14 13 recnd ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\in ℂ$
15 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
16 15 recnd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℂ$
17 14 16 mulcld ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\mathrm{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 ℕ$
20 19 adantl ${⊢}\left({x}\in {ℝ}^{+}\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {d}\in ℕ$
21 vmacl ${⊢}{d}\in ℕ\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 ℕ\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)\mathrm{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)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left(\frac{{R}\left({x}\right)\mathrm{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)\mathrm{log}{x}\in ℂ$
44 43 31 addcld ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{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)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}-\mathrm{log}{x}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\left(\mathrm{log}{x}+\mathrm{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)\mathrm{log}{x}=\left(\psi \left({x}\right)-{x}\right)\mathrm{log}{x}$
49 42 33 16 subdird ${⊢}{x}\in {ℝ}^{+}\to \left(\psi \left({x}\right)-{x}\right)\mathrm{log}{x}=\psi \left({x}\right)\mathrm{log}{x}-{x}\mathrm{log}{x}$
50 48 49 eqtrd ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\mathrm{log}{x}=\psi \left({x}\right)\mathrm{log}{x}-{x}\mathrm{log}{x}$
51 50 oveq1d ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)=\psi \left({x}\right)\mathrm{log}{x}-{x}\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)$
52 33 16 mulcld ${⊢}{x}\in {ℝ}^{+}\to {x}\mathrm{log}{x}\in ℂ$
53 43 31 52 addsubd ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)-{x}\mathrm{log}{x}=\psi \left({x}\right)\mathrm{log}{x}-{x}\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)=\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)-{x}\mathrm{log}{x}$
55 54 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}=\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)-{x}\mathrm{log}{x}}{{x}}$
56 rpcnne0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
57 divsubdir ${⊢}\left(\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)\in ℂ\wedge {x}\mathrm{log}{x}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)-{x}\mathrm{log}{x}}{{x}}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\left(\frac{{x}\mathrm{log}{x}}{{x}}\right)$
58 44 52 56 57 syl3anc ${⊢}{x}\in {ℝ}^{+}\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)-{x}\mathrm{log}{x}}{{x}}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\left(\frac{{x}\mathrm{log}{x}}{{x}}\right)$
59 16 33 34 divcan3d ${⊢}{x}\in {ℝ}^{+}\to \frac{{x}\mathrm{log}{x}}{{x}}=\mathrm{log}{x}$
60 59 oveq2d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\left(\frac{{x}\mathrm{log}{x}}{{x}}\right)=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}$
61 55 58 60 3eqtrd ${⊢}{x}\in {ℝ}^{+}\to \frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}$
62 61 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}-\mathrm{log}{x}$
63 16 2timesd ${⊢}{x}\in {ℝ}^{+}\to 2\mathrm{log}{x}=\mathrm{log}{x}+\mathrm{log}{x}$
64 63 oveq2d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\left(\mathrm{log}{x}+\mathrm{log}{x}\right)$
65 46 62 64 3eqtr4d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}$
66 65 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\frac{{R}\left({x}\right)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}-\left(\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\right)=\left({x}\in {ℝ}^{+}⟼\frac{{R}\left({x}\right)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\frac{{R}\left({x}\right)\mathrm{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)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
103 vmadivsum ${⊢}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
104 o1sub ${⊢}\left(\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)\wedge \left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)\right)\to \left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
105 102 103 104 mp2an ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right)\psi \left(\frac{{x}}{{d}}\right)}{{x}}\right)-2\mathrm{log}{x}\right){-}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({d}\right)}{{d}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
106 101 105 eqeltrri ${⊢}\left({x}\in {ℝ}^{+}⟼\frac{{R}\left({x}\right)\mathrm{log}{x}+\sum _{{d}=1}^{⌊{x}⌋}\Lambda \left({d}\right){R}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\in 𝑂\left(1\right)$