# Metamath Proof Explorer

## Theorem dchrvmasumlem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z ${⊢}{Z}=ℤ/{N}ℤ$
rpvmasum.l ${⊢}{L}=\mathrm{ℤRHom}\left({Z}\right)$
rpvmasum.a ${⊢}{\phi }\to {N}\in ℕ$
rpvmasum.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
rpvmasum.d ${⊢}{D}={\mathrm{Base}}_{{G}}$
rpvmasum.1
dchrisum.b ${⊢}{\phi }\to {X}\in {D}$
dchrisum.n1
dchrvmasum.f ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to {F}\in ℂ$
dchrvmasum.g ${⊢}{m}=\frac{{x}}{{d}}\to {F}={K}$
dchrvmasum.c ${⊢}{\phi }\to {C}\in \left[0,\mathrm{+\infty }\right)$
dchrvmasum.t ${⊢}{\phi }\to {T}\in ℂ$
dchrvmasum.1 ${⊢}\left({\phi }\wedge {m}\in \left[3,\mathrm{+\infty }\right)\right)\to \left|{F}-{T}\right|\le {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
dchrvmasum.r ${⊢}{\phi }\to {R}\in ℝ$
dchrvmasum.2 ${⊢}{\phi }\to \forall {m}\in \left[1,3\right)\phantom{\rule{.4em}{0ex}}\left|{F}-{T}\right|\le {R}$
Assertion dchrvmasumlem2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 rpvmasum.z ${⊢}{Z}=ℤ/{N}ℤ$
2 rpvmasum.l ${⊢}{L}=\mathrm{ℤRHom}\left({Z}\right)$
3 rpvmasum.a ${⊢}{\phi }\to {N}\in ℕ$
4 rpvmasum.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
5 rpvmasum.d ${⊢}{D}={\mathrm{Base}}_{{G}}$
6 rpvmasum.1
7 dchrisum.b ${⊢}{\phi }\to {X}\in {D}$
8 dchrisum.n1
9 dchrvmasum.f ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to {F}\in ℂ$
10 dchrvmasum.g ${⊢}{m}=\frac{{x}}{{d}}\to {F}={K}$
11 dchrvmasum.c ${⊢}{\phi }\to {C}\in \left[0,\mathrm{+\infty }\right)$
12 dchrvmasum.t ${⊢}{\phi }\to {T}\in ℂ$
13 dchrvmasum.1 ${⊢}\left({\phi }\wedge {m}\in \left[3,\mathrm{+\infty }\right)\right)\to \left|{F}-{T}\right|\le {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
14 dchrvmasum.r ${⊢}{\phi }\to {R}\in ℝ$
15 dchrvmasum.2 ${⊢}{\phi }\to \forall {m}\in \left[1,3\right)\phantom{\rule{.4em}{0ex}}\left|{F}-{T}\right|\le {R}$
16 1red ${⊢}{\phi }\to 1\in ℝ$
17 elrege0 ${⊢}{C}\in \left[0,\mathrm{+\infty }\right)↔\left({C}\in ℝ\wedge 0\le {C}\right)$
18 11 17 sylib ${⊢}{\phi }\to \left({C}\in ℝ\wedge 0\le {C}\right)$
19 18 simpld ${⊢}{\phi }\to {C}\in ℝ$
20 19 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\in ℝ$
21 fzfid ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
22 simpr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
23 elfznn ${⊢}{d}\in \left(1\dots ⌊{x}⌋\right)\to {d}\in ℕ$
24 23 nnrpd ${⊢}{d}\in \left(1\dots ⌊{x}⌋\right)\to {d}\in {ℝ}^{+}$
25 rpdivcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\to \frac{{x}}{{d}}\in {ℝ}^{+}$
26 22 24 25 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{d}}\in {ℝ}^{+}$
27 26 relogcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{d}}\right)\in ℝ$
28 22 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in {ℝ}^{+}$
29 27 28 rerpdivcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\in ℝ$
30 21 29 fsumrecl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\in ℝ$
31 20 30 remulcld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\in ℝ$
32 3nn ${⊢}3\in ℕ$
33 nnrp ${⊢}3\in ℕ\to 3\in {ℝ}^{+}$
34 relogcl ${⊢}3\in {ℝ}^{+}\to \mathrm{log}3\in ℝ$
35 32 33 34 mp2b ${⊢}\mathrm{log}3\in ℝ$
36 1re ${⊢}1\in ℝ$
37 35 36 readdcli ${⊢}\mathrm{log}3+1\in ℝ$
38 remulcl ${⊢}\left({R}\in ℝ\wedge \mathrm{log}3+1\in ℝ\right)\to {R}\left(\mathrm{log}3+1\right)\in ℝ$
39 14 37 38 sylancl ${⊢}{\phi }\to {R}\left(\mathrm{log}3+1\right)\in ℝ$
40 39 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\left(\mathrm{log}3+1\right)\in ℝ$
41 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
42 19 recnd ${⊢}{\phi }\to {C}\in ℂ$
43 o1const ${⊢}\left({ℝ}^{+}\subseteq ℝ\wedge {C}\in ℂ\right)\to \left({x}\in {ℝ}^{+}⟼{C}\right)\in 𝑂\left(1\right)$
44 41 42 43 sylancr ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼{C}\right)\in 𝑂\left(1\right)$
45 logfacrlim2
46 rlimo1
47 45 46 mp1i ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\right)\in 𝑂\left(1\right)$
48 20 30 44 47 o1mul2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\right)\in 𝑂\left(1\right)$
49 39 recnd ${⊢}{\phi }\to {R}\left(\mathrm{log}3+1\right)\in ℂ$
50 o1const ${⊢}\left({ℝ}^{+}\subseteq ℝ\wedge {R}\left(\mathrm{log}3+1\right)\in ℂ\right)\to \left({x}\in {ℝ}^{+}⟼{R}\left(\mathrm{log}3+1\right)\right)\in 𝑂\left(1\right)$
51 41 49 50 sylancr ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼{R}\left(\mathrm{log}3+1\right)\right)\in 𝑂\left(1\right)$
52 31 40 48 51 o1add2 ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\right)\in 𝑂\left(1\right)$
53 31 40 readdcld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\in ℝ$
54 10 eleq1d ${⊢}{m}=\frac{{x}}{{d}}\to \left({F}\in ℂ↔{K}\in ℂ\right)$
55 9 ralrimiva ${⊢}{\phi }\to \forall {m}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{F}\in ℂ$
56 55 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \forall {m}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{F}\in ℂ$
57 54 56 26 rspcdva ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {K}\in ℂ$
58 12 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {T}\in ℂ$
59 57 58 subcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {K}-{T}\in ℂ$
60 59 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{K}-{T}\right|\in ℝ$
61 23 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {d}\in ℕ$
62 60 61 nndivred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\left|{K}-{T}\right|}{{d}}\in ℝ$
63 21 62 fsumrecl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\in ℝ$
64 63 recnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\in ℂ$
65 61 nnrpd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {d}\in {ℝ}^{+}$
66 59 absge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \left|{K}-{T}\right|$
67 60 65 66 divge0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \frac{\left|{K}-{T}\right|}{{d}}$
68 21 62 67 fsumge0 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0\le \sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)$
69 63 68 absidd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|=\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)$
70 69 63 eqeltrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|\in ℝ$
71 53 recnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\in ℂ$
72 71 abscld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\right|\in ℝ$
73 3re ${⊢}3\in ℝ$
74 73 a1i ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 3\in ℝ$
75 1le3 ${⊢}1\le 3$
76 74 75 jctir ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(3\in ℝ\wedge 1\le 3\right)$
77 14 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\in ℝ$
78 36 rexri ${⊢}1\in {ℝ}^{*}$
79 73 rexri ${⊢}3\in {ℝ}^{*}$
80 1lt3 ${⊢}1<3$
81 lbico1 ${⊢}\left(1\in {ℝ}^{*}\wedge 3\in {ℝ}^{*}\wedge 1<3\right)\to 1\in \left[1,3\right)$
82 78 79 80 81 mp3an ${⊢}1\in \left[1,3\right)$
83 0red ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to 0\in ℝ$
84 elico2 ${⊢}\left(1\in ℝ\wedge 3\in {ℝ}^{*}\right)\to \left({m}\in \left[1,3\right)↔\left({m}\in ℝ\wedge 1\le {m}\wedge {m}<3\right)\right)$
85 36 79 84 mp2an ${⊢}{m}\in \left[1,3\right)↔\left({m}\in ℝ\wedge 1\le {m}\wedge {m}<3\right)$
86 85 simp1bi ${⊢}{m}\in \left[1,3\right)\to {m}\in ℝ$
87 0red ${⊢}{m}\in \left[1,3\right)\to 0\in ℝ$
88 1red ${⊢}{m}\in \left[1,3\right)\to 1\in ℝ$
89 0lt1 ${⊢}0<1$
90 89 a1i ${⊢}{m}\in \left[1,3\right)\to 0<1$
91 85 simp2bi ${⊢}{m}\in \left[1,3\right)\to 1\le {m}$
92 87 88 86 90 91 ltletrd ${⊢}{m}\in \left[1,3\right)\to 0<{m}$
93 86 92 elrpd ${⊢}{m}\in \left[1,3\right)\to {m}\in {ℝ}^{+}$
94 12 adantr ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to {T}\in ℂ$
95 9 94 subcld ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to {F}-{T}\in ℂ$
96 95 abscld ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to \left|{F}-{T}\right|\in ℝ$
97 93 96 sylan2 ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to \left|{F}-{T}\right|\in ℝ$
98 14 adantr ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to {R}\in ℝ$
99 95 absge0d ${⊢}\left({\phi }\wedge {m}\in {ℝ}^{+}\right)\to 0\le \left|{F}-{T}\right|$
100 93 99 sylan2 ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to 0\le \left|{F}-{T}\right|$
101 15 r19.21bi ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to \left|{F}-{T}\right|\le {R}$
102 83 97 98 100 101 letrd ${⊢}\left({\phi }\wedge {m}\in \left[1,3\right)\right)\to 0\le {R}$
103 102 ralrimiva ${⊢}{\phi }\to \forall {m}\in \left[1,3\right)\phantom{\rule{.4em}{0ex}}0\le {R}$
104 biidd ${⊢}{m}=1\to \left(0\le {R}↔0\le {R}\right)$
105 104 rspcv ${⊢}1\in \left[1,3\right)\to \left(\forall {m}\in \left[1,3\right)\phantom{\rule{.4em}{0ex}}0\le {R}\to 0\le {R}\right)$
106 82 103 105 mpsyl ${⊢}{\phi }\to 0\le {R}$
107 106 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0\le {R}$
108 77 107 jca ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({R}\in ℝ\wedge 0\le {R}\right)$
109 60 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|{K}-{T}\right|\in ℂ$
110 19 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\in ℝ$
111 110 29 remulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\in ℝ$
112 18 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({C}\in ℝ\wedge 0\le {C}\right)$
113 log1 ${⊢}\mathrm{log}1=0$
114 61 nncnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {d}\in ℂ$
115 114 mulid2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{d}={d}$
116 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
117 116 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
118 fznnfl ${⊢}{x}\in ℝ\to \left({d}\in \left(1\dots ⌊{x}⌋\right)↔\left({d}\in ℕ\wedge {d}\le {x}\right)\right)$
119 117 118 syl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({d}\in \left(1\dots ⌊{x}⌋\right)↔\left({d}\in ℕ\wedge {d}\le {x}\right)\right)$
120 119 simplbda ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {d}\le {x}$
121 115 120 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1{d}\le {x}$
122 1red ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in ℝ$
123 116 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {x}\in ℝ$
124 122 123 65 lemuldivd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1{d}\le {x}↔1\le \frac{{x}}{{d}}\right)$
125 121 124 mpbid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\le \frac{{x}}{{d}}$
126 1rp ${⊢}1\in {ℝ}^{+}$
127 126 a1i ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 1\in {ℝ}^{+}$
128 127 26 logled ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left(1\le \frac{{x}}{{d}}↔\mathrm{log}1\le \mathrm{log}\left(\frac{{x}}{{d}}\right)\right)$
129 125 128 mpbid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}1\le \mathrm{log}\left(\frac{{x}}{{d}}\right)$
130 113 129 eqbrtrrid ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \mathrm{log}\left(\frac{{x}}{{d}}\right)$
131 rpregt0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0<{x}\right)$
132 131 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\in ℝ\wedge 0<{x}\right)$
133 divge0 ${⊢}\left(\left(\mathrm{log}\left(\frac{{x}}{{d}}\right)\in ℝ\wedge 0\le \mathrm{log}\left(\frac{{x}}{{d}}\right)\right)\wedge \left({x}\in ℝ\wedge 0<{x}\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}$
134 27 130 132 133 syl21anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}$
135 mulge0 ${⊢}\left(\left({C}\in ℝ\wedge 0\le {C}\right)\wedge \left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\in ℝ\wedge 0\le \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)\right)\to 0\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)$
136 112 29 134 135 syl12anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to 0\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)$
137 absidm ${⊢}{K}-{T}\in ℂ\to \left|\left|{K}-{T}\right|\right|=\left|{K}-{T}\right|$
138 59 137 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left|\left|{K}-{T}\right|\right|=\left|{K}-{T}\right|$
139 138 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \left|\left|{K}-{T}\right|\right|=\left|{K}-{T}\right|$
140 10 fvoveq1d ${⊢}{m}=\frac{{x}}{{d}}\to \left|{F}-{T}\right|=\left|{K}-{T}\right|$
141 fveq2 ${⊢}{m}=\frac{{x}}{{d}}\to \mathrm{log}{m}=\mathrm{log}\left(\frac{{x}}{{d}}\right)$
142 id ${⊢}{m}=\frac{{x}}{{d}}\to {m}=\frac{{x}}{{d}}$
143 141 142 oveq12d ${⊢}{m}=\frac{{x}}{{d}}\to \frac{\mathrm{log}{m}}{{m}}=\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}$
144 143 oveq2d ${⊢}{m}=\frac{{x}}{{d}}\to {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)={C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)$
145 140 144 breq12d ${⊢}{m}=\frac{{x}}{{d}}\to \left(\left|{F}-{T}\right|\le {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)↔\left|{K}-{T}\right|\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)\right)$
146 13 ralrimiva ${⊢}{\phi }\to \forall {m}\in \left[3,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left|{F}-{T}\right|\le {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
147 146 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \forall {m}\in \left[3,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left|{F}-{T}\right|\le {C}\left(\frac{\mathrm{log}{m}}{{m}}\right)$
148 nndivre ${⊢}\left({x}\in ℝ\wedge {d}\in ℕ\right)\to \frac{{x}}{{d}}\in ℝ$
149 117 23 148 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{{x}}{{d}}\in ℝ$
150 149 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \frac{{x}}{{d}}\in ℝ$
151 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to 3\le \frac{{x}}{{d}}$
152 elicopnf ${⊢}3\in ℝ\to \left(\frac{{x}}{{d}}\in \left[3,\mathrm{+\infty }\right)↔\left(\frac{{x}}{{d}}\in ℝ\wedge 3\le \frac{{x}}{{d}}\right)\right)$
153 73 152 ax-mp ${⊢}\frac{{x}}{{d}}\in \left[3,\mathrm{+\infty }\right)↔\left(\frac{{x}}{{d}}\in ℝ\wedge 3\le \frac{{x}}{{d}}\right)$
154 150 151 153 sylanbrc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \frac{{x}}{{d}}\in \left[3,\mathrm{+\infty }\right)$
155 145 147 154 rspcdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \left|{K}-{T}\right|\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)$
156 27 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \mathrm{log}\left(\frac{{x}}{{d}}\right)\in ℂ$
157 rpcnne0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
158 157 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
159 65 rpcnne0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \left({d}\in ℂ\wedge {d}\ne 0\right)$
160 divdiv2 ${⊢}\left(\mathrm{log}\left(\frac{{x}}{{d}}\right)\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\wedge \left({d}\in ℂ\wedge {d}\ne 0\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}=\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right){d}}{{x}}$
161 156 158 159 160 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}=\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right){d}}{{x}}$
162 div23 ${⊢}\left(\mathrm{log}\left(\frac{{x}}{{d}}\right)\in ℂ\wedge {d}\in ℂ\wedge \left({x}\in ℂ\wedge {x}\ne 0\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right){d}}{{x}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
163 156 114 158 162 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right){d}}{{x}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
164 161 163 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}=\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
165 164 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)={C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
166 42 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\in ℂ$
167 29 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to \frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\in ℂ$
168 166 167 114 mulassd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}={C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
169 165 168 eqtr4d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\to {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)={C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
170 169 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{\frac{{x}}{{d}}}\right)={C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
171 155 170 breqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \left|{K}-{T}\right|\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
172 139 171 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge 3\le \frac{{x}}{{d}}\right)\to \left|\left|{K}-{T}\right|\right|\le {C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right){d}$
173 138 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \left|\left|{K}-{T}\right|\right|=\left|{K}-{T}\right|$
174 140 breq1d ${⊢}{m}=\frac{{x}}{{d}}\to \left(\left|{F}-{T}\right|\le {R}↔\left|{K}-{T}\right|\le {R}\right)$
175 15 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \forall {m}\in \left[1,3\right)\phantom{\rule{.4em}{0ex}}\left|{F}-{T}\right|\le {R}$
176 149 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \frac{{x}}{{d}}\in ℝ$
177 125 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to 1\le \frac{{x}}{{d}}$
178 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \frac{{x}}{{d}}<3$
179 elico2 ${⊢}\left(1\in ℝ\wedge 3\in {ℝ}^{*}\right)\to \left(\frac{{x}}{{d}}\in \left[1,3\right)↔\left(\frac{{x}}{{d}}\in ℝ\wedge 1\le \frac{{x}}{{d}}\wedge \frac{{x}}{{d}}<3\right)\right)$
180 36 79 179 mp2an ${⊢}\frac{{x}}{{d}}\in \left[1,3\right)↔\left(\frac{{x}}{{d}}\in ℝ\wedge 1\le \frac{{x}}{{d}}\wedge \frac{{x}}{{d}}<3\right)$
181 176 177 178 180 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \frac{{x}}{{d}}\in \left[1,3\right)$
182 174 175 181 rspcdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \left|{K}-{T}\right|\le {R}$
183 173 182 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {d}\in \left(1\dots ⌊{x}⌋\right)\right)\wedge \frac{{x}}{{d}}<3\right)\to \left|\left|{K}-{T}\right|\right|\le {R}$
184 22 76 108 109 111 136 172 183 fsumharmonic ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|\le \sum _{{d}=1}^{⌊{x}⌋}{C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)$
185 42 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\in ℂ$
186 21 185 167 fsummulc2 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)=\sum _{{d}=1}^{⌊{x}⌋}{C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)$
187 186 oveq1d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)=\sum _{{d}=1}^{⌊{x}⌋}{C}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)$
188 184 187 breqtrrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|\le {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)$
189 53 leabsd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\le \left|{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\right|$
190 70 53 72 188 189 letrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|\le \left|{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\right|$
191 190 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \left|\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right|\le \left|{C}\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\mathrm{log}\left(\frac{{x}}{{d}}\right)}{{x}}\right)+{R}\left(\mathrm{log}3+1\right)\right|$
192 16 52 53 64 191 o1le ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\sum _{{d}=1}^{⌊{x}⌋}\left(\frac{\left|{K}-{T}\right|}{{d}}\right)\right)\in 𝑂\left(1\right)$