# Metamath Proof Explorer

## Theorem pntrlog2bndlem1

Description: The sum of selberg3r and selberg4r . (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses pntsval.1 ${⊢}{S}=\left({a}\in ℝ⟼\sum _{{i}=1}^{⌊{a}⌋}\Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)\right)$
pntrlog2bnd.r ${⊢}{R}=\left({a}\in {ℝ}^{+}⟼\psi \left({a}\right)-{a}\right)$
Assertion pntrlog2bndlem1 ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\right)\in \le 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 pntsval.1 ${⊢}{S}=\left({a}\in ℝ⟼\sum _{{i}=1}^{⌊{a}⌋}\Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)\right)$
2 pntrlog2bnd.r ${⊢}{R}=\left({a}\in {ℝ}^{+}⟼\psi \left({a}\right)-{a}\right)$
3 1red ${⊢}\top \to 1\in ℝ$
4 2 selberg34r ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right)\in 𝑂\left(1\right)$
5 elioore ${⊢}{x}\in \left(1,\mathrm{+\infty }\right)\to {x}\in ℝ$
6 5 adantl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
7 1rp ${⊢}1\in {ℝ}^{+}$
8 7 a1i ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\in {ℝ}^{+}$
9 1red ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\in ℝ$
10 eliooord ${⊢}{x}\in \left(1,\mathrm{+\infty }\right)\to \left(1<{x}\wedge {x}<\mathrm{+\infty }\right)$
11 10 adantl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(1<{x}\wedge {x}<\mathrm{+\infty }\right)$
12 11 simpld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1<{x}$
13 9 6 12 ltled ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\le {x}$
14 6 8 13 rpgecld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\in {ℝ}^{+}$
15 2 pntrf ${⊢}{R}:{ℝ}^{+}⟶ℝ$
16 15 ffvelrni ${⊢}{x}\in {ℝ}^{+}\to {R}\left({x}\right)\in ℝ$
17 14 16 syl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\in ℝ$
18 14 relogcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℝ$
19 17 18 remulcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\mathrm{log}{x}\in ℝ$
20 fzfid ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
21 14 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 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
23 22 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 ℕ$
24 23 nnrpd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in {ℝ}^{+}$
25 21 24 rpdivcld ${⊢}\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 {ℝ}^{+}$
26 15 ffvelrni ${⊢}\frac{{x}}{{n}}\in {ℝ}^{+}\to {R}\left(\frac{{x}}{{n}}\right)\in ℝ$
27 25 26 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {R}\left(\frac{{x}}{{n}}\right)\in ℝ$
28 fzfid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots {n}\right)\in \mathrm{Fin}$
29 dvdsssfz1 ${⊢}{n}\in ℕ\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq \left(1\dots {n}\right)$
30 23 29 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq \left(1\dots {n}\right)$
31 28 30 ssfid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\in \mathrm{Fin}$
32 ssrab2 ${⊢}\left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq ℕ$
33 simpr ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
34 32 33 sseldi ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to {m}\in ℕ$
35 vmacl ${⊢}{m}\in ℕ\to \Lambda \left({m}\right)\in ℝ$
36 34 35 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\in ℝ$
37 dvdsdivcl ${⊢}\left({n}\in ℕ\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
38 23 37 sylan ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
39 32 38 sseldi ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in ℕ$
40 vmacl ${⊢}\frac{{n}}{{m}}\in ℕ\to \Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
41 39 40 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
42 36 41 remulcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
43 31 42 fsumrecl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
44 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
45 23 44 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 ℝ$
46 24 relogcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{n}\in ℝ$
47 45 46 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)\mathrm{log}{n}\in ℝ$
48 43 47 resubcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\in ℝ$
49 27 48 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\in ℝ$
50 20 49 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\in ℝ$
51 6 12 rplogcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in {ℝ}^{+}$
52 50 51 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\in ℝ$
53 19 52 resubcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\in ℝ$
54 53 14 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\in ℝ$
55 54 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\in ℂ$
56 55 lo1o12 ${⊢}\top \to \left(\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right)\in 𝑂\left(1\right)↔\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|\right)\in \le 𝑂\left(1\right)\right)$
57 4 56 mpbii ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|\right)\in \le 𝑂\left(1\right)$
58 55 abscld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|\in ℝ$
59 17 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\in ℂ$
60 59 abscld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\in ℝ$
61 60 18 remulcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}\in ℝ$
62 27 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {R}\left(\frac{{x}}{{n}}\right)\in ℂ$
63 62 abscld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\right|\in ℝ$
64 23 nnred ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℝ$
65 1 pntsf ${⊢}{S}:ℝ⟶ℝ$
66 65 ffvelrni ${⊢}{n}\in ℝ\to {S}\left({n}\right)\in ℝ$
67 64 66 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)\in ℝ$
68 1red ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in ℝ$
69 64 68 resubcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}-1\in ℝ$
70 65 ffvelrni ${⊢}{n}-1\in ℝ\to {S}\left({n}-1\right)\in ℝ$
71 69 70 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)\in ℝ$
72 67 71 resubcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)-{S}\left({n}-1\right)\in ℝ$
73 63 72 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)\in ℝ$
74 20 73 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)\in ℝ$
75 74 51 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\in ℝ$
76 61 75 resubcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)\in ℝ$
77 76 14 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\in ℝ$
78 18 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℂ$
79 59 78 mulcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\mathrm{log}{x}\in ℂ$
80 50 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\in ℂ$
81 51 rpne0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\ne 0$
82 80 78 81 divcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\in ℂ$
83 79 82 subcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\in ℂ$
84 83 abscld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|\in ℝ$
85 80 abscld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\in ℝ$
86 85 51 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\in ℝ$
87 61 86 resubcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\right)\in ℝ$
88 49 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\in ℂ$
89 88 abscld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\in ℝ$
90 20 89 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\in ℝ$
91 20 88 fsumabs ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|$
92 48 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\in ℂ$
93 62 92 absmuld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|=\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right|$
94 92 abscld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right|\in ℝ$
95 62 absge0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \left|{R}\left(\frac{{x}}{{n}}\right)\right|$
96 43 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℂ$
97 47 recnd ${⊢}\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)\mathrm{log}{n}\in ℂ$
98 96 97 abs2dif2d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right|\le \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right|+\left|\Lambda \left({n}\right)\mathrm{log}{n}\right|$
99 71 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)\in ℂ$
100 96 97 addcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}\in ℂ$
101 99 100 pncan2d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)+\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}\right)-{S}\left({n}-1\right)=\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}$
102 elfzuz ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in {ℤ}_{\ge 1}$
103 102 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 {ℤ}_{\ge 1}$
104 elfznn ${⊢}{k}\in \left(1\dots {n}\right)\to {k}\in ℕ$
105 104 adantl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℕ$
106 vmacl ${⊢}{k}\in ℕ\to \Lambda \left({k}\right)\in ℝ$
107 105 106 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \Lambda \left({k}\right)\in ℝ$
108 105 nnrpd ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in {ℝ}^{+}$
109 108 relogcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \mathrm{log}{k}\in ℝ$
110 107 109 remulcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \Lambda \left({k}\right)\mathrm{log}{k}\in ℝ$
111 fzfid ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left(1\dots {k}\right)\in \mathrm{Fin}$
112 dvdsssfz1 ${⊢}{k}\in ℕ\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq \left(1\dots {k}\right)$
113 105 112 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq \left(1\dots {k}\right)$
114 111 113 ssfid ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\in \mathrm{Fin}$
115 ssrab2 ${⊢}\left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq ℕ$
116 simpr ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}$
117 115 116 sseldi ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to {m}\in ℕ$
118 117 35 syl ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \Lambda \left({m}\right)\in ℝ$
119 dvdsdivcl ${⊢}\left({k}\in ℕ\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \frac{{k}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}$
120 105 119 sylan ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \frac{{k}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}$
121 115 120 sseldi ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \frac{{k}}{{m}}\in ℕ$
122 vmacl ${⊢}\frac{{k}}{{m}}\in ℕ\to \Lambda \left(\frac{{k}}{{m}}\right)\in ℝ$
123 121 122 syl ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \Lambda \left(\frac{{k}}{{m}}\right)\in ℝ$
124 118 123 remulcld ${⊢}\left(\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\in ℝ$
125 114 124 fsumrecl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\in ℝ$
126 110 125 readdcld ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\in ℝ$
127 126 recnd ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\in ℂ$
128 fveq2 ${⊢}{k}={n}\to \Lambda \left({k}\right)=\Lambda \left({n}\right)$
129 fveq2 ${⊢}{k}={n}\to \mathrm{log}{k}=\mathrm{log}{n}$
130 128 129 oveq12d ${⊢}{k}={n}\to \Lambda \left({k}\right)\mathrm{log}{k}=\Lambda \left({n}\right)\mathrm{log}{n}$
131 breq2 ${⊢}{k}={n}\to \left({y}\parallel {k}↔{y}\parallel {n}\right)$
132 131 rabbidv ${⊢}{k}={n}\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}=\left\{{y}\in ℕ|{y}\parallel {n}\right\}$
133 fvoveq1 ${⊢}{k}={n}\to \Lambda \left(\frac{{k}}{{m}}\right)=\Lambda \left(\frac{{n}}{{m}}\right)$
134 133 oveq2d ${⊢}{k}={n}\to \Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)=\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
135 134 adantr ${⊢}\left({k}={n}\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)=\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
136 132 135 sumeq12rdv ${⊢}{k}={n}\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)=\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
137 130 136 oveq12d ${⊢}{k}={n}\to \Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)=\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
138 103 127 137 fsumm1 ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{k}=1}^{{n}}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)=\sum _{{k}=1}^{{n}-1}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)+\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
139 1 pntsval2 ${⊢}{n}\in ℝ\to {S}\left({n}\right)=\sum _{{k}=1}^{⌊{n}⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
140 64 139 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)=\sum _{{k}=1}^{⌊{n}⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
141 23 nnzd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℤ$
142 flid ${⊢}{n}\in ℤ\to ⌊{n}⌋={n}$
143 141 142 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to ⌊{n}⌋={n}$
144 143 oveq2d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots ⌊{n}⌋\right)=\left(1\dots {n}\right)$
145 144 sumeq1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{k}=1}^{⌊{n}⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)=\sum _{{k}=1}^{{n}}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
146 140 145 eqtrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)=\sum _{{k}=1}^{{n}}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
147 1 pntsval2 ${⊢}{n}-1\in ℝ\to {S}\left({n}-1\right)=\sum _{{k}=1}^{⌊{n}-1⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
148 69 147 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)=\sum _{{k}=1}^{⌊{n}-1⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
149 1zzd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in ℤ$
150 141 149 zsubcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}-1\in ℤ$
151 flid ${⊢}{n}-1\in ℤ\to ⌊{n}-1⌋={n}-1$
152 150 151 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to ⌊{n}-1⌋={n}-1$
153 152 oveq2d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots ⌊{n}-1⌋\right)=\left(1\dots {n}-1\right)$
154 153 sumeq1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{k}=1}^{⌊{n}-1⌋}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)=\sum _{{k}=1}^{{n}-1}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
155 148 154 eqtrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)=\sum _{{k}=1}^{{n}-1}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)$
156 96 97 addcomd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}=\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
157 155 156 oveq12d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}-1\right)+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}=\sum _{{k}=1}^{{n}-1}\left(\Lambda \left({k}\right)\mathrm{log}{k}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{k}}{{m}}\right)\right)+\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
158 138 146 157 3eqtr4d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)={S}\left({n}-1\right)+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}$
159 158 oveq1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)-{S}\left({n}-1\right)={S}\left({n}-1\right)+\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}\right)-{S}\left({n}-1\right)$
160 vmage0 ${⊢}{m}\in ℕ\to 0\le \Lambda \left({m}\right)$
161 34 160 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to 0\le \Lambda \left({m}\right)$
162 vmage0 ${⊢}\frac{{n}}{{m}}\in ℕ\to 0\le \Lambda \left(\frac{{n}}{{m}}\right)$
163 39 162 syl ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to 0\le \Lambda \left(\frac{{n}}{{m}}\right)$
164 36 41 161 163 mulge0d ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to 0\le \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
165 31 42 164 fsumge0 ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
166 43 165 absidd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right|=\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
167 vmage0 ${⊢}{n}\in ℕ\to 0\le \Lambda \left({n}\right)$
168 23 167 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)$
169 23 nnge1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\le {n}$
170 64 169 logge0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \mathrm{log}{n}$
171 45 46 168 170 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)\mathrm{log}{n}$
172 47 171 absidd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\Lambda \left({n}\right)\mathrm{log}{n}\right|=\Lambda \left({n}\right)\mathrm{log}{n}$
173 166 172 oveq12d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right|+\left|\Lambda \left({n}\right)\mathrm{log}{n}\right|=\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)+\Lambda \left({n}\right)\mathrm{log}{n}$
174 101 159 173 3eqtr4d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {S}\left({n}\right)-{S}\left({n}-1\right)=\left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right|+\left|\Lambda \left({n}\right)\mathrm{log}{n}\right|$
175 98 174 breqtrrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right|\le {S}\left({n}\right)-{S}\left({n}-1\right)$
176 94 72 63 95 175 lemul2ad ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\right|\left|\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right|\le \left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)$
177 93 176 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\le \left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)$
178 20 89 73 177 fsumle ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)$
179 85 90 74 91 178 letrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)$
180 85 74 51 179 lediv1dd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\le \frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}$
181 86 75 61 180 lesub2dd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)\le \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\right)$
182 59 78 absmuld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\mathrm{log}{x}\right|=\left|{R}\left({x}\right)\right|\left|\mathrm{log}{x}\right|$
183 6 13 logge0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 0\le \mathrm{log}{x}$
184 18 183 absidd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\mathrm{log}{x}\right|=\mathrm{log}{x}$
185 184 oveq2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\left|\mathrm{log}{x}\right|=\left|{R}\left({x}\right)\right|\mathrm{log}{x}$
186 182 185 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\mathrm{log}{x}\right|=\left|{R}\left({x}\right)\right|\mathrm{log}{x}$
187 80 78 81 absdivd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right|=\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\left|\mathrm{log}{x}\right|}$
188 184 oveq2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\left|\mathrm{log}{x}\right|}=\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}$
189 187 188 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right|=\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}$
190 186 189 oveq12d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\mathrm{log}{x}\right|-\left|\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right|=\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\right)$
191 79 82 abs2difd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\mathrm{log}{x}\right|-\left|\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right|\le \left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|$
192 190 191 eqbrtrrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\left|\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)\right|}{\mathrm{log}{x}}\right)\le \left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|$
193 76 87 84 181 192 letrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)\le \left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|$
194 76 84 14 193 lediv1dd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\le \frac{\left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|}{{x}}$
195 53 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\in ℂ$
196 6 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\in ℂ$
197 14 rpne0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\ne 0$
198 195 196 197 absdivd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|=\frac{\left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|}{\left|{x}\right|}$
199 14 rpge0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 0\le {x}$
200 6 199 absidd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|{x}\right|={x}$
201 200 oveq2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|}{\left|{x}\right|}=\frac{\left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|}{{x}}$
202 198 201 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|=\frac{\left|{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)\right|}{{x}}$
203 194 202 breqtrrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\le \left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|$
204 203 adantrr ${⊢}\left(\top \wedge \left({x}\in \left(1,\mathrm{+\infty }\right)\wedge 1\le {x}\right)\right)\to \frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\le \left|\frac{{R}\left({x}\right)\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{R}\left(\frac{{x}}{{n}}\right)\left(\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)-\Lambda \left({n}\right)\mathrm{log}{n}\right)}{\mathrm{log}{x}}\right)}{{x}}\right|$
205 3 57 58 77 204 lo1le ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\right)\in \le 𝑂\left(1\right)$
206 205 mptru ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\left|{R}\left({x}\right)\right|\mathrm{log}{x}-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left|{R}\left(\frac{{x}}{{n}}\right)\right|\left({S}\left({n}\right)-{S}\left({n}-1\right)\right)}{\mathrm{log}{x}}\right)}{{x}}\right)\in \le 𝑂\left(1\right)$