# Metamath Proof Explorer

## Theorem selberg2lem

Description: Lemma for selberg2 . Equation 10.4.12 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
2 chpcl ${⊢}{x}\in ℝ\to \psi \left({x}\right)\in ℝ$
3 1 2 syl ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\in ℝ$
4 3 recnd ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\in ℂ$
5 rprege0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0\le {x}\right)$
6 flge0nn0 ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to ⌊{x}⌋\in {ℕ}_{0}$
7 5 6 syl ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋\in {ℕ}_{0}$
8 nn0p1nn ${⊢}⌊{x}⌋\in {ℕ}_{0}\to ⌊{x}⌋+1\in ℕ$
9 7 8 syl ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋+1\in ℕ$
10 9 nnrpd ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋+1\in {ℝ}^{+}$
11 10 relogcld ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\in ℝ$
12 11 recnd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\in ℂ$
13 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
14 13 recnd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℂ$
15 12 14 subcld ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\in ℂ$
16 4 15 mulcld ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in ℂ$
17 fzfid ${⊢}{x}\in {ℝ}^{+}\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
18 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
19 18 adantl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℕ$
20 19 nnrpd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in {ℝ}^{+}$
21 1rp ${⊢}1\in {ℝ}^{+}$
22 rpaddcl ${⊢}\left({n}\in {ℝ}^{+}\wedge 1\in {ℝ}^{+}\right)\to {n}+1\in {ℝ}^{+}$
23 21 22 mpan2 ${⊢}{n}\in {ℝ}^{+}\to {n}+1\in {ℝ}^{+}$
24 23 relogcld ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}\left({n}+1\right)\in ℝ$
25 relogcl ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}{n}\in ℝ$
26 24 25 resubcld ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\in ℝ$
27 rpre ${⊢}{n}\in {ℝ}^{+}\to {n}\in ℝ$
28 chpcl ${⊢}{n}\in ℝ\to \psi \left({n}\right)\in ℝ$
29 27 28 syl ${⊢}{n}\in {ℝ}^{+}\to \psi \left({n}\right)\in ℝ$
30 26 29 remulcld ${⊢}{n}\in {ℝ}^{+}\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℝ$
31 30 recnd ${⊢}{n}\in {ℝ}^{+}\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ$
32 20 31 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ$
33 17 32 fsumcl ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ$
34 rpcnne0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
35 divsubdir ${⊢}\left(\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in ℂ\wedge \sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}=\left(\frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)$
36 16 33 34 35 syl3anc ${⊢}{x}\in {ℝ}^{+}\to \frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}=\left(\frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)$
37 4 12 mulcld ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)\in ℂ$
38 4 14 mulcld ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{log}{x}\in ℂ$
39 37 38 33 sub32d ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\psi \left({x}\right)\mathrm{log}{x}-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)-\psi \left({x}\right)\mathrm{log}{x}$
40 4 12 14 subdid ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\psi \left({x}\right)\mathrm{log}{x}$
41 40 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\psi \left({x}\right)\mathrm{log}{x}-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
42 fveq2 ${⊢}{m}={n}\to \mathrm{log}{m}=\mathrm{log}{n}$
43 fvoveq1 ${⊢}{m}={n}\to \psi \left({m}-1\right)=\psi \left({n}-1\right)$
44 42 43 jca ${⊢}{m}={n}\to \left(\mathrm{log}{m}=\mathrm{log}{n}\wedge \psi \left({m}-1\right)=\psi \left({n}-1\right)\right)$
45 fveq2 ${⊢}{m}={n}+1\to \mathrm{log}{m}=\mathrm{log}\left({n}+1\right)$
46 fvoveq1 ${⊢}{m}={n}+1\to \psi \left({m}-1\right)=\psi \left({n}+1-1\right)$
47 45 46 jca ${⊢}{m}={n}+1\to \left(\mathrm{log}{m}=\mathrm{log}\left({n}+1\right)\wedge \psi \left({m}-1\right)=\psi \left({n}+1-1\right)\right)$
48 fveq2 ${⊢}{m}=1\to \mathrm{log}{m}=\mathrm{log}1$
49 log1 ${⊢}\mathrm{log}1=0$
50 48 49 syl6eq ${⊢}{m}=1\to \mathrm{log}{m}=0$
51 oveq1 ${⊢}{m}=1\to {m}-1=1-1$
52 1m1e0 ${⊢}1-1=0$
53 51 52 syl6eq ${⊢}{m}=1\to {m}-1=0$
54 53 fveq2d ${⊢}{m}=1\to \psi \left({m}-1\right)=\psi \left(0\right)$
55 2pos ${⊢}0<2$
56 0re ${⊢}0\in ℝ$
57 chpeq0 ${⊢}0\in ℝ\to \left(\psi \left(0\right)=0↔0<2\right)$
58 56 57 ax-mp ${⊢}\psi \left(0\right)=0↔0<2$
59 55 58 mpbir ${⊢}\psi \left(0\right)=0$
60 54 59 syl6eq ${⊢}{m}=1\to \psi \left({m}-1\right)=0$
61 50 60 jca ${⊢}{m}=1\to \left(\mathrm{log}{m}=0\wedge \psi \left({m}-1\right)=0\right)$
62 fveq2 ${⊢}{m}=⌊{x}⌋+1\to \mathrm{log}{m}=\mathrm{log}\left(⌊{x}⌋+1\right)$
63 fvoveq1 ${⊢}{m}=⌊{x}⌋+1\to \psi \left({m}-1\right)=\psi \left(⌊{x}⌋+1-1\right)$
64 62 63 jca ${⊢}{m}=⌊{x}⌋+1\to \left(\mathrm{log}{m}=\mathrm{log}\left(⌊{x}⌋+1\right)\wedge \psi \left({m}-1\right)=\psi \left(⌊{x}⌋+1-1\right)\right)$
65 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
66 9 65 eleqtrdi ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋+1\in {ℤ}_{\ge 1}$
67 elfznn ${⊢}{m}\in \left(1\dots ⌊{x}⌋+1\right)\to {m}\in ℕ$
68 67 adantl ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to {m}\in ℕ$
69 68 nnrpd ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to {m}\in {ℝ}^{+}$
70 69 relogcld ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to \mathrm{log}{m}\in ℝ$
71 70 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to \mathrm{log}{m}\in ℂ$
72 68 nnred ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to {m}\in ℝ$
73 peano2rem ${⊢}{m}\in ℝ\to {m}-1\in ℝ$
74 72 73 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to {m}-1\in ℝ$
75 chpcl ${⊢}{m}-1\in ℝ\to \psi \left({m}-1\right)\in ℝ$
76 74 75 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to \psi \left({m}-1\right)\in ℝ$
77 76 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {m}\in \left(1\dots ⌊{x}⌋+1\right)\right)\to \psi \left({m}-1\right)\in ℂ$
78 44 47 61 64 66 71 77 fsumparts ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}\in \left(1..^⌊{x}⌋+1\right)}\mathrm{log}{n}\left(\psi \left({n}+1-1\right)-\psi \left({n}-1\right)\right)=\mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)-0\cdot 0-\sum _{{n}\in \left(1..^⌊{x}⌋+1\right)}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}+1-1\right)$
79 7 nn0zd ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋\in ℤ$
80 fzval3 ${⊢}⌊{x}⌋\in ℤ\to \left(1\dots ⌊{x}⌋\right)=\left(1..^⌊{x}⌋+1\right)$
81 79 80 syl ${⊢}{x}\in {ℝ}^{+}\to \left(1\dots ⌊{x}⌋\right)=\left(1..^⌊{x}⌋+1\right)$
82 81 eqcomd ${⊢}{x}\in {ℝ}^{+}\to \left(1..^⌊{x}⌋+1\right)=\left(1\dots ⌊{x}⌋\right)$
83 nnm1nn0 ${⊢}{n}\in ℕ\to {n}-1\in {ℕ}_{0}$
84 19 83 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}-1\in {ℕ}_{0}$
85 84 nn0red ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}-1\in ℝ$
86 chpcl ${⊢}{n}-1\in ℝ\to \psi \left({n}-1\right)\in ℝ$
87 85 86 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}-1\right)\in ℝ$
88 87 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}-1\right)\in ℂ$
89 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
90 19 89 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
91 90 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\in ℂ$
92 19 nncnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℂ$
93 ax-1cn ${⊢}1\in ℂ$
94 pncan ${⊢}\left({n}\in ℂ\wedge 1\in ℂ\right)\to {n}+1-1={n}$
95 92 93 94 sylancl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}+1-1={n}$
96 npcan ${⊢}\left({n}\in ℂ\wedge 1\in ℂ\right)\to {n}-1+1={n}$
97 92 93 96 sylancl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}-1+1={n}$
98 95 97 eqtr4d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}+1-1={n}-1+1$
99 98 fveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}+1-1\right)=\psi \left({n}-1+1\right)$
100 chpp1 ${⊢}{n}-1\in {ℕ}_{0}\to \psi \left({n}-1+1\right)=\psi \left({n}-1\right)+\Lambda \left({n}-1+1\right)$
101 84 100 syl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}-1+1\right)=\psi \left({n}-1\right)+\Lambda \left({n}-1+1\right)$
102 97 fveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}-1+1\right)=\Lambda \left({n}\right)$
103 102 oveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}-1\right)+\Lambda \left({n}-1+1\right)=\psi \left({n}-1\right)+\Lambda \left({n}\right)$
104 99 101 103 3eqtrd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}+1-1\right)=\psi \left({n}-1\right)+\Lambda \left({n}\right)$
105 88 91 104 mvrladdd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}+1-1\right)-\psi \left({n}-1\right)=\Lambda \left({n}\right)$
106 105 oveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\left(\psi \left({n}+1-1\right)-\psi \left({n}-1\right)\right)=\mathrm{log}{n}\Lambda \left({n}\right)$
107 20 relogcld ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\in ℝ$
108 107 recnd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\in ℂ$
109 91 108 mulcomd ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\mathrm{log}{n}=\mathrm{log}{n}\Lambda \left({n}\right)$
110 106 109 eqtr4d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\left(\psi \left({n}+1-1\right)-\psi \left({n}-1\right)\right)=\Lambda \left({n}\right)\mathrm{log}{n}$
111 82 110 sumeq12rdv ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}\in \left(1..^⌊{x}⌋+1\right)}\mathrm{log}{n}\left(\psi \left({n}+1-1\right)-\psi \left({n}-1\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}$
112 7 nn0cnd ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋\in ℂ$
113 pncan ${⊢}\left(⌊{x}⌋\in ℂ\wedge 1\in ℂ\right)\to ⌊{x}⌋+1-1=⌊{x}⌋$
114 112 93 113 sylancl ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋+1-1=⌊{x}⌋$
115 114 fveq2d ${⊢}{x}\in {ℝ}^{+}\to \psi \left(⌊{x}⌋+1-1\right)=\psi \left(⌊{x}⌋\right)$
116 chpfl ${⊢}{x}\in ℝ\to \psi \left(⌊{x}⌋\right)=\psi \left({x}\right)$
117 1 116 syl ${⊢}{x}\in {ℝ}^{+}\to \psi \left(⌊{x}⌋\right)=\psi \left({x}\right)$
118 115 117 eqtrd ${⊢}{x}\in {ℝ}^{+}\to \psi \left(⌊{x}⌋+1-1\right)=\psi \left({x}\right)$
119 118 oveq2d ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)=\mathrm{log}\left(⌊{x}⌋+1\right)\psi \left({x}\right)$
120 12 4 mulcomd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left({x}\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)$
121 119 120 eqtrd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)$
122 0cn ${⊢}0\in ℂ$
123 122 mul01i ${⊢}0\cdot 0=0$
124 123 a1i ${⊢}{x}\in {ℝ}^{+}\to 0\cdot 0=0$
125 121 124 oveq12d ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)-0\cdot 0=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-0$
126 37 subid1d ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-0=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)$
127 125 126 eqtrd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)-0\cdot 0=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)$
128 95 fveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left({n}+1-1\right)=\psi \left({n}\right)$
129 128 oveq2d ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}+1-1\right)=\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
130 82 129 sumeq12rdv ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}\in \left(1..^⌊{x}⌋+1\right)}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}+1-1\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
131 127 130 oveq12d ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\psi \left(⌊{x}⌋+1-1\right)-0\cdot 0-\sum _{{n}\in \left(1..^⌊{x}⌋+1\right)}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}+1-1\right)=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
132 78 111 131 3eqtr3d ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
133 132 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}=\psi \left({x}\right)\mathrm{log}\left(⌊{x}⌋+1\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)-\psi \left({x}\right)\mathrm{log}{x}$
134 39 41 133 3eqtr4d ${⊢}{x}\in {ℝ}^{+}\to \psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)=\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}$
135 134 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}=\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}$
136 div23 ${⊢}\left(\psi \left({x}\right)\in ℂ\wedge \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)}{{x}}=\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)$
137 4 15 34 136 syl3anc ${⊢}{x}\in {ℝ}^{+}\to \frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)}{{x}}=\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)$
138 137 oveq1d ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\psi \left({x}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)}{{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)=\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)$
139 36 135 138 3eqtr3rd ${⊢}{x}\in {ℝ}^{+}\to \left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)=\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\mathrm{log}{n}-\psi \left({x}\right)\mathrm{log}{x}}{{x}}$
140 139 mpteq2ia ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)\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)$
141 ovexd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in \mathrm{V}$
142 ovexd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\in \mathrm{V}$
143 reex ${⊢}ℝ\in \mathrm{V}$
144 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
145 143 144 ssexi ${⊢}{ℝ}^{+}\in \mathrm{V}$
146 145 a1i ${⊢}\top \to {ℝ}^{+}\in \mathrm{V}$
147 ovexd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\psi \left({x}\right)}{{x}}\in \mathrm{V}$
148 15 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\in ℂ$
149 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right)=\left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right)$
150 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)$
151 146 147 148 149 150 offval2 ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right){×}_{f}\left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\right)$
152 chpo1ub ${⊢}\left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right)\in 𝑂\left(1\right)$
153 0red ${⊢}\top \to 0\in ℝ$
154 1red ${⊢}\top \to 1\in ℝ$
155 divrcnv
156 93 155 mp1i
157 rpreccl ${⊢}{x}\in {ℝ}^{+}\to \frac{1}{{x}}\in {ℝ}^{+}$
158 157 rpred ${⊢}{x}\in {ℝ}^{+}\to \frac{1}{{x}}\in ℝ$
159 158 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{1}{{x}}\in ℝ$
160 11 13 resubcld ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\in ℝ$
161 160 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\in ℝ$
162 rpaddcl ${⊢}\left({x}\in {ℝ}^{+}\wedge 1\in {ℝ}^{+}\right)\to {x}+1\in {ℝ}^{+}$
163 21 162 mpan2 ${⊢}{x}\in {ℝ}^{+}\to {x}+1\in {ℝ}^{+}$
164 163 relogcld ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left({x}+1\right)\in ℝ$
165 164 13 resubcld ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left({x}+1\right)-\mathrm{log}{x}\in ℝ$
166 7 nn0red ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋\in ℝ$
167 1red ${⊢}{x}\in {ℝ}^{+}\to 1\in ℝ$
168 flle ${⊢}{x}\in ℝ\to ⌊{x}⌋\le {x}$
169 1 168 syl ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋\le {x}$
170 166 1 167 169 leadd1dd ${⊢}{x}\in {ℝ}^{+}\to ⌊{x}⌋+1\le {x}+1$
171 10 163 logled ${⊢}{x}\in {ℝ}^{+}\to \left(⌊{x}⌋+1\le {x}+1↔\mathrm{log}\left(⌊{x}⌋+1\right)\le \mathrm{log}\left({x}+1\right)\right)$
172 170 171 mpbid ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)\le \mathrm{log}\left({x}+1\right)$
173 11 164 13 172 lesub1dd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\le \mathrm{log}\left({x}+1\right)-\mathrm{log}{x}$
174 logdifbnd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left({x}+1\right)-\mathrm{log}{x}\le \frac{1}{{x}}$
175 160 165 158 173 174 letrd ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\le \frac{1}{{x}}$
176 175 ad2antrl ${⊢}\left(\top \wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\le \frac{1}{{x}}$
177 fllep1 ${⊢}{x}\in ℝ\to {x}\le ⌊{x}⌋+1$
178 1 177 syl ${⊢}{x}\in {ℝ}^{+}\to {x}\le ⌊{x}⌋+1$
179 logleb ${⊢}\left({x}\in {ℝ}^{+}\wedge ⌊{x}⌋+1\in {ℝ}^{+}\right)\to \left({x}\le ⌊{x}⌋+1↔\mathrm{log}{x}\le \mathrm{log}\left(⌊{x}⌋+1\right)\right)$
180 10 179 mpdan ${⊢}{x}\in {ℝ}^{+}\to \left({x}\le ⌊{x}⌋+1↔\mathrm{log}{x}\le \mathrm{log}\left(⌊{x}⌋+1\right)\right)$
181 178 180 mpbid ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\le \mathrm{log}\left(⌊{x}⌋+1\right)$
182 11 13 subge0d ${⊢}{x}\in {ℝ}^{+}\to \left(0\le \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}↔\mathrm{log}{x}\le \mathrm{log}\left(⌊{x}⌋+1\right)\right)$
183 181 182 mpbird ${⊢}{x}\in {ℝ}^{+}\to 0\le \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}$
184 183 ad2antrl ${⊢}\left(\top \wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 0\le \mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}$
185 153 154 156 159 161 176 184 rlimsqz2
186 rlimo1
187 185 186 syl ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
188 o1mul ${⊢}\left(\left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right)\in 𝑂\left(1\right)\wedge \left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)\right)\to \left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right){×}_{f}\left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
189 152 187 188 sylancr ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\frac{\psi \left({x}\right)}{{x}}\right){×}_{f}\left({x}\in {ℝ}^{+}⟼\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
190 151 189 eqeltrrd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)\right)\in 𝑂\left(1\right)$
191 nnrp ${⊢}{m}\in ℕ\to {m}\in {ℝ}^{+}$
192 191 ssriv ${⊢}ℕ\subseteq {ℝ}^{+}$
193 192 a1i ${⊢}\top \to ℕ\subseteq {ℝ}^{+}$
194 193 sselda ${⊢}\left(\top \wedge {n}\in ℕ\right)\to {n}\in {ℝ}^{+}$
195 194 31 syl ${⊢}\left(\top \wedge {n}\in ℕ\right)\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ$
196 chpo1ub ${⊢}\left({n}\in {ℝ}^{+}⟼\frac{\psi \left({n}\right)}{{n}}\right)\in 𝑂\left(1\right)$
197 196 a1i ${⊢}\top \to \left({n}\in {ℝ}^{+}⟼\frac{\psi \left({n}\right)}{{n}}\right)\in 𝑂\left(1\right)$
198 rerpdivcl ${⊢}\left(\psi \left({n}\right)\in ℝ\wedge {n}\in {ℝ}^{+}\right)\to \frac{\psi \left({n}\right)}{{n}}\in ℝ$
199 29 198 mpancom ${⊢}{n}\in {ℝ}^{+}\to \frac{\psi \left({n}\right)}{{n}}\in ℝ$
200 199 adantl ${⊢}\left(\top \wedge {n}\in {ℝ}^{+}\right)\to \frac{\psi \left({n}\right)}{{n}}\in ℝ$
201 31 adantl ${⊢}\left(\top \wedge {n}\in {ℝ}^{+}\right)\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\in ℂ$
202 rpreccl ${⊢}{n}\in {ℝ}^{+}\to \frac{1}{{n}}\in {ℝ}^{+}$
203 202 rpred ${⊢}{n}\in {ℝ}^{+}\to \frac{1}{{n}}\in ℝ$
204 chpge0 ${⊢}{n}\in ℝ\to 0\le \psi \left({n}\right)$
205 27 204 syl ${⊢}{n}\in {ℝ}^{+}\to 0\le \psi \left({n}\right)$
206 logdifbnd ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\le \frac{1}{{n}}$
207 26 203 29 205 206 lemul1ad ${⊢}{n}\in {ℝ}^{+}\to \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\le \left(\frac{1}{{n}}\right)\psi \left({n}\right)$
208 27 lep1d ${⊢}{n}\in {ℝ}^{+}\to {n}\le {n}+1$
209 logleb ${⊢}\left({n}\in {ℝ}^{+}\wedge {n}+1\in {ℝ}^{+}\right)\to \left({n}\le {n}+1↔\mathrm{log}{n}\le \mathrm{log}\left({n}+1\right)\right)$
210 23 209 mpdan ${⊢}{n}\in {ℝ}^{+}\to \left({n}\le {n}+1↔\mathrm{log}{n}\le \mathrm{log}\left({n}+1\right)\right)$
211 208 210 mpbid ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}{n}\le \mathrm{log}\left({n}+1\right)$
212 24 25 subge0d ${⊢}{n}\in {ℝ}^{+}\to \left(0\le \mathrm{log}\left({n}+1\right)-\mathrm{log}{n}↔\mathrm{log}{n}\le \mathrm{log}\left({n}+1\right)\right)$
213 211 212 mpbird ${⊢}{n}\in {ℝ}^{+}\to 0\le \mathrm{log}\left({n}+1\right)-\mathrm{log}{n}$
214 26 29 213 205 mulge0d ${⊢}{n}\in {ℝ}^{+}\to 0\le \left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
215 30 214 absidd ${⊢}{n}\in {ℝ}^{+}\to \left|\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\right|=\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)$
216 rpregt0 ${⊢}{n}\in {ℝ}^{+}\to \left({n}\in ℝ\wedge 0<{n}\right)$
217 divge0 ${⊢}\left(\left(\psi \left({n}\right)\in ℝ\wedge 0\le \psi \left({n}\right)\right)\wedge \left({n}\in ℝ\wedge 0<{n}\right)\right)\to 0\le \frac{\psi \left({n}\right)}{{n}}$
218 29 205 216 217 syl21anc ${⊢}{n}\in {ℝ}^{+}\to 0\le \frac{\psi \left({n}\right)}{{n}}$
219 199 218 absidd ${⊢}{n}\in {ℝ}^{+}\to \left|\frac{\psi \left({n}\right)}{{n}}\right|=\frac{\psi \left({n}\right)}{{n}}$
220 29 recnd ${⊢}{n}\in {ℝ}^{+}\to \psi \left({n}\right)\in ℂ$
221 rpcn ${⊢}{n}\in {ℝ}^{+}\to {n}\in ℂ$
222 rpne0 ${⊢}{n}\in {ℝ}^{+}\to {n}\ne 0$
223 220 221 222 divrec2d ${⊢}{n}\in {ℝ}^{+}\to \frac{\psi \left({n}\right)}{{n}}=\left(\frac{1}{{n}}\right)\psi \left({n}\right)$
224 219 223 eqtrd ${⊢}{n}\in {ℝ}^{+}\to \left|\frac{\psi \left({n}\right)}{{n}}\right|=\left(\frac{1}{{n}}\right)\psi \left({n}\right)$
225 207 215 224 3brtr4d ${⊢}{n}\in {ℝ}^{+}\to \left|\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\right|\le \left|\frac{\psi \left({n}\right)}{{n}}\right|$
226 225 ad2antrl ${⊢}\left(\top \wedge \left({n}\in {ℝ}^{+}\wedge 1\le {n}\right)\right)\to \left|\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\right|\le \left|\frac{\psi \left({n}\right)}{{n}}\right|$
227 154 197 200 201 226 o1le ${⊢}\top \to \left({n}\in {ℝ}^{+}⟼\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\right)\in 𝑂\left(1\right)$
228 193 227 o1res2 ${⊢}\top \to \left({n}\in ℕ⟼\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)\right)\in 𝑂\left(1\right)$
229 195 228 o1fsum ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)\in 𝑂\left(1\right)$
230 141 142 190 229 o1sub2 ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\psi \left({x}\right)}{{x}}\right)\left(\mathrm{log}\left(⌊{x}⌋+1\right)-\mathrm{log}{x}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\mathrm{log}\left({n}+1\right)-\mathrm{log}{n}\right)\psi \left({n}\right)}{{x}}\right)\right)\in 𝑂\left(1\right)$
231 140 230 eqeltrrid ${⊢}\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)\in 𝑂\left(1\right)$
232 231 mptru ${⊢}\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)$