# Metamath Proof Explorer

## Theorem selberglem2

Description: Lemma for selberg . (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Hypothesis selberglem1.t ${⊢}{T}=\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{n}}$
Assertion selberglem2 ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 selberglem1.t ${⊢}{T}=\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{n}}$
2 reex ${⊢}ℝ\in \mathrm{V}$
3 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
4 2 3 ssexi ${⊢}{ℝ}^{+}\in \mathrm{V}$
5 4 a1i ${⊢}\top \to {ℝ}^{+}\in \mathrm{V}$
6 fzfid ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
7 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
8 7 adantl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℕ$
9 mucl ${⊢}{n}\in ℕ\to \mu \left({n}\right)\in ℤ$
10 8 9 syl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℤ$
11 10 zred ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℝ$
12 11 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℂ$
13 fzfid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\in \mathrm{Fin}$
14 elfznn ${⊢}{m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\to {m}\in ℕ$
15 14 adantl ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\in ℕ$
16 15 nnrpd ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\in {ℝ}^{+}$
17 16 relogcld ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \mathrm{log}{m}\in ℝ$
18 17 resqcld ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {\mathrm{log}{m}}^{2}\in ℝ$
19 13 18 fsumrecl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}\in ℝ$
20 simplr ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in {ℝ}^{+}$
21 19 20 rerpdivcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\in ℝ$
22 21 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\in ℂ$
23 simpr ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
24 7 nnrpd ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in {ℝ}^{+}$
25 rpdivcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
26 23 24 25 syl2an ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
27 26 relogcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
28 27 resqcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ$
29 2re ${⊢}2\in ℝ$
30 remulcl ${⊢}\left(2\in ℝ\wedge \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ\right)\to 2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
31 29 27 30 sylancr ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
32 resubcl ${⊢}\left(2\in ℝ\wedge 2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ\right)\to 2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
33 29 31 32 sylancr ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
34 28 33 readdcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
35 34 8 nndivred ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{n}}\in ℝ$
36 1 35 eqeltrid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {T}\in ℝ$
37 36 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {T}\in ℂ$
38 22 37 subcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\in ℂ$
39 12 38 mulcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\in ℂ$
40 6 39 fsumcl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\in ℂ$
41 12 37 mulcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right){T}\in ℂ$
42 6 41 fsumcl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}\in ℂ$
43 2cn ${⊢}2\in ℂ$
44 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
45 44 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℝ$
46 45 recnd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℂ$
47 mulcl ${⊢}\left(2\in ℂ\wedge \mathrm{log}{x}\in ℂ\right)\to 2\mathrm{log}{x}\in ℂ$
48 43 46 47 sylancr ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to 2\mathrm{log}{x}\in ℂ$
49 42 48 subcld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\in ℂ$
50 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right)$
51 eqidd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)$
52 5 40 49 50 51 offval2 ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right){+}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)$
53 40 42 48 addsubassd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}=\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}$
54 rpcnne0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
55 54 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
56 55 simpld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℂ$
57 11 adantr ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \mu \left({n}\right)\in ℝ$
58 57 18 remulcld ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \mu \left({n}\right){\mathrm{log}{m}}^{2}\in ℝ$
59 13 58 fsumrecl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}\in ℝ$
60 59 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}\in ℂ$
61 55 simprd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\ne 0$
62 6 56 60 61 fsumdivc ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)$
63 18 recnd ${⊢}\left(\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {\mathrm{log}{m}}^{2}\in ℂ$
64 13 63 fsumcl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}\in ℂ$
65 55 adantr ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
66 divass ${⊢}\left(\mu \left({n}\right)\in ℂ\wedge \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\mu \left({n}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}=\mu \left({n}\right)\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)$
67 12 64 65 66 syl3anc ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}=\mu \left({n}\right)\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)$
68 13 12 63 fsummulc2 ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}$
69 68 oveq1d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}=\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}$
70 22 37 npcand ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}+{T}=\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}$
71 70 oveq2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}+{T}\right)=\mu \left({n}\right)\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)$
72 12 38 37 adddid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}+{T}\right)=\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\mu \left({n}\right){T}$
73 71 72 eqtr3d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)=\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\mu \left({n}\right){T}$
74 67 69 73 3eqtr3d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}=\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\mu \left({n}\right){T}$
75 74 sumeq2dv ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\mu \left({n}\right){T}\right)$
76 6 39 41 fsumadd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\mu \left({n}\right){T}\right)=\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}$
77 62 75 76 3eqtrrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}=\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}$
78 77 oveq1d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}$
79 53 78 eqtr3d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}$
80 79 mpteq2dva ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)+\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}\right)$
81 52 80 eqtrd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right){+}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)=\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}\right)$
82 1red ${⊢}\top \to 1\in ℝ$
83 6 28 fsumrecl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ$
84 83 23 rerpdivcld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\in ℝ$
85 84 recnd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\in ℂ$
86 2cnd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to 2\in ℂ$
87 2nn0 ${⊢}2\in {ℕ}_{0}$
88 logexprlim
89 87 88 mp1i
90 2cnd ${⊢}\top \to 2\in ℂ$
91 rlimconst
92 3 90 91 sylancr
93 85 86 89 92 rlimadd
94 rlimo1
95 93 94 syl ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\right)\in 𝑂\left(1\right)$
96 readdcl ${⊢}\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\in ℝ\wedge 2\in ℝ\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\in ℝ$
97 84 29 96 sylancl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\in ℝ$
98 40 abscld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\in ℝ$
99 97 recnd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\in ℂ$
100 99 abscld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\right|\in ℝ$
101 39 abscld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\in ℝ$
102 6 101 fsumrecl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\in ℝ$
103 6 39 fsumabs ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}\left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|$
104 readdcl ${⊢}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ\wedge 2\in ℝ\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\in ℝ$
105 28 29 104 sylancl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\in ℝ$
106 105 20 rerpdivcld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\in ℝ$
107 6 106 fsumrecl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\right)\in ℝ$
108 38 abscld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\in ℝ$
109 12 38 absmuld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|=\left|\mu \left({n}\right)\right|\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
110 12 abscld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\in ℝ$
111 1red ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in ℝ$
112 38 absge0d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
113 mule1 ${⊢}{n}\in ℕ\to \left|\mu \left({n}\right)\right|\le 1$
114 8 113 syl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\le 1$
115 110 111 108 112 114 lemul1ad ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le 1\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
116 108 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\in ℂ$
117 116 mulid2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|=\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
118 115 117 breqtrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
119 109 118 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
120 65 simpld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℂ$
121 120 38 absmuld ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{x}\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|=\left|{x}\right|\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
122 120 22 37 subdid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)={x}\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{x}{T}$
123 65 simprd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\ne 0$
124 64 120 123 divcan2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}$
125 34 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
126 8 nnrpd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in {ℝ}^{+}$
127 rpcnne0 ${⊢}{n}\in {ℝ}^{+}\to \left({n}\in ℂ\wedge {n}\ne 0\right)$
128 126 127 syl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({n}\in ℂ\wedge {n}\ne 0\right)$
129 divass ${⊢}\left({x}\in ℂ\wedge {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{{x}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{{n}}={x}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{n}}\right)$
130 1 oveq2i ${⊢}{x}{T}={x}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{n}}\right)$
131 129 130 syl6eqr ${⊢}\left({x}\in ℂ\wedge {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{{x}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{{n}}={x}{T}$
132 div23 ${⊢}\left({x}\in ℂ\wedge {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{{x}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)}{{n}}=\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
133 131 132 eqtr3d ${⊢}\left({x}\in ℂ\wedge {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to {x}{T}=\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
134 120 125 128 133 syl3anc ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}{T}=\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
135 124 134 oveq12d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{x}{T}=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
136 122 135 eqtrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
137 136 fveq2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{x}\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|=\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\right|$
138 rprege0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0\le {x}\right)$
139 absid ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to \left|{x}\right|={x}$
140 20 138 139 3syl ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{x}\right|={x}$
141 140 oveq1d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{x}\right|\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|={x}\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
142 121 137 141 3eqtr3d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\right|={x}\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|$
143 8 nncnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℂ$
144 143 mulid2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}={n}$
145 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
146 145 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
147 fznnfl ${⊢}{x}\in ℝ\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
148 146 147 syl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
149 148 simplbda ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\le {x}$
150 144 149 eqbrtrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}\le {x}$
151 20 rpred ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℝ$
152 111 151 126 lemuldivd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1{n}\le {x}↔1\le \frac{{x}}{{n}}\right)$
153 150 152 mpbid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\le \frac{{x}}{{n}}$
154 log2sumbnd ${⊢}\left(\frac{{x}}{{n}}\in {ℝ}^{+}\wedge 1\le \frac{{x}}{{n}}\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\right|\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2$
155 26 153 154 syl2anc ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}-\left(\frac{{x}}{{n}}\right)\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2-2\mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\right|\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2$
156 142 155 eqbrtrrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2$
157 108 105 20 lemuldiv2d ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2↔\left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\right)$
158 156 157 mpbid ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right|\le \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}$
159 101 108 106 119 158 letrd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}$
160 6 101 106 159 fsumle ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\right)$
161 6 105 fsumrecl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)\in ℝ$
162 remulcl ${⊢}\left({x}\in ℝ\wedge 2\in ℝ\right)\to {x}\cdot 2\in ℝ$
163 146 29 162 sylancl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\cdot 2\in ℝ$
164 83 163 readdcld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2\in ℝ$
165 28 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℂ$
166 2cnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\in ℂ$
167 6 165 166 fsumadd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)=\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+\sum _{{n}=1}^{⌊{x}⌋}2$
168 fsumconst ${⊢}\left(\left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}\wedge 2\in ℂ\right)\to \sum _{{n}=1}^{⌊{x}⌋}2=\left|\left(1\dots ⌊{x}⌋\right)\right|\cdot 2$
169 6 43 168 sylancl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}2=\left|\left(1\dots ⌊{x}⌋\right)\right|\cdot 2$
170 138 adantl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left({x}\in ℝ\wedge 0\le {x}\right)$
171 flge0nn0 ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to ⌊{x}⌋\in {ℕ}_{0}$
172 hashfz1 ${⊢}⌊{x}⌋\in {ℕ}_{0}\to \left|\left(1\dots ⌊{x}⌋\right)\right|=⌊{x}⌋$
173 170 171 172 3syl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\left(1\dots ⌊{x}⌋\right)\right|=⌊{x}⌋$
174 173 oveq1d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\left(1\dots ⌊{x}⌋\right)\right|\cdot 2=⌊{x}⌋\cdot 2$
175 169 174 eqtrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}2=⌊{x}⌋\cdot 2$
176 175 oveq2d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+\sum _{{n}=1}^{⌊{x}⌋}2=\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+⌊{x}⌋\cdot 2$
177 167 176 eqtrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)=\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+⌊{x}⌋\cdot 2$
178 reflcl ${⊢}{x}\in ℝ\to ⌊{x}⌋\in ℝ$
179 146 178 syl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to ⌊{x}⌋\in ℝ$
180 29 a1i ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to 2\in ℝ$
181 179 180 remulcld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to ⌊{x}⌋\cdot 2\in ℝ$
182 flle ${⊢}{x}\in ℝ\to ⌊{x}⌋\le {x}$
183 146 182 syl ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to ⌊{x}⌋\le {x}$
184 2pos ${⊢}0<2$
185 29 184 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
186 185 a1i ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(2\in ℝ\wedge 0<2\right)$
187 lemul1 ${⊢}\left(⌊{x}⌋\in ℝ\wedge {x}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(⌊{x}⌋\le {x}↔⌊{x}⌋\cdot 2\le {x}\cdot 2\right)$
188 179 146 186 187 syl3anc ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(⌊{x}⌋\le {x}↔⌊{x}⌋\cdot 2\le {x}\cdot 2\right)$
189 183 188 mpbid ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to ⌊{x}⌋\cdot 2\le {x}\cdot 2$
190 181 163 83 189 leadd2dd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+⌊{x}⌋\cdot 2\le \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2$
191 177 190 eqbrtrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)\le \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2$
192 161 164 23 191 lediv1dd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)}{{x}}\le \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2}{{x}}$
193 105 recnd ${⊢}\left(\left(\top \wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\in ℂ$
194 6 56 193 61 fsumdivc ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2\right)}{{x}}=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\right)$
195 83 recnd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℂ$
196 56 86 mulcld ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to {x}\cdot 2\in ℂ$
197 divdir ${⊢}\left(\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℂ\wedge {x}\cdot 2\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2}{{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+\left(\frac{{x}\cdot 2}{{x}}\right)$
198 195 196 55 197 syl3anc ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2}{{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+\left(\frac{{x}\cdot 2}{{x}}\right)$
199 86 56 61 divcan3d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{{x}\cdot 2}{{x}}=2$
200 199 oveq2d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+\left(\frac{{x}\cdot 2}{{x}}\right)=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2$
201 198 200 eqtrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+{x}\cdot 2}{{x}}=\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2$
202 192 194 201 3brtr3d ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}+2}{{x}}\right)\le \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2$
203 102 107 97 160 202 letrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left|\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2$
204 98 102 97 103 203 letrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2$
205 97 leabsd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\le \left|\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\right|$
206 98 97 100 204 205 letrd ${⊢}\left(\top \wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \left|\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\right|$
207 206 adantrr ${⊢}\left(\top \wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right|\le \left|\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{{x}}\right)+2\right|$
208 82 95 97 40 207 o1le ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right)\in 𝑂\left(1\right)$
209 1 selberglem1 ${⊢}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
210 o1add ${⊢}\left(\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right)\in 𝑂\left(1\right)\wedge \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right){+}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
211 208 209 210 sylancl ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right)\left(\left(\frac{\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}{\mathrm{log}{m}}^{2}}{{x}}\right)-{T}\right)\right){+}_{f}\left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\mu \left({n}\right){T}-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
212 81 211 eqeltrrd ${⊢}\top \to \left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
213 212 mptru ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right){\mathrm{log}{m}}^{2}}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$