# Metamath Proof Explorer

## Theorem mulog2sumlem2

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 19-May-2016)

Ref Expression
Hypotheses logdivsum.1 ${⊢}{F}=\left({y}\in {ℝ}^{+}⟼\sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)-\left(\frac{{\mathrm{log}{y}}^{2}}{2}\right)\right)$
mulog2sumlem.1
mulog2sumlem2.t ${⊢}{T}=\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}$
mulog2sumlem2.r ${⊢}{R}=\left(\frac{1}{2}\right)+\left(\gamma +\left|{L}\right|\right)+\sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
Assertion mulog2sumlem2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 logdivsum.1 ${⊢}{F}=\left({y}\in {ℝ}^{+}⟼\sum _{{i}=1}^{⌊{y}⌋}\left(\frac{\mathrm{log}{i}}{{i}}\right)-\left(\frac{{\mathrm{log}{y}}^{2}}{2}\right)\right)$
2 mulog2sumlem.1
3 mulog2sumlem2.t ${⊢}{T}=\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}$
4 mulog2sumlem2.r ${⊢}{R}=\left(\frac{1}{2}\right)+\left(\gamma +\left|{L}\right|\right)+\sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
5 1red ${⊢}{\phi }\to 1\in ℝ$
6 2re ${⊢}2\in ℝ$
7 fzfid ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
8 simpr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
9 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
10 9 nnrpd ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in {ℝ}^{+}$
11 rpdivcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
12 8 10 11 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
13 12 relogcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
14 simplr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in {ℝ}^{+}$
15 13 14 rerpdivcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\in ℝ$
16 7 15 fsumrecl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ$
17 remulcl ${⊢}\left(2\in ℝ\wedge \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ$
18 6 16 17 sylancr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ$
19 halfre ${⊢}\frac{1}{2}\in ℝ$
20 emre ${⊢}\gamma \in ℝ$
21 rlimcl
22 2 21 syl ${⊢}{\phi }\to {L}\in ℂ$
23 22 abscld ${⊢}{\phi }\to \left|{L}\right|\in ℝ$
24 readdcl ${⊢}\left(\gamma \in ℝ\wedge \left|{L}\right|\in ℝ\right)\to \gamma +\left|{L}\right|\in ℝ$
25 20 23 24 sylancr ${⊢}{\phi }\to \gamma +\left|{L}\right|\in ℝ$
26 readdcl ${⊢}\left(\frac{1}{2}\in ℝ\wedge \gamma +\left|{L}\right|\in ℝ\right)\to \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|\in ℝ$
27 19 25 26 sylancr ${⊢}{\phi }\to \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|\in ℝ$
28 fzfid ${⊢}{\phi }\to \left(1\dots 2\right)\in \mathrm{Fin}$
29 epr ${⊢}\mathrm{e}\in {ℝ}^{+}$
30 elfznn ${⊢}{m}\in \left(1\dots 2\right)\to {m}\in ℕ$
31 30 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\in ℕ$
32 31 nnrpd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\in {ℝ}^{+}$
33 rpdivcl ${⊢}\left(\mathrm{e}\in {ℝ}^{+}\wedge {m}\in {ℝ}^{+}\right)\to \frac{\mathrm{e}}{{m}}\in {ℝ}^{+}$
34 29 32 33 sylancr ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\mathrm{e}}{{m}}\in {ℝ}^{+}$
35 34 relogcld ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\in ℝ$
36 35 31 nndivred ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\in ℝ$
37 28 36 fsumrecl ${⊢}{\phi }\to \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)\in ℝ$
38 27 37 readdcld ${⊢}{\phi }\to \left(\frac{1}{2}\right)+\left(\gamma +\left|{L}\right|\right)+\sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)\in ℝ$
39 4 38 eqeltrid ${⊢}{\phi }\to {R}\in ℝ$
40 remulcl ${⊢}\left({R}\in ℝ\wedge 2\in ℝ\right)\to {R}\cdot 2\in ℝ$
41 39 6 40 sylancl ${⊢}{\phi }\to {R}\cdot 2\in ℝ$
42 41 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\cdot 2\in ℝ$
43 6 a1i ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\in ℝ$
44 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
45 2cnd ${⊢}{\phi }\to 2\in ℂ$
46 o1const ${⊢}\left({ℝ}^{+}\subseteq ℝ\wedge 2\in ℂ\right)\to \left({x}\in {ℝ}^{+}⟼2\right)\in 𝑂\left(1\right)$
47 44 45 46 sylancr ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼2\right)\in 𝑂\left(1\right)$
48 logfacrlim2
49 rlimo1
50 48 49 mp1i ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\right)\in 𝑂\left(1\right)$
51 43 16 47 50 o1mul2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\right)\in 𝑂\left(1\right)$
52 41 recnd ${⊢}{\phi }\to {R}\cdot 2\in ℂ$
53 o1const ${⊢}\left({ℝ}^{+}\subseteq ℝ\wedge {R}\cdot 2\in ℂ\right)\to \left({x}\in {ℝ}^{+}⟼{R}\cdot 2\right)\in 𝑂\left(1\right)$
54 44 52 53 sylancr ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼{R}\cdot 2\right)\in 𝑂\left(1\right)$
55 18 42 51 54 o1add2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right)\in 𝑂\left(1\right)$
56 18 42 readdcld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\in ℝ$
57 9 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℕ$
58 mucl ${⊢}{n}\in ℕ\to \mu \left({n}\right)\in ℤ$
59 57 58 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℤ$
60 59 zred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℝ$
61 60 57 nndivred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)}{{n}}\in ℝ$
62 61 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)}{{n}}\in ℂ$
63 13 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
64 63 sqcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℂ$
65 64 halfcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\in ℂ$
66 remulcl ${⊢}\left(\gamma \in ℝ\wedge \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
67 20 13 66 sylancr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
68 67 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
69 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {L}\in ℂ$
70 68 69 subcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\in ℂ$
71 65 70 addcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\in ℂ$
72 3 71 eqeltrid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {T}\in ℂ$
73 62 72 mulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right){T}\in ℂ$
74 7 73 fsumcl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}\in ℂ$
75 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
76 75 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℝ$
77 76 recnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℂ$
78 74 77 subcld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\in ℂ$
79 78 abscld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right|\in ℝ$
80 79 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right|\in ℝ$
81 56 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\in ℝ$
82 56 recnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\in ℂ$
83 82 abscld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right|\in ℝ$
84 83 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right|\in ℝ$
85 59 zcnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\in ℂ$
86 fzfid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\in \mathrm{Fin}$
87 elfznn ${⊢}{m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\to {m}\in ℕ$
88 nnrp ${⊢}{m}\in ℕ\to {m}\in {ℝ}^{+}$
89 rpdivcl ${⊢}\left(\frac{{x}}{{n}}\in {ℝ}^{+}\wedge {m}\in {ℝ}^{+}\right)\to \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}$
90 12 88 89 syl2an ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}$
91 90 relogcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ$
92 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {m}\in ℕ$
93 91 92 nndivred ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℝ$
94 93 recnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℂ$
95 87 94 sylan2 ${⊢}\left(\left(\left({\phi }\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 \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℂ$
96 86 95 fsumcl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℂ$
97 72 96 subcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℂ$
98 57 nncnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℂ$
99 57 nnne0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\ne 0$
100 85 97 98 99 div23d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}=\left(\frac{\mu \left({n}\right)}{{n}}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)$
101 62 72 96 subdid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)=\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
102 100 101 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}=\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
103 102 sumeq2dv ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)$
104 62 96 mulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℂ$
105 7 73 104 fsumsub ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
106 103 105 eqtrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
107 106 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
108 86 62 95 fsummulc2 ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
109 85 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \mu \left({n}\right)\in ℂ$
110 98 99 jca ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({n}\in ℂ\wedge {n}\ne 0\right)$
111 110 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \left({n}\in ℂ\wedge {n}\ne 0\right)$
112 div23 ${⊢}\left(\mu \left({n}\right)\in ℂ\wedge \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)}{{n}}=\left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
113 divass ${⊢}\left(\mu \left({n}\right)\in ℂ\wedge \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)}{{n}}=\mu \left({n}\right)\left(\frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}\right)$
114 112 113 eqtr3d ${⊢}\left(\mu \left({n}\right)\in ℂ\wedge \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\mu \left({n}\right)\left(\frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}\right)$
115 109 94 111 114 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\mu \left({n}\right)\left(\frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}\right)$
116 91 recnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℂ$
117 92 nnrpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {m}\in {ℝ}^{+}$
118 rpcnne0 ${⊢}{m}\in {ℝ}^{+}\to \left({m}\in ℂ\wedge {m}\ne 0\right)$
119 117 118 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \left({m}\in ℂ\wedge {m}\ne 0\right)$
120 divdiv1 ${⊢}\left(\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℂ\wedge \left({m}\in ℂ\wedge {m}\ne 0\right)\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}=\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}{n}}$
121 116 119 111 120 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}=\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}{n}}$
122 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
123 122 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
124 123 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℝ$
125 124 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℂ$
126 125 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {x}\in ℂ$
127 divdiv1 ${⊢}\left({x}\in ℂ\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\wedge \left({m}\in ℂ\wedge {m}\ne 0\right)\right)\to \frac{\frac{{x}}{{n}}}{{m}}=\frac{{x}}{{n}{m}}$
128 126 111 119 127 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\frac{{x}}{{n}}}{{m}}=\frac{{x}}{{n}{m}}$
129 128 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)=\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)$
130 92 nncnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {m}\in ℂ$
131 98 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {n}\in ℂ$
132 130 131 mulcomd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to {m}{n}={n}{m}$
133 129 132 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}{n}}=\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}$
134 121 133 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}=\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}$
135 134 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \mu \left({n}\right)\left(\frac{\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}}{{n}}\right)=\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
136 115 135 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
137 87 136 sylan2 ${⊢}\left(\left(\left({\phi }\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 \left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
138 137 sumeq2dv ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
139 108 138 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
140 139 sumeq2dv ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
141 oveq2 ${⊢}{k}={n}{m}\to \frac{{x}}{{k}}=\frac{{x}}{{n}{m}}$
142 141 fveq2d ${⊢}{k}={n}{m}\to \mathrm{log}\left(\frac{{x}}{{k}}\right)=\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)$
143 id ${⊢}{k}={n}{m}\to {k}={n}{m}$
144 142 143 oveq12d ${⊢}{k}={n}{m}\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}=\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}$
145 144 oveq2d ${⊢}{k}={n}{m}\to \mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)=\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
146 8 rpred ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
147 ssrab2 ${⊢}\left\{{y}\in ℕ|{y}\parallel {k}\right\}\subseteq ℕ$
148 simprr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\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\}$
149 147 148 sseldi ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\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 ℕ$
150 149 58 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \mu \left({n}\right)\in ℤ$
151 150 zred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \mu \left({n}\right)\in ℝ$
152 elfznn ${⊢}{k}\in \left(1\dots ⌊{x}⌋\right)\to {k}\in ℕ$
153 152 adantr ${⊢}\left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to {k}\in ℕ$
154 153 nnrpd ${⊢}\left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\to {k}\in {ℝ}^{+}$
155 rpdivcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {k}\in {ℝ}^{+}\right)\to \frac{{x}}{{k}}\in {ℝ}^{+}$
156 8 154 155 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \frac{{x}}{{k}}\in {ℝ}^{+}$
157 156 relogcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \mathrm{log}\left(\frac{{x}}{{k}}\right)\in ℝ$
158 152 ad2antrl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\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 ℕ$
159 157 158 nndivred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\in ℝ$
160 151 159 remulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)\in ℝ$
161 160 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({k}\in \left(1\dots ⌊{x}⌋\right)\wedge {n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}\right)\right)\to \mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)\in ℂ$
162 145 146 161 dvdsflsumcom ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}{m}}\right)}{{n}{m}}\right)$
163 140 162 eqtr4d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)$
164 163 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)$
165 oveq2 ${⊢}{k}=1\to \frac{{x}}{{k}}=\frac{{x}}{1}$
166 165 fveq2d ${⊢}{k}=1\to \mathrm{log}\left(\frac{{x}}{{k}}\right)=\mathrm{log}\left(\frac{{x}}{1}\right)$
167 id ${⊢}{k}=1\to {k}=1$
168 166 167 oveq12d ${⊢}{k}=1\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}=\frac{\mathrm{log}\left(\frac{{x}}{1}\right)}{1}$
169 fzfid ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
170 fz1ssnn ${⊢}\left(1\dots ⌊{x}⌋\right)\subseteq ℕ$
171 170 a1i ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left(1\dots ⌊{x}⌋\right)\subseteq ℕ$
172 123 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to {x}\in ℝ$
173 simprr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 1\le {x}$
174 flge1nn ${⊢}\left({x}\in ℝ\wedge 1\le {x}\right)\to ⌊{x}⌋\in ℕ$
175 172 173 174 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to ⌊{x}⌋\in ℕ$
176 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
177 175 176 eleqtrdi ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to ⌊{x}⌋\in {ℤ}_{\ge 1}$
178 eluzfz1 ${⊢}⌊{x}⌋\in {ℤ}_{\ge 1}\to 1\in \left(1\dots ⌊{x}⌋\right)$
179 177 178 syl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 1\in \left(1\dots ⌊{x}⌋\right)$
180 152 nnrpd ${⊢}{k}\in \left(1\dots ⌊{x}⌋\right)\to {k}\in {ℝ}^{+}$
181 8 180 155 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{k}}\in {ℝ}^{+}$
182 181 relogcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{k}}\right)\in ℝ$
183 170 a1i ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(1\dots ⌊{x}⌋\right)\subseteq ℕ$
184 183 sselda ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to {k}\in ℕ$
185 182 184 nndivred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\in ℝ$
186 185 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\in ℂ$
187 186 adantlrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\wedge {k}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\in ℂ$
188 168 169 171 179 187 musumsum ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}\sum _{{n}\in \left\{{y}\in ℕ|{y}\parallel {k}\right\}}\mu \left({n}\right)\left(\frac{\mathrm{log}\left(\frac{{x}}{{k}}\right)}{{k}}\right)=\frac{\mathrm{log}\left(\frac{{x}}{1}\right)}{1}$
189 8 rpcnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℂ$
190 189 div1d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{{x}}{1}={x}$
191 190 fveq2d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}\left(\frac{{x}}{1}\right)=\mathrm{log}{x}$
192 191 oveq1d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}\left(\frac{{x}}{1}\right)}{1}=\frac{\mathrm{log}{x}}{1}$
193 77 div1d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}{x}}{1}=\mathrm{log}{x}$
194 192 193 eqtrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}\left(\frac{{x}}{1}\right)}{1}=\mathrm{log}{x}$
195 194 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{1}\right)}{1}=\mathrm{log}{x}$
196 164 188 195 3eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\mathrm{log}{x}$
197 196 oveq2d ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right)\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}$
198 107 197 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)=\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}$
199 198 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)\right|=\left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right|$
200 ere ${⊢}\mathrm{e}\in ℝ$
201 200 a1i ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{e}\in ℝ$
202 1re ${⊢}1\in ℝ$
203 1lt2 ${⊢}1<2$
204 egt2lt3 ${⊢}\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$
205 204 simpli ${⊢}2<\mathrm{e}$
206 202 6 200 lttri ${⊢}\left(1<2\wedge 2<\mathrm{e}\right)\to 1<\mathrm{e}$
207 203 205 206 mp2an ${⊢}1<\mathrm{e}$
208 202 200 207 ltleii ${⊢}1\le \mathrm{e}$
209 201 208 jctir ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\mathrm{e}\in ℝ\wedge 1\le \mathrm{e}\right)$
210 39 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\in ℝ$
211 19 a1i ${⊢}{\phi }\to \frac{1}{2}\in ℝ$
212 1rp ${⊢}1\in {ℝ}^{+}$
213 rphalfcl ${⊢}1\in {ℝ}^{+}\to \frac{1}{2}\in {ℝ}^{+}$
214 212 213 ax-mp ${⊢}\frac{1}{2}\in {ℝ}^{+}$
215 rpge0 ${⊢}\frac{1}{2}\in {ℝ}^{+}\to 0\le \frac{1}{2}$
216 214 215 mp1i ${⊢}{\phi }\to 0\le \frac{1}{2}$
217 20 a1i ${⊢}{\phi }\to \gamma \in ℝ$
218 0re ${⊢}0\in ℝ$
219 emgt0 ${⊢}0<\gamma$
220 218 20 219 ltleii ${⊢}0\le \gamma$
221 220 a1i ${⊢}{\phi }\to 0\le \gamma$
222 22 absge0d ${⊢}{\phi }\to 0\le \left|{L}\right|$
223 217 23 221 222 addge0d ${⊢}{\phi }\to 0\le \gamma +\left|{L}\right|$
224 211 25 216 223 addge0d ${⊢}{\phi }\to 0\le \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|$
225 log1 ${⊢}\mathrm{log}1=0$
226 31 nncnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\in ℂ$
227 226 mulid2d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 1{m}={m}$
228 32 rpred ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\in ℝ$
229 6 a1i ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 2\in ℝ$
230 200 a1i ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{e}\in ℝ$
231 elfzle2 ${⊢}{m}\in \left(1\dots 2\right)\to {m}\le 2$
232 231 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\le 2$
233 6 200 205 ltleii ${⊢}2\le \mathrm{e}$
234 233 a1i ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 2\le \mathrm{e}$
235 228 229 230 232 234 letrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to {m}\le \mathrm{e}$
236 227 235 eqbrtrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 1{m}\le \mathrm{e}$
237 1red ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 1\in ℝ$
238 237 230 32 lemuldivd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \left(1{m}\le \mathrm{e}↔1\le \frac{\mathrm{e}}{{m}}\right)$
239 236 238 mpbid ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 1\le \frac{\mathrm{e}}{{m}}$
240 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge \frac{\mathrm{e}}{{m}}\in {ℝ}^{+}\right)\to \left(1\le \frac{\mathrm{e}}{{m}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\right)$
241 212 34 240 sylancr ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \left(1\le \frac{\mathrm{e}}{{m}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\right)$
242 239 241 mpbid ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{log}1\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)$
243 225 242 eqbrtrrid ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 0\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)$
244 35 32 243 divge0d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}$
245 28 36 244 fsumge0 ${⊢}{\phi }\to 0\le \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
246 27 37 224 245 addge0d ${⊢}{\phi }\to 0\le \left(\frac{1}{2}\right)+\left(\gamma +\left|{L}\right|\right)+\sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
247 246 4 breqtrrdi ${⊢}{\phi }\to 0\le {R}$
248 247 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0\le {R}$
249 210 248 jca ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({R}\in ℝ\wedge 0\le {R}\right)$
250 85 97 mulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\in ℂ$
251 remulcl ${⊢}\left(2\in ℝ\wedge \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\in ℝ\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ$
252 6 15 251 sylancr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)\in ℝ$
253 6 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\in ℝ$
254 0le2 ${⊢}0\le 2$
255 254 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le 2$
256 98 mulid2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}={n}$
257 fznnfl ${⊢}{x}\in ℝ\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
258 123 257 syl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({n}\in \left(1\dots ⌊{x}⌋\right)↔\left({n}\in ℕ\wedge {n}\le {x}\right)\right)$
259 258 simplbda ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\le {x}$
260 256 259 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{n}\le {x}$
261 1red ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in ℝ$
262 57 nnrpd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in {ℝ}^{+}$
263 261 124 262 lemuldivd ${⊢}\left(\left({\phi }\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)$
264 260 263 mpbid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\le \frac{{x}}{{n}}$
265 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge \frac{{x}}{{n}}\in {ℝ}^{+}\right)\to \left(1\le \frac{{x}}{{n}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
266 212 12 265 sylancr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\le \frac{{x}}{{n}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{{x}}{{n}}\right)\right)$
267 264 266 mpbid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}1\le \mathrm{log}\left(\frac{{x}}{{n}}\right)$
268 225 267 eqbrtrrid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \mathrm{log}\left(\frac{{x}}{{n}}\right)$
269 rpregt0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0<{x}\right)$
270 269 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\in ℝ\wedge 0<{x}\right)$
271 divge0 ${⊢}\left(\left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ\wedge 0\le \mathrm{log}\left(\frac{{x}}{{n}}\right)\right)\wedge \left({x}\in ℝ\wedge 0<{x}\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}$
272 13 268 270 271 syl21anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}$
273 253 15 255 272 mulge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)$
274 250 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\in ℝ$
275 274 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\in ℝ$
276 97 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to {T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℂ$
277 276 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℝ$
278 262 rpred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {n}\in ℝ$
279 252 278 remulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}\in ℝ$
280 279 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}\in ℝ$
281 85 97 absmuld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|=\left|\mu \left({n}\right)\right|\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
282 85 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\in ℝ$
283 97 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℝ$
284 97 absge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
285 mule1 ${⊢}{n}\in ℕ\to \left|\mu \left({n}\right)\right|\le 1$
286 57 285 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\le 1$
287 282 261 283 284 286 lemul1ad ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le 1\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
288 283 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℂ$
289 288 mulid2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|=\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
290 287 289 breqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\right|\left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
291 281 290 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\le \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
292 291 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\le \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
294 12 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
295 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \mathrm{e}\le \frac{{x}}{{n}}$
296 1 293 294 295 mulog2sumlem1 ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right)\right|\le 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}\right)$
297 72 96 abssubd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|=\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-{T}\right|$
298 297 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|=\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-{T}\right|$
299 3 oveq2i ${⊢}\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-{T}=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right)$
300 299 fveq2i ${⊢}\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-{T}\right|=\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right)\right|$
301 298 300 syl6eq ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|=\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)-\left(\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right)\right|$
302 2cnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\in ℂ$
303 15 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\in ℂ$
304 302 303 98 mulassd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}=2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
305 rpcnne0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
306 305 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
307 divdiv2 ${⊢}\left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\wedge \left({n}\in ℂ\wedge {n}\ne 0\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}=\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right){n}}{{x}}$
308 63 306 110 307 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}=\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right){n}}{{x}}$
309 div23 ${⊢}\left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ\wedge {n}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right){n}}{{x}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
310 63 98 306 309 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right){n}}{{x}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
311 308 310 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
312 311 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}\right)=2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
313 304 312 eqtr4d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}=2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}\right)$
314 313 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}=2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{\frac{{x}}{{n}}}\right)$
315 296 301 314 3brtr4d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
316 275 277 280 292 315 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \mathrm{e}\le \frac{{x}}{{n}}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\le 2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right){n}$
317 274 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\in ℝ$
318 283 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℝ$
319 39 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {R}\in ℝ$
320 291 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\le \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
321 72 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {T}\in ℂ$
322 321 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}\right|\in ℝ$
323 96 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℂ$
324 323 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℝ$
325 322 324 readdcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}\right|+\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\in ℝ$
326 321 323 abs2dif2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le \left|{T}\right|+\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|$
327 27 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|\in ℝ$
328 37 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)\in ℝ$
329 3 fveq2i ${⊢}\left|{T}\right|=\left|\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|$
330 329 322 eqeltrrid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\in ℝ$
331 65 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\in ℂ$
332 331 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|\in ℝ$
333 70 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\in ℂ$
334 333 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\in ℝ$
335 332 334 readdcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|+\left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\in ℝ$
336 331 333 abstrid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|+\left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|$
337 19 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{1}{2}\in ℝ$
338 25 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma +\left|{L}\right|\in ℝ$
339 13 resqcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ$
340 339 rehalfcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\in ℝ$
341 13 sqge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}$
342 2pos ${⊢}0<2$
343 6 342 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
344 343 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(2\in ℝ\wedge 0<2\right)$
345 divge0 ${⊢}\left(\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ\wedge 0\le {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0\le \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}$
346 339 341 344 345 syl21anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}$
347 340 346 absidd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|=\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}$
348 347 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|=\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}$
349 12 rpred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{n}}\in ℝ$
350 ltle ${⊢}\left(\frac{{x}}{{n}}\in ℝ\wedge \mathrm{e}\in ℝ\right)\to \left(\frac{{x}}{{n}}<\mathrm{e}\to \frac{{x}}{{n}}\le \mathrm{e}\right)$
351 349 200 350 sylancl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\frac{{x}}{{n}}<\mathrm{e}\to \frac{{x}}{{n}}\le \mathrm{e}\right)$
352 351 imp ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{x}}{{n}}\le \mathrm{e}$
353 12 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{x}}{{n}}\in {ℝ}^{+}$
354 logleb ${⊢}\left(\frac{{x}}{{n}}\in {ℝ}^{+}\wedge \mathrm{e}\in {ℝ}^{+}\right)\to \left(\frac{{x}}{{n}}\le \mathrm{e}↔\mathrm{log}\left(\frac{{x}}{{n}}\right)\le \mathrm{log}\mathrm{e}\right)$
355 353 29 354 sylancl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\frac{{x}}{{n}}\le \mathrm{e}↔\mathrm{log}\left(\frac{{x}}{{n}}\right)\le \mathrm{log}\mathrm{e}\right)$
356 352 355 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \mathrm{log}\mathrm{e}$
357 loge ${⊢}\mathrm{log}\mathrm{e}=1$
358 356 357 breqtrdi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1$
359 0le1 ${⊢}0\le 1$
360 359 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le 1$
361 13 261 268 360 le2sqd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1↔{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le {1}^{2}\right)$
362 361 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1↔{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le {1}^{2}\right)$
363 358 362 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le {1}^{2}$
364 sq1 ${⊢}{1}^{2}=1$
365 363 364 breqtrdi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le 1$
366 339 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ$
367 1red ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to 1\in ℝ$
368 343 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(2\in ℝ\wedge 0<2\right)$
369 lediv1 ${⊢}\left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\in ℝ\wedge 1\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le 1↔\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\le \frac{1}{2}\right)$
370 366 367 368 369 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left({\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}\le 1↔\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\le \frac{1}{2}\right)$
371 365 370 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\le \frac{1}{2}$
372 348 371 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|\le \frac{1}{2}$
373 69 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{L}\right|\in ℝ$
374 67 373 readdcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)+\left|{L}\right|\in ℝ$
375 374 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)+\left|{L}\right|\in ℝ$
376 68 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℂ$
377 22 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to {L}\in ℂ$
378 376 377 abs2dif2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\right|+\left|{L}\right|$
379 20 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \gamma \in ℝ$
380 220 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \gamma$
381 379 13 380 268 mulge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)$
382 67 381 absidd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\right|=\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)$
383 382 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\right|=\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)$
384 383 oveq1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\right|+\left|{L}\right|=\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)+\left|{L}\right|$
385 378 384 breqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)+\left|{L}\right|$
386 67 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
387 20 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \in ℝ$
388 377 abscld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{L}\right|\in ℝ$
389 13 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ$
390 387 219 jctir ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\gamma \in ℝ\wedge 0<\gamma \right)$
391 lemul2 ${⊢}\left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\in ℝ\wedge 1\in ℝ\wedge \left(\gamma \in ℝ\wedge 0<\gamma \right)\right)\to \left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1↔\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \gamma \cdot 1\right)$
392 389 367 390 391 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\mathrm{log}\left(\frac{{x}}{{n}}\right)\le 1↔\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \gamma \cdot 1\right)$
393 358 392 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \gamma \cdot 1$
394 20 recni ${⊢}\gamma \in ℂ$
395 394 mulid1i ${⊢}\gamma \cdot 1=\gamma$
396 393 395 breqtrdi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)\le \gamma$
397 386 387 388 396 leadd1dd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)+\left|{L}\right|\le \gamma +\left|{L}\right|$
398 334 375 338 385 397 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \gamma +\left|{L}\right|$
399 332 334 337 338 372 398 le2addd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right|+\left|\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|$
400 330 335 327 336 399 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\left(\frac{{\mathrm{log}\left(\frac{{x}}{{n}}\right)}^{2}}{2}\right)+\gamma \mathrm{log}\left(\frac{{x}}{{n}}\right)-{L}\right|\le \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|$
401 329 400 eqbrtrid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}\right|\le \left(\frac{1}{2}\right)+\gamma +\left|{L}\right|$
402 87 93 sylan2 ${⊢}\left(\left(\left({\phi }\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 \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℝ$
403 86 402 fsumrecl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℝ$
404 403 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\in ℝ$
405 87 91 sylan2 ${⊢}\left(\left(\left({\phi }\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}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ$
406 87 130 sylan2 ${⊢}\left(\left(\left({\phi }\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 ℂ$
407 406 mulid2d ${⊢}\left(\left(\left({\phi }\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 1{m}={m}$
408 fznnfl ${⊢}\frac{{x}}{{n}}\in ℝ\to \left({m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)↔\left({m}\in ℕ\wedge {m}\le \frac{{x}}{{n}}\right)\right)$
409 349 408 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)↔\left({m}\in ℕ\wedge {m}\le \frac{{x}}{{n}}\right)\right)$
410 409 simplbda ${⊢}\left(\left(\left({\phi }\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}\le \frac{{x}}{{n}}$
411 407 410 eqbrtrd ${⊢}\left(\left(\left({\phi }\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 1{m}\le \frac{{x}}{{n}}$
412 1red ${⊢}\left(\left(\left({\phi }\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 1\in ℝ$
413 349 adantr ${⊢}\left(\left(\left({\phi }\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 \frac{{x}}{{n}}\in ℝ$
414 117 rpregt0d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge {m}\in ℕ\right)\to \left({m}\in ℝ\wedge 0<{m}\right)$
415 87 414 sylan2 ${⊢}\left(\left(\left({\phi }\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 \left({m}\in ℝ\wedge 0<{m}\right)$
416 lemuldiv ${⊢}\left(1\in ℝ\wedge \frac{{x}}{{n}}\in ℝ\wedge \left({m}\in ℝ\wedge 0<{m}\right)\right)\to \left(1{m}\le \frac{{x}}{{n}}↔1\le \frac{\frac{{x}}{{n}}}{{m}}\right)$
417 412 413 415 416 syl3anc ${⊢}\left(\left(\left({\phi }\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 \left(1{m}\le \frac{{x}}{{n}}↔1\le \frac{\frac{{x}}{{n}}}{{m}}\right)$
418 411 417 mpbid ${⊢}\left(\left(\left({\phi }\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 1\le \frac{\frac{{x}}{{n}}}{{m}}$
419 87 90 sylan2 ${⊢}\left(\left(\left({\phi }\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 \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}$
420 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}\right)\to \left(1\le \frac{\frac{{x}}{{n}}}{{m}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\right)$
421 212 419 420 sylancr ${⊢}\left(\left(\left({\phi }\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 \left(1\le \frac{\frac{{x}}{{n}}}{{m}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\right)$
422 418 421 mpbid ${⊢}\left(\left(\left({\phi }\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}1\le \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)$
423 225 422 eqbrtrrid ${⊢}\left(\left(\left({\phi }\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 0\le \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)$
424 divge0 ${⊢}\left(\left(\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ\wedge 0\le \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\right)\wedge \left({m}\in ℝ\wedge 0<{m}\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}$
425 405 423 415 424 syl21anc ${⊢}\left(\left(\left({\phi }\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 0\le \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}$
426 86 402 425 fsumge0 ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
427 426 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to 0\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
428 404 427 absidd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|=\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)$
429 fzfid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\in \mathrm{Fin}$
430 349 flcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\to ⌊\frac{{x}}{{n}}⌋\in ℤ$
431 430 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to ⌊\frac{{x}}{{n}}⌋\in ℤ$
432 2z ${⊢}2\in ℤ$
433 432 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to 2\in ℤ$
434 349 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{x}}{{n}}\in ℝ$
435 200 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \mathrm{e}\in ℝ$
436 3re ${⊢}3\in ℝ$
437 436 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to 3\in ℝ$
438 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{x}}{{n}}<\mathrm{e}$
439 204 simpri ${⊢}\mathrm{e}<3$
440 439 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \mathrm{e}<3$
441 434 435 437 438 440 lttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \frac{{x}}{{n}}<3$
442 3z ${⊢}3\in ℤ$
443 fllt ${⊢}\left(\frac{{x}}{{n}}\in ℝ\wedge 3\in ℤ\right)\to \left(\frac{{x}}{{n}}<3↔⌊\frac{{x}}{{n}}⌋<3\right)$
444 434 442 443 sylancl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(\frac{{x}}{{n}}<3↔⌊\frac{{x}}{{n}}⌋<3\right)$
445 441 444 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to ⌊\frac{{x}}{{n}}⌋<3$
446 df-3 ${⊢}3=2+1$
447 445 446 breqtrdi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to ⌊\frac{{x}}{{n}}⌋<2+1$
448 zleltp1 ${⊢}\left(⌊\frac{{x}}{{n}}⌋\in ℤ\wedge 2\in ℤ\right)\to \left(⌊\frac{{x}}{{n}}⌋\le 2↔⌊\frac{{x}}{{n}}⌋<2+1\right)$
449 431 432 448 sylancl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(⌊\frac{{x}}{{n}}⌋\le 2↔⌊\frac{{x}}{{n}}⌋<2+1\right)$
450 447 449 mpbird ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to ⌊\frac{{x}}{{n}}⌋\le 2$
451 eluz2 ${⊢}2\in {ℤ}_{\ge ⌊\frac{{x}}{{n}}⌋}↔\left(⌊\frac{{x}}{{n}}⌋\in ℤ\wedge 2\in ℤ\wedge ⌊\frac{{x}}{{n}}⌋\le 2\right)$
452 431 433 450 451 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to 2\in {ℤ}_{\ge ⌊\frac{{x}}{{n}}⌋}$
453 fzss2 ${⊢}2\in {ℤ}_{\ge ⌊\frac{{x}}{{n}}⌋}\to \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\subseteq \left(1\dots 2\right)$
454 452 453 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\subseteq \left(1\dots 2\right)$
455 454 sselda ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to {m}\in \left(1\dots 2\right)$
456 36 ad5ant15 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\in ℝ$
457 455 456 syldan ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\in ℝ$
458 429 457 fsumrecl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)\in ℝ$
459 93 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in ℕ\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℝ$
460 87 459 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\in ℝ$
461 352 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{{x}}{{n}}\le \mathrm{e}$
462 434 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{{x}}{{n}}\in ℝ$
463 200 a1i ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{e}\in ℝ$
464 32 rpregt0d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots 2\right)\right)\to \left({m}\in ℝ\wedge 0<{m}\right)$
465 464 ad5ant15 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \left({m}\in ℝ\wedge 0<{m}\right)$
466 lediv1 ${⊢}\left(\frac{{x}}{{n}}\in ℝ\wedge \mathrm{e}\in ℝ\wedge \left({m}\in ℝ\wedge 0<{m}\right)\right)\to \left(\frac{{x}}{{n}}\le \mathrm{e}↔\frac{\frac{{x}}{{n}}}{{m}}\le \frac{\mathrm{e}}{{m}}\right)$
467 462 463 465 466 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \left(\frac{{x}}{{n}}\le \mathrm{e}↔\frac{\frac{{x}}{{n}}}{{m}}\le \frac{\mathrm{e}}{{m}}\right)$
468 461 467 mpbid ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\frac{{x}}{{n}}}{{m}}\le \frac{\mathrm{e}}{{m}}$
469 90 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in ℕ\right)\to \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}$
470 30 469 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\frac{{x}}{{n}}}{{m}}\in {ℝ}^{+}$
471 34 ad5ant15 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\mathrm{e}}{{m}}\in {ℝ}^{+}$
472 470 471 logled ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \left(\frac{\frac{{x}}{{n}}}{{m}}\le \frac{\mathrm{e}}{{m}}↔\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\right)$
473 468 472 mpbid ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)$
474 91 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in ℕ\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ$
475 30 474 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ$
476 35 ad5ant15 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\in ℝ$
477 lediv1 ${⊢}\left(\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\in ℝ\wedge \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)\in ℝ\wedge \left({m}\in ℝ\wedge 0<{m}\right)\right)\to \left(\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)↔\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
478 475 476 465 477 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \left(\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)\le \mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)↔\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
479 473 478 mpbid ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}$
480 455 479 syldan ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots ⌊\frac{{x}}{{n}}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}$
481 429 460 457 480 fsumle ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\le \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
482 fzfid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left(1\dots 2\right)\in \mathrm{Fin}$
483 244 ad5ant15 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\wedge {m}\in \left(1\dots 2\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}$
484 482 456 483 454 fsumless ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)\le \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
485 404 458 328 481 484 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\le \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
486 428 485 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le \sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
487 322 324 327 328 401 486 le2addd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}\right|+\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le \left(\frac{1}{2}\right)+\left(\gamma +\left|{L}\right|\right)+\sum _{{m}=1}^{2}\left(\frac{\mathrm{log}\left(\frac{\mathrm{e}}{{m}}\right)}{{m}}\right)$
488 487 4 breqtrrdi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}\right|+\left|\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le {R}$
489 318 325 319 326 488 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|{T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right|\le {R}$
490 317 318 319 320 489 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {n}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{n}}<\mathrm{e}\right)\to \left|\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)\right|\le {R}$
491 8 209 249 250 252 273 316 490 fsumharmonic ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)\right|\le \sum _{{n}=1}^{⌊{x}⌋}2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\left(\mathrm{log}\mathrm{e}+1\right)$
492 2cnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\in ℂ$
493 7 492 303 fsummulc2 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)=\sum _{{n}=1}^{⌊{x}⌋}2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)$
494 df-2 ${⊢}2=1+1$
495 357 oveq1i ${⊢}\mathrm{log}\mathrm{e}+1=1+1$
496 494 495 eqtr4i ${⊢}2=\mathrm{log}\mathrm{e}+1$
497 496 a1i ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2=\mathrm{log}\mathrm{e}+1$
498 497 oveq2d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\cdot 2={R}\left(\mathrm{log}\mathrm{e}+1\right)$
499 493 498 oveq12d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2=\sum _{{n}=1}^{⌊{x}⌋}2\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\left(\mathrm{log}\mathrm{e}+1\right)$
500 491 499 breqtrrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)\right|\le 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2$
501 500 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)\left({T}-\sum _{{m}=1}^{⌊\frac{{x}}{{n}}⌋}\left(\frac{\mathrm{log}\left(\frac{\frac{{x}}{{n}}}{{m}}\right)}{{m}}\right)\right)}{{n}}\right)\right|\le 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2$
502 199 501 eqbrtrrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right|\le 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2$
503 56 leabsd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\le \left|2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right|$
504 503 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to 2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\le \left|2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right|$
505 80 81 84 502 504 letrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right|\le \left|2\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{n}}\right)}{{x}}\right)+{R}\cdot 2\right|$
506 5 55 56 78 505 o1le ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}=1}^{⌊{x}⌋}\left(\frac{\mu \left({n}\right)}{{n}}\right){T}-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$