# Metamath Proof Explorer

## Theorem vmalogdivsum2

Description: The sum sum_ n <_ x , Lam ( n ) log ( x / n ) / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . Exercise 9.1.7 of Shapiro, p. 336. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion vmalogdivsum2 ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 fzfid ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
2 elfznn ${⊢}{k}\in \left(1\dots ⌊{x}⌋\right)\to {k}\in ℕ$
3 2 adantl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to {k}\in ℕ$
4 3 nnrpd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to {k}\in {ℝ}^{+}$
5 4 relogcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}{k}\in ℝ$
6 5 3 nndivred ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}{k}}{{k}}\in ℝ$
7 1 6 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)\in ℝ$
8 7 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)\in ℂ$
9 elioore ${⊢}{x}\in \left(1,\mathrm{+\infty }\right)\to {x}\in ℝ$
10 9 adantl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
11 1rp ${⊢}1\in {ℝ}^{+}$
12 11 a1i ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\in {ℝ}^{+}$
13 1red ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\in ℝ$
14 eliooord ${⊢}{x}\in \left(1,\mathrm{+\infty }\right)\to \left(1<{x}\wedge {x}<\mathrm{+\infty }\right)$
15 14 adantl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(1<{x}\wedge {x}<\mathrm{+\infty }\right)$
16 15 simpld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1<{x}$
17 13 10 16 ltled ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\le {x}$
18 10 12 17 rpgecld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {x}\in {ℝ}^{+}$
19 18 relogcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℝ$
20 19 resqcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {\mathrm{log}{x}}^{2}\in ℝ$
21 20 rehalfcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{\mathrm{log}{x}}^{2}}{2}\in ℝ$
22 21 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{\mathrm{log}{x}}^{2}}{2}\in ℂ$
23 19 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℂ$
24 10 16 rplogcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in {ℝ}^{+}$
25 24 rpne0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\ne 0$
26 8 22 23 25 divsubdird ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)}{\mathrm{log}{x}}=\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\frac{{\mathrm{log}{x}}^{2}}{2}}{\mathrm{log}{x}}\right)$
27 7 21 resubcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\in ℝ$
28 27 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\in ℂ$
29 28 23 25 divrecd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)}{\mathrm{log}{x}}=\left(\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\left(\frac{1}{\mathrm{log}{x}}\right)$
30 20 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {\mathrm{log}{x}}^{2}\in ℂ$
31 2cnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 2\in ℂ$
32 2ne0 ${⊢}2\ne 0$
33 32 a1i ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 2\ne 0$
34 30 31 23 33 25 divdiv32d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\frac{{\mathrm{log}{x}}^{2}}{2}}{\mathrm{log}{x}}=\frac{\frac{{\mathrm{log}{x}}^{2}}{\mathrm{log}{x}}}{2}$
35 23 sqvald ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to {\mathrm{log}{x}}^{2}=\mathrm{log}{x}\mathrm{log}{x}$
36 35 oveq1d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{\mathrm{log}{x}}^{2}}{\mathrm{log}{x}}=\frac{\mathrm{log}{x}\mathrm{log}{x}}{\mathrm{log}{x}}$
37 23 23 25 divcan3d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}\mathrm{log}{x}}{\mathrm{log}{x}}=\mathrm{log}{x}$
38 36 37 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{{\mathrm{log}{x}}^{2}}{\mathrm{log}{x}}=\mathrm{log}{x}$
39 38 oveq1d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\frac{{\mathrm{log}{x}}^{2}}{\mathrm{log}{x}}}{2}=\frac{\mathrm{log}{x}}{2}$
40 34 39 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\frac{{\mathrm{log}{x}}^{2}}{2}}{\mathrm{log}{x}}=\frac{\mathrm{log}{x}}{2}$
41 40 oveq2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\frac{{\mathrm{log}{x}}^{2}}{2}}{\mathrm{log}{x}}\right)=\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)$
42 26 29 41 3eqtr3rd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)=\left(\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\left(\frac{1}{\mathrm{log}{x}}\right)$
43 42 mpteq2dva ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)=\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\left(\frac{1}{\mathrm{log}{x}}\right)\right)$
44 24 rprecred ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{1}{\mathrm{log}{x}}\in ℝ$
45 18 ex ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)\to {x}\in {ℝ}^{+}\right)$
46 45 ssrdv ${⊢}\top \to \left(1,\mathrm{+\infty }\right)\subseteq {ℝ}^{+}$
47 eqid ${⊢}\left({x}\in {ℝ}^{+}⟼\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)$
48 47 logdivsum
49 48 simp2i
50 rlimdmo1
51 49 50 mp1i ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\in 𝑂\left(1\right)$
52 46 51 o1res2 ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\in 𝑂\left(1\right)$
53 divlogrlim
54 rlimo1
55 53 54 mp1i ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{1}{\mathrm{log}{x}}\right)\in 𝑂\left(1\right)$
56 27 44 52 55 o1mul2 ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\left(\frac{{\mathrm{log}{x}}^{2}}{2}\right)\right)\left(\frac{1}{\mathrm{log}{x}}\right)\right)\in 𝑂\left(1\right)$
57 43 56 eqeltrd ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)$
58 8 23 25 divcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\in ℂ$
59 23 halfcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}}{2}\in ℂ$
60 58 59 subcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\in ℂ$
61 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
62 61 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 ℕ$
63 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
64 62 63 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 ℝ$
65 64 62 nndivred ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\Lambda \left({n}\right)}{{n}}\in ℝ$
66 18 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 {ℝ}^{+}$
67 62 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 {ℝ}^{+}$
68 66 67 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 {ℝ}^{+}$
69 68 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}\left(\frac{{x}}{{n}}\right)\in ℝ$
70 65 69 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
71 1 70 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
72 71 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
73 24 rpcnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in ℂ$
74 72 73 25 divcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\in ℂ$
75 73 halfcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}}{2}\in ℂ$
76 74 75 subcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\in ℂ$
77 58 74 59 nnncan2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)-\left(\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)=\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)$
78 8 72 23 25 divsubdird ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}=\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)$
79 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 ⌊\frac{{x}}{{n}}⌋\right)\in \mathrm{Fin}$
80 64 adantr ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
81 62 adantr ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {n}\in ℕ$
82 elfznn ${⊢}{m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\to {m}\in ℕ$
83 82 adantl ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\in ℕ$
84 81 83 nnmulcld ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {n}{m}\in ℕ$
85 80 84 nndivred ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\Lambda \left({n}\right)}{{n}{m}}\in ℝ$
86 79 85 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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)\in ℝ$
87 86 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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)\in ℂ$
88 70 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
89 1 87 88 fsumsub ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)$
90 64 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)\in ℂ$
91 62 nncnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℂ$
92 62 nnne0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\ne 0$
93 90 91 92 divcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\Lambda \left({n}\right)}{{n}}\in ℂ$
94 83 nnrecred ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{1}{{m}}\in ℝ$
95 79 94 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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\in ℝ$
96 95 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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\in ℂ$
97 69 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
98 93 96 97 subdid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)=\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)$
99 90 adantr ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \Lambda \left({n}\right)\in ℂ$
100 91 adantr ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {n}\in ℂ$
101 83 nncnd ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\in ℂ$
102 92 adantr ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {n}\ne 0$
103 83 nnne0d ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\ne 0$
104 99 100 101 102 103 divdiv1d ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\frac{\Lambda \left({n}\right)}{{n}}}{{m}}=\frac{\Lambda \left({n}\right)}{{n}{m}}$
105 99 100 102 divcld ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\Lambda \left({n}\right)}{{n}}\in ℂ$
106 105 101 103 divrecd ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\frac{\Lambda \left({n}\right)}{{n}}}{{m}}=\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\frac{1}{{m}}\right)$
107 104 106 eqtr3d ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\Lambda \left({n}\right)}{{n}{m}}=\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\frac{1}{{m}}\right)$
108 107 sumeq2dv ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\frac{1}{{m}}\right)$
109 101 103 reccld ${⊢}\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(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{1}{{m}}\in ℂ$
110 79 93 109 fsummulc2 ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\frac{1}{{m}}\right)$
111 108 110 eqtr4d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)=\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)$
112 111 oveq1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)=\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)$
113 98 112 eqtr4d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)$
114 113 sumeq2dv ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
115 vmasum ${⊢}{k}\in ℕ\to \sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({n}\right)=\mathrm{log}{k}$
116 3 115 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({n}\right)=\mathrm{log}{k}$
117 116 oveq1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({n}\right)}{{k}}=\frac{\mathrm{log}{k}}{{k}}$
118 fzfid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots {k}\right)\in \mathrm{Fin}$
119 dvdsssfz1 ${⊢}{k}\in ℕ\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq \left(1\dots {k}\right)$
120 3 119 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq \left(1\dots {k}\right)$
121 118 120 ssfid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {k}\right\}\in \mathrm{Fin}$
122 3 nncnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to {k}\in ℂ$
123 ssrab2 ${⊢}\left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq ℕ$
124 simprr ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}$
125 123 124 sseldi ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to {n}\in ℕ$
126 125 63 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \Lambda \left({n}\right)\in ℝ$
127 126 recnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \Lambda \left({n}\right)\in ℂ$
128 127 anassrs ${⊢}\left(\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to \Lambda \left({n}\right)\in ℂ$
129 3 nnne0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to {k}\ne 0$
130 121 122 128 129 fsumdivc ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\Lambda \left({n}\right)}{{k}}=\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\left(\frac{\Lambda \left({n}\right)}{{k}}\right)$
131 117 130 eqtr3d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}{k}}{{k}}=\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\left(\frac{\Lambda \left({n}\right)}{{k}}\right)$
132 131 sumeq2dv ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)=\sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\left(\frac{\Lambda \left({n}\right)}{{k}}\right)$
133 oveq2 ${⊢}{k}={n}{m}\to \frac{\Lambda \left({n}\right)}{{k}}=\frac{\Lambda \left({n}\right)}{{n}{m}}$
134 2 ad2antrl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to {k}\in ℕ$
135 134 nncnd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to {k}\in ℂ$
136 134 nnne0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to {k}\ne 0$
137 127 135 136 divcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \frac{\Lambda \left({n}\right)}{{k}}\in ℂ$
138 133 10 137 dvdsflsumcom ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\left(\frac{\Lambda \left({n}\right)}{{k}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)$
139 132 138 eqtrd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)$
140 139 oveq1d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}{m}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)$
141 89 114 140 3eqtr4rd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
142 141 oveq1d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}=\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}$
143 77 78 142 3eqtr2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)-\left(\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)=\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}$
144 143 mpteq2dva ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)-\left(\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\right)=\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\right)$
145 1red ${⊢}\top \to 1\in ℝ$
146 1 65 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\in ℝ$
147 146 24 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\in ℝ$
148 ioossre ${⊢}\left(1,\mathrm{+\infty }\right)\subseteq ℝ$
149 ax-1cn ${⊢}1\in ℂ$
150 o1const ${⊢}\left(\left(1,\mathrm{+\infty }\right)\subseteq ℝ\wedge 1\in ℂ\right)\to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼1\right)\in 𝑂\left(1\right)$
151 148 149 150 mp2an ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼1\right)\in 𝑂\left(1\right)$
152 151 a1i ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼1\right)\in 𝑂\left(1\right)$
153 147 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\in ℂ$
154 12 rpcnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 1\in ℂ$
155 146 recnd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\in ℂ$
156 155 23 23 25 divsubdird ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}}{\mathrm{log}{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{\mathrm{log}{x}}\right)$
157 155 23 subcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\in ℂ$
158 157 23 25 divrecd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}}{\mathrm{log}{x}}=\left(\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\left(\frac{1}{\mathrm{log}{x}}\right)$
159 23 25 dividd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}}{\mathrm{log}{x}}=1$
160 159 oveq2d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{\mathrm{log}{x}}\right)=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-1$
161 156 158 160 3eqtr3rd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-1=\left(\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\left(\frac{1}{\mathrm{log}{x}}\right)$
162 161 mpteq2dva ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-1\right)=\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\left(\frac{1}{\mathrm{log}{x}}\right)\right)$
163 146 19 resubcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\in ℝ$
164 vmadivsum ${⊢}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
165 164 a1i ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
166 46 165 o1res2 ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
167 163 44 166 55 o1mul2 ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)-\mathrm{log}{x}\right)\left(\frac{1}{\mathrm{log}{x}}\right)\right)\in 𝑂\left(1\right)$
168 162 167 eqeltrd ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)-1\right)\in 𝑂\left(1\right)$
169 153 154 168 o1dif ${⊢}\top \to \left(\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)\in 𝑂\left(1\right)↔\left({x}\in \left(1,\mathrm{+\infty }\right)⟼1\right)\in 𝑂\left(1\right)\right)$
170 152 169 mpbird ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)\in 𝑂\left(1\right)$
171 147 170 o1lo1d ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}\right)\in \le 𝑂\left(1\right)$
172 95 69 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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
173 65 172 remulcld ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\in ℝ$
174 1 173 fsumrecl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\in ℝ$
175 174 24 rerpdivcld ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\in ℝ$
176 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 ℝ$
177 vmage0 ${⊢}{n}\in ℕ\to 0\le \Lambda \left({n}\right)$
178 62 177 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)$
179 64 67 178 divge0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \frac{\Lambda \left({n}\right)}{{n}}$
180 68 rpred ${⊢}\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 ℝ$
181 91 mulid2d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}={n}$
182 fznnfl ${⊢}{x}\in ℝ\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
183 10 182 syl ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
184 183 simplbda ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\le {x}$
185 181 184 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}\le {x}$
186 10 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 ℝ$
187 176 186 67 lemuldivd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1{n}\le {x}↔1\le \frac{{x}}{{n}}\right)$
188 185 187 mpbid ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\le \frac{{x}}{{n}}$
189 harmonicubnd ${⊢}\left(\frac{{x}}{{n}}\in ℝ\wedge 1\le \frac{{x}}{{n}}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\le \mathrm{log}\left(\frac{{x}}{{n}}\right)+1$
190 180 188 189 syl2anc ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\le \mathrm{log}\left(\frac{{x}}{{n}}\right)+1$
191 95 69 176 lesubadd2d ${⊢}\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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1↔\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\le \mathrm{log}\left(\frac{{x}}{{n}}\right)+1\right)$
192 190 191 mpbird ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1$
193 172 176 65 179 192 lemul2ad ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\le \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\cdot 1$
194 93 mulid1d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\cdot 1=\frac{\Lambda \left({n}\right)}{{n}}$
195 193 194 breqtrd ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\le \frac{\Lambda \left({n}\right)}{{n}}$
196 1 173 65 195 fsumle ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\le \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)$
197 174 146 24 196 lediv1dd ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\le \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}$
198 197 adantrr ${⊢}\left(\top \wedge \left({x}\in \left(1,\mathrm{+\infty }\right)\wedge 1\le {x}\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\le \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)}{\mathrm{log}{x}}$
199 145 171 147 175 198 lo1le ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\right)\in \le 𝑂\left(1\right)$
200 0red ${⊢}\top \to 0\in ℝ$
201 harmoniclbnd ${⊢}\frac{{x}}{{n}}\in {ℝ}^{+}\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)$
202 68 201 syl ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)$
203 95 69 subge0d ${⊢}\left(\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(0\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)↔\mathrm{log}\left(\frac{{x}}{{n}}\right)\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)\right)$
204 202 203 mpbird ${⊢}\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}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)$
205 65 172 179 204 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 \left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
206 1 173 205 fsumge0 ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 0\le \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
207 174 24 206 divge0d ${⊢}\left(\top \wedge {x}\in \left(1,\mathrm{+\infty }\right)\right)\to 0\le \frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}$
208 175 200 207 o1lo12 ${⊢}\top \to \left(\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\right)\in 𝑂\left(1\right)↔\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\right)\in \le 𝑂\left(1\right)\right)$
209 199 208 mpbird ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\left(\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{1}{{m}}\right)-\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{\mathrm{log}{x}}\right)\in 𝑂\left(1\right)$
210 144 209 eqeltrd ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)-\left(\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\right)\in 𝑂\left(1\right)$
211 60 76 210 o1dif ${⊢}\top \to \left(\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{k}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}{k}}{{k}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)↔\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)\right)$
212 57 211 mpbid ${⊢}\top \to \left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)$
213 212 mptru ${⊢}\left({x}\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\Lambda \left({n}\right)}{{n}}\right)\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\mathrm{log}{x}}\right)-\left(\frac{\mathrm{log}{x}}{2}\right)\right)\in 𝑂\left(1\right)$