Metamath Proof Explorer


Theorem mulog2sumlem2

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

Ref Expression
Hypotheses logdivsum.1 F = y + i = 1 y log i i log y 2 2
mulog2sumlem.1 φ F L
mulog2sumlem2.t T = log x n 2 2 + γ log x n - L
mulog2sumlem2.r R = 1 2 + γ + L + m = 1 2 log e m m
Assertion mulog2sumlem2 φ x + n = 1 x μ n n T log x 𝑂1

Proof

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