# Metamath Proof Explorer

## Theorem selberg2b

Description: Convert eventual boundedness in selberg2 to boundedness on any interval [ A , +oo ) . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Assertion selberg2b ${⊢}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left|\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|\le {c}$

### Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 elicopnf ${⊢}1\in ℝ\to \left({x}\in \left[1,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 1\le {x}\right)\right)$
3 1 2 mp1i ${⊢}\top \to \left({x}\in \left[1,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 1\le {x}\right)\right)$
4 3 simprbda ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
5 4 ex ${⊢}\top \to \left({x}\in \left[1,\mathrm{+\infty }\right)\to {x}\in ℝ\right)$
6 5 ssrdv ${⊢}\top \to \left[1,\mathrm{+\infty }\right)\subseteq ℝ$
7 1 a1i ${⊢}\top \to 1\in ℝ$
8 chpcl ${⊢}{x}\in ℝ\to \psi \left({x}\right)\in ℝ$
9 4 8 syl ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \psi \left({x}\right)\in ℝ$
10 1rp ${⊢}1\in {ℝ}^{+}$
11 10 a1i ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to 1\in {ℝ}^{+}$
12 3 simplbda ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to 1\le {x}$
13 4 11 12 rpgecld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to {x}\in {ℝ}^{+}$
14 13 relogcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℝ$
15 9 14 remulcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}\in ℝ$
16 fzfid ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
17 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
18 17 adantl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℕ$
19 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
20 18 19 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
21 4 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℝ$
22 21 18 nndivred ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{n}}\in ℝ$
23 chpcl ${⊢}\frac{{x}}{{n}}\in ℝ\to \psi \left(\frac{{x}}{{n}}\right)\in ℝ$
24 22 23 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \psi \left(\frac{{x}}{{n}}\right)\in ℝ$
25 20 24 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
26 16 25 fsumrecl ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
27 15 26 readdcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
28 27 13 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\in ℝ$
29 2re ${⊢}2\in ℝ$
30 29 a1i ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to 2\in ℝ$
31 30 14 remulcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to 2\mathrm{log}{x}\in ℝ$
32 28 31 resubcld ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \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}\in ℝ$
33 32 recnd ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to \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}\in ℂ$
34 13 ex ${⊢}\top \to \left({x}\in \left[1,\mathrm{+\infty }\right)\to {x}\in {ℝ}^{+}\right)$
35 34 ssrdv ${⊢}\top \to \left[1,\mathrm{+\infty }\right)\subseteq {ℝ}^{+}$
36 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)$
37 36 a1i ${⊢}\top \to \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)$
38 35 37 o1res2 ${⊢}\top \to \left({x}\in \left[1,\mathrm{+\infty }\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}\right)\in 𝑂\left(1\right)$
39 chpcl ${⊢}{y}\in ℝ\to \psi \left({y}\right)\in ℝ$
40 39 ad2antrl ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \psi \left({y}\right)\in ℝ$
41 simprl ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to {y}\in ℝ$
42 10 a1i ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to 1\in {ℝ}^{+}$
43 simprr ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to 1\le {y}$
44 41 42 43 rpgecld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to {y}\in {ℝ}^{+}$
45 44 relogcld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \mathrm{log}{y}\in ℝ$
46 40 45 remulcld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}\in ℝ$
47 fzfid ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \left(1\dots ⌊{y}⌋\right)\in \mathrm{Fin}$
48 elfznn ${⊢}{n}\in \left(1\dots ⌊{y}⌋\right)\to {n}\in ℕ$
49 48 adantl ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {n}\in ℕ$
50 49 19 syl ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
51 41 adantr ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {y}\in ℝ$
52 51 49 nndivred ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \frac{{y}}{{n}}\in ℝ$
53 chpcl ${⊢}\frac{{y}}{{n}}\in ℝ\to \psi \left(\frac{{y}}{{n}}\right)\in ℝ$
54 52 53 syl ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \psi \left(\frac{{y}}{{n}}\right)\in ℝ$
55 50 54 remulcld ${⊢}\left(\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
56 47 55 fsumrecl ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
57 46 56 readdcld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
58 29 a1i ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to 2\in ℝ$
59 58 45 remulcld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to 2\mathrm{log}{y}\in ℝ$
60 57 59 readdcld ${⊢}\left(\top \wedge \left({y}\in ℝ\wedge 1\le {y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)+2\mathrm{log}{y}\in ℝ$
61 32 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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}\in ℝ$
62 61 recnd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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}\in ℂ$
63 62 abscld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|\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 ℝ$
64 28 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\in ℝ$
65 64 recnd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\in ℂ$
66 65 abscld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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|\in ℝ$
67 31 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{log}{x}\in ℝ$
68 67 recnd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{log}{x}\in ℂ$
69 68 abscld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|2\mathrm{log}{x}\right|\in ℝ$
70 66 69 readdcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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|+\left|2\mathrm{log}{x}\right|\in ℝ$
71 60 ad2ant2r ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)+2\mathrm{log}{y}\in ℝ$
72 65 68 abs2dif2d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|\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|\le \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|+\left|2\mathrm{log}{x}\right|$
73 simprll ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {y}\in ℝ$
74 73 39 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({y}\right)\in ℝ$
75 13 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {x}\in {ℝ}^{+}$
76 4 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {x}\in ℝ$
77 simprr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {x}<{y}$
78 76 73 77 ltled ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {x}\le {y}$
79 73 75 78 rpgecld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to {y}\in {ℝ}^{+}$
80 79 relogcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \mathrm{log}{y}\in ℝ$
81 74 80 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}\in ℝ$
82 56 ad2ant2r ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
83 81 82 readdcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
84 29 a1i ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 2\in ℝ$
85 84 80 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{log}{y}\in ℝ$
86 76 8 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\in ℝ$
87 75 relogcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \mathrm{log}{x}\in ℝ$
88 86 87 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}\in ℝ$
89 26 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
90 88 89 readdcld ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
91 chpge0 ${⊢}{x}\in ℝ\to 0\le \psi \left({x}\right)$
92 76 91 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \psi \left({x}\right)$
93 12 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 1\le {x}$
94 76 93 logge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \mathrm{log}{x}$
95 86 87 92 94 mulge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \psi \left({x}\right)\mathrm{log}{x}$
96 vmage0 ${⊢}{n}\in ℕ\to 0\le \Lambda \left({n}\right)$
97 18 96 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \Lambda \left({n}\right)$
98 chpge0 ${⊢}\frac{{x}}{{n}}\in ℝ\to 0\le \psi \left(\frac{{x}}{{n}}\right)$
99 22 98 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \psi \left(\frac{{x}}{{n}}\right)$
100 20 24 97 99 mulge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
101 16 25 100 fsumge0 ${⊢}\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\to 0\le \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
102 101 adantr ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
103 88 89 95 102 addge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
104 90 75 103 divge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}$
105 64 104 absidd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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|=\frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}$
106 10 a1i ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 1\in {ℝ}^{+}$
107 chpwordi ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}\le {y}\right)\to \psi \left({x}\right)\le \psi \left({y}\right)$
108 76 73 78 107 syl3anc ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\le \psi \left({y}\right)$
109 75 79 logled ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left({x}\le {y}↔\mathrm{log}{x}\le \mathrm{log}{y}\right)$
110 78 109 mpbid ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \mathrm{log}{x}\le \mathrm{log}{y}$
111 86 74 87 80 92 94 108 110 lemul12ad ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}\le \psi \left({y}\right)\mathrm{log}{y}$
112 fzfid ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left(1\dots ⌊{y}⌋\right)\in \mathrm{Fin}$
113 48 adantl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {n}\in ℕ$
114 113 19 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
115 76 adantr ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {x}\in ℝ$
116 115 113 nndivred ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \frac{{x}}{{n}}\in ℝ$
117 116 23 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \psi \left(\frac{{x}}{{n}}\right)\in ℝ$
118 114 117 remulcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
119 112 118 fsumrecl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\in ℝ$
120 113 96 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to 0\le \Lambda \left({n}\right)$
121 116 98 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to 0\le \psi \left(\frac{{x}}{{n}}\right)$
122 114 117 120 121 mulge0d ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to 0\le \Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
123 flword2 ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}\le {y}\right)\to ⌊{y}⌋\in {ℤ}_{\ge ⌊{x}⌋}$
124 76 73 78 123 syl3anc ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to ⌊{y}⌋\in {ℤ}_{\ge ⌊{x}⌋}$
125 fzss2 ${⊢}⌊{y}⌋\in {ℤ}_{\ge ⌊{x}⌋}\to \left(1\dots ⌊{x}⌋\right)\subseteq \left(1\dots ⌊{y}⌋\right)$
126 124 125 syl ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left(1\dots ⌊{x}⌋\right)\subseteq \left(1\dots ⌊{y}⌋\right)$
127 112 118 122 126 fsumless ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\le \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)$
128 73 adantr ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {y}\in ℝ$
129 128 113 nndivred ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \frac{{y}}{{n}}\in ℝ$
130 129 53 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \psi \left(\frac{{y}}{{n}}\right)\in ℝ$
131 114 130 remulcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℝ$
132 113 nnrpd ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {n}\in {ℝ}^{+}$
133 78 adantr ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to {x}\le {y}$
134 115 128 132 133 lediv1dd ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \frac{{x}}{{n}}\le \frac{{y}}{{n}}$
135 chpwordi ${⊢}\left(\frac{{x}}{{n}}\in ℝ\wedge \frac{{y}}{{n}}\in ℝ\wedge \frac{{x}}{{n}}\le \frac{{y}}{{n}}\right)\to \psi \left(\frac{{x}}{{n}}\right)\le \psi \left(\frac{{y}}{{n}}\right)$
136 116 129 134 135 syl3anc ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \psi \left(\frac{{x}}{{n}}\right)\le \psi \left(\frac{{y}}{{n}}\right)$
137 117 130 114 120 136 lemul2ad ${⊢}\left(\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\wedge {n}\in \left(1\dots ⌊{y}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\le \Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
138 112 118 131 137 fsumle ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\le \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
139 89 119 82 127 138 letrd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\le \sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
140 88 89 81 82 111 139 le2addd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)\le \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
141 90 83 106 76 103 140 93 lediv12ad ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\le \frac{\psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)}{1}$
142 83 recnd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)\in ℂ$
143 142 div1d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \frac{\psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)}{1}=\psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
144 141 143 breqtrd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \frac{\psi \left({x}\right)\mathrm{log}{x}+\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\psi \left(\frac{{x}}{{n}}\right)}{{x}}\le \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
145 105 144 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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|\le \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)$
146 2rp ${⊢}2\in {ℝ}^{+}$
147 rpge0 ${⊢}2\in {ℝ}^{+}\to 0\le 2$
148 146 147 mp1i ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le 2$
149 84 87 148 94 mulge0d ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 0\le 2\mathrm{log}{x}$
150 67 149 absidd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|2\mathrm{log}{x}\right|=2\mathrm{log}{x}$
151 87 80 84 148 110 lemul2ad ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{log}{x}\le 2\mathrm{log}{y}$
152 150 151 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|2\mathrm{log}{x}\right|\le 2\mathrm{log}{y}$
153 66 69 83 85 145 152 le2addd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \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|+\left|2\mathrm{log}{x}\right|\le \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)+2\mathrm{log}{y}$
154 63 70 71 72 153 letrd ${⊢}\left(\left(\top \wedge {x}\in \left[1,\mathrm{+\infty }\right)\right)\wedge \left(\left({y}\in ℝ\wedge 1\le {y}\right)\wedge {x}<{y}\right)\right)\to \left|\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|\le \psi \left({y}\right)\mathrm{log}{y}+\sum _{{n}=1}^{⌊{y}⌋}\Lambda \left({n}\right)\psi \left(\frac{{y}}{{n}}\right)+2\mathrm{log}{y}$
155 6 7 33 38 60 154 o1bddrp ${⊢}\top \to \exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left|\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|\le {c}$
156 155 mptru ${⊢}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left|\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|\le {c}$