Metamath Proof Explorer


Theorem log2sumbnd

Description: Bound on the difference between sum_ n <_ A , log ^ 2 ( n ) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion log2sumbnd A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A log A 2 + 2

Proof

Step Hyp Ref Expression
1 fzfid A + 1 A 1 A Fin
2 elfznn n 1 A n
3 2 adantl A + 1 A n 1 A n
4 3 nnrpd A + 1 A n 1 A n +
5 4 relogcld A + 1 A n 1 A log n
6 5 resqcld A + 1 A n 1 A log n 2
7 1 6 fsumrecl A + 1 A n = 1 A log n 2
8 rpre A + A
9 8 adantr A + 1 A A
10 relogcl A + log A
11 10 adantr A + 1 A log A
12 11 resqcld A + 1 A log A 2
13 2re 2
14 remulcl 2 log A 2 log A
15 13 11 14 sylancr A + 1 A 2 log A
16 resubcl 2 2 log A 2 2 log A
17 13 15 16 sylancr A + 1 A 2 2 log A
18 12 17 readdcld A + 1 A log A 2 + 2 - 2 log A
19 9 18 remulcld A + 1 A A log A 2 + 2 - 2 log A
20 7 19 resubcld A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A
21 20 recnd A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A
22 21 abscld A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A
23 resubcl n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 A log A 2 + 2 - 2 log A 2
24 22 13 23 sylancl A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A 2
25 2cn 2
26 25 negcli 2
27 subcl n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
28 21 26 27 sylancl A + 1 A n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
29 28 abscld A + 1 A n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
30 25 absnegi 2 = 2
31 0le2 0 2
32 absid 2 0 2 2 = 2
33 13 31 32 mp2an 2 = 2
34 30 33 eqtri 2 = 2
35 34 oveq2i n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 = n = 1 A log n 2 A log A 2 + 2 - 2 log A 2
36 abs2dif n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
37 21 26 36 sylancl A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
38 35 37 eqbrtrrid A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
39 fveq2 x = A x = A
40 39 oveq2d x = A 1 x = 1 A
41 40 sumeq1d x = A n = 1 x log n 2 = n = 1 A log n 2
42 id x = A x = A
43 fveq2 x = A log x = log A
44 43 oveq1d x = A log x 2 = log A 2
45 43 oveq2d x = A 2 log x = 2 log A
46 45 oveq2d x = A 2 2 log x = 2 2 log A
47 44 46 oveq12d x = A log x 2 + 2 - 2 log x = log A 2 + 2 - 2 log A
48 42 47 oveq12d x = A x log x 2 + 2 - 2 log x = A log A 2 + 2 - 2 log A
49 41 48 oveq12d x = A n = 1 x log n 2 x log x 2 + 2 - 2 log x = n = 1 A log n 2 A log A 2 + 2 - 2 log A
50 eqid x + n = 1 x log n 2 x log x 2 + 2 - 2 log x = x + n = 1 x log n 2 x log x 2 + 2 - 2 log x
51 ovex n = 1 x log n 2 x log x 2 + 2 - 2 log x V
52 49 50 51 fvmpt3i A + x + n = 1 x log n 2 x log x 2 + 2 - 2 log x A = n = 1 A log n 2 A log A 2 + 2 - 2 log A
53 52 adantr A + 1 A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x A = n = 1 A log n 2 A log A 2 + 2 - 2 log A
54 1rp 1 +
55 fveq2 x = 1 x = 1
56 1z 1
57 flid 1 1 = 1
58 56 57 ax-mp 1 = 1
59 55 58 syl6eq x = 1 x = 1
60 59 oveq2d x = 1 1 x = 1 1
61 60 sumeq1d x = 1 n = 1 x log n 2 = n = 1 1 log n 2
62 0cn 0
63 fveq2 n = 1 log n = log 1
64 log1 log 1 = 0
65 63 64 syl6eq n = 1 log n = 0
66 65 sq0id n = 1 log n 2 = 0
67 66 fsum1 1 0 n = 1 1 log n 2 = 0
68 56 62 67 mp2an n = 1 1 log n 2 = 0
69 61 68 syl6eq x = 1 n = 1 x log n 2 = 0
70 id x = 1 x = 1
71 fveq2 x = 1 log x = log 1
72 71 64 syl6eq x = 1 log x = 0
73 72 sq0id x = 1 log x 2 = 0
74 72 oveq2d x = 1 2 log x = 2 0
75 2t0e0 2 0 = 0
76 74 75 syl6eq x = 1 2 log x = 0
77 76 oveq2d x = 1 2 2 log x = 2 0
78 25 subid1i 2 0 = 2
79 77 78 syl6eq x = 1 2 2 log x = 2
80 73 79 oveq12d x = 1 log x 2 + 2 - 2 log x = 0 + 2
81 25 addid2i 0 + 2 = 2
82 80 81 syl6eq x = 1 log x 2 + 2 - 2 log x = 2
83 70 82 oveq12d x = 1 x log x 2 + 2 - 2 log x = 1 2
84 25 mulid2i 1 2 = 2
85 83 84 syl6eq x = 1 x log x 2 + 2 - 2 log x = 2
86 69 85 oveq12d x = 1 n = 1 x log n 2 x log x 2 + 2 - 2 log x = 0 2
87 df-neg 2 = 0 2
88 86 87 syl6eqr x = 1 n = 1 x log n 2 x log x 2 + 2 - 2 log x = 2
89 88 50 51 fvmpt3i 1 + x + n = 1 x log n 2 x log x 2 + 2 - 2 log x 1 = 2
90 54 89 mp1i A + 1 A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x 1 = 2
91 53 90 oveq12d A + 1 A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x 1 = n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
92 91 fveq2d A + 1 A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x 1 = n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2
93 ioorp 0 +∞ = +
94 93 eqcomi + = 0 +∞
95 nnuz = 1
96 56 a1i A + 1 A 1
97 1red A + 1 A 1
98 pnfxr +∞ *
99 98 a1i A + 1 A +∞ *
100 1re 1
101 1nn0 1 0
102 100 101 nn0addge1i 1 1 + 1
103 102 a1i A + 1 A 1 1 + 1
104 0red A + 1 A 0
105 rpre x + x
106 105 adantl A + 1 A x + x
107 simpr A + 1 A x + x +
108 107 relogcld A + 1 A x + log x
109 108 resqcld A + 1 A x + log x 2
110 remulcl 2 log x 2 log x
111 13 108 110 sylancr A + 1 A x + 2 log x
112 resubcl 2 2 log x 2 2 log x
113 13 111 112 sylancr A + 1 A x + 2 2 log x
114 109 113 readdcld A + 1 A x + log x 2 + 2 - 2 log x
115 106 114 remulcld A + 1 A x + x log x 2 + 2 - 2 log x
116 nnrp x x +
117 116 109 sylan2 A + 1 A x log x 2
118 reelprrecn
119 118 a1i A + 1 A
120 106 recnd A + 1 A x + x
121 1red A + 1 A x + 1
122 recn x x
123 122 adantl A + 1 A x x
124 1red A + 1 A x 1
125 119 dvmptid A + 1 A dx x d x = x 1
126 rpssre +
127 126 a1i A + 1 A +
128 eqid TopOpen fld = TopOpen fld
129 128 tgioo2 topGen ran . = TopOpen fld 𝑡
130 iooretop 0 +∞ topGen ran .
131 93 130 eqeltrri + topGen ran .
132 131 a1i A + 1 A + topGen ran .
133 119 123 124 125 127 129 128 132 dvmptres A + 1 A dx + x d x = x + 1
134 114 recnd A + 1 A x + log x 2 + 2 - 2 log x
135 resubcl 2 log x 2 2 log x 2
136 111 13 135 sylancl A + 1 A x + 2 log x 2
137 136 107 rerpdivcld A + 1 A x + 2 log x 2 x
138 109 recnd A + 1 A x + log x 2
139 111 recnd A + 1 A x + 2 log x
140 107 rpreccld A + 1 A x + 1 x +
141 140 rpcnd A + 1 A x + 1 x
142 139 141 mulcld A + 1 A x + 2 log x 1 x
143 cnelprrecn
144 143 a1i A + 1 A
145 108 recnd A + 1 A x + log x
146 sqcl y y 2
147 146 adantl A + 1 A y y 2
148 simpr A + 1 A y y
149 mulcl 2 y 2 y
150 25 148 149 sylancr A + 1 A y 2 y
151 dvrelog D log + = x + 1 x
152 relogf1o log + : + 1-1 onto
153 f1of log + : + 1-1 onto log + : +
154 152 153 mp1i A + 1 A log + : +
155 154 feqmptd A + 1 A log + = x + log + x
156 fvres x + log + x = log x
157 156 mpteq2ia x + log + x = x + log x
158 155 157 syl6eq A + 1 A log + = x + log x
159 158 oveq2d A + 1 A D log + = dx + log x d x
160 151 159 syl5reqr A + 1 A dx + log x d x = x + 1 x
161 2nn 2
162 dvexp 2 dy y 2 d y = y 2 y 2 1
163 161 162 mp1i A + 1 A dy y 2 d y = y 2 y 2 1
164 2m1e1 2 1 = 1
165 164 oveq2i y 2 1 = y 1
166 exp1 y y 1 = y
167 165 166 syl5eq y y 2 1 = y
168 167 oveq2d y 2 y 2 1 = 2 y
169 168 mpteq2ia y 2 y 2 1 = y 2 y
170 163 169 syl6eq A + 1 A dy y 2 d y = y 2 y
171 oveq1 y = log x y 2 = log x 2
172 oveq2 y = log x 2 y = 2 log x
173 119 144 145 140 147 150 160 170 171 172 dvmptco A + 1 A dx + log x 2 d x = x + 2 log x 1 x
174 113 recnd A + 1 A x + 2 2 log x
175 ovexd A + 1 A x + 0 2 1 x V
176 2cnd A + 1 A x + 2
177 0red A + 1 A x + 0
178 2cnd A + 1 A x 2
179 0red A + 1 A x 0
180 2cnd A + 1 A 2
181 119 180 dvmptc A + 1 A dx 2 d x = x 0
182 119 178 179 181 127 129 128 132 dvmptres A + 1 A dx + 2 d x = x + 0
183 mulcl 2 1 x 2 1 x
184 25 141 183 sylancr A + 1 A x + 2 1 x
185 119 145 140 160 180 dvmptcmul A + 1 A dx + 2 log x d x = x + 2 1 x
186 119 176 177 182 139 184 185 dvmptsub A + 1 A dx + 2 2 log x d x = x + 0 2 1 x
187 119 138 142 173 174 175 186 dvmptadd A + 1 A dx + log x 2 + 2 - 2 log x d x = x + 2 log x 1 x + 0 - 2 1 x
188 139 176 141 subdird A + 1 A x + 2 log x 2 1 x = 2 log x 1 x 2 1 x
189 136 recnd A + 1 A x + 2 log x 2
190 rpne0 x + x 0
191 190 adantl A + 1 A x + x 0
192 189 120 191 divrecd A + 1 A x + 2 log x 2 x = 2 log x 2 1 x
193 df-neg 2 1 x = 0 2 1 x
194 193 oveq2i 2 log x 1 x + 2 1 x = 2 log x 1 x + 0 - 2 1 x
195 142 184 negsubd A + 1 A x + 2 log x 1 x + 2 1 x = 2 log x 1 x 2 1 x
196 194 195 syl5eqr A + 1 A x + 2 log x 1 x + 0 - 2 1 x = 2 log x 1 x 2 1 x
197 188 192 196 3eqtr4rd A + 1 A x + 2 log x 1 x + 0 - 2 1 x = 2 log x 2 x
198 197 mpteq2dva A + 1 A x + 2 log x 1 x + 0 - 2 1 x = x + 2 log x 2 x
199 187 198 eqtrd A + 1 A dx + log x 2 + 2 - 2 log x d x = x + 2 log x 2 x
200 119 120 121 133 134 137 199 dvmptmul A + 1 A dx + x log x 2 + 2 - 2 log x d x = x + 1 log x 2 + 2 - 2 log x + 2 log x 2 x x
201 134 mulid2d A + 1 A x + 1 log x 2 + 2 - 2 log x = log x 2 + 2 - 2 log x
202 138 139 176 subsub2d A + 1 A x + log x 2 2 log x 2 = log x 2 + 2 - 2 log x
203 201 202 eqtr4d A + 1 A x + 1 log x 2 + 2 - 2 log x = log x 2 2 log x 2
204 189 120 191 divcan1d A + 1 A x + 2 log x 2 x x = 2 log x 2
205 203 204 oveq12d A + 1 A x + 1 log x 2 + 2 - 2 log x + 2 log x 2 x x = log x 2 2 log x 2 + 2 log x - 2
206 138 189 npcand A + 1 A x + log x 2 2 log x 2 + 2 log x - 2 = log x 2
207 205 206 eqtrd A + 1 A x + 1 log x 2 + 2 - 2 log x + 2 log x 2 x x = log x 2
208 207 mpteq2dva A + 1 A x + 1 log x 2 + 2 - 2 log x + 2 log x 2 x x = x + log x 2
209 200 208 eqtrd A + 1 A dx + x log x 2 + 2 - 2 log x d x = x + log x 2
210 fveq2 x = n log x = log n
211 210 oveq1d x = n log x 2 = log n 2
212 simp32 A + 1 A x + n + 1 x x n n +∞ x n
213 simp2l A + 1 A x + n + 1 x x n n +∞ x +
214 simp2r A + 1 A x + n + 1 x x n n +∞ n +
215 213 214 logled A + 1 A x + n + 1 x x n n +∞ x n log x log n
216 212 215 mpbid A + 1 A x + n + 1 x x n n +∞ log x log n
217 213 relogcld A + 1 A x + n + 1 x x n n +∞ log x
218 214 relogcld A + 1 A x + n + 1 x x n n +∞ log n
219 simp31 A + 1 A x + n + 1 x x n n +∞ 1 x
220 logleb 1 + x + 1 x log 1 log x
221 54 213 220 sylancr A + 1 A x + n + 1 x x n n +∞ 1 x log 1 log x
222 219 221 mpbid A + 1 A x + n + 1 x x n n +∞ log 1 log x
223 64 222 eqbrtrrid A + 1 A x + n + 1 x x n n +∞ 0 log x
224 214 rpred A + 1 A x + n + 1 x x n n +∞ n
225 1red A + 1 A x + n + 1 x x n n +∞ 1
226 213 rpred A + 1 A x + n + 1 x x n n +∞ x
227 225 226 224 219 212 letrd A + 1 A x + n + 1 x x n n +∞ 1 n
228 224 227 logge0d A + 1 A x + n + 1 x x n n +∞ 0 log n
229 217 218 223 228 le2sqd A + 1 A x + n + 1 x x n n +∞ log x log n log x 2 log n 2
230 216 229 mpbid A + 1 A x + n + 1 x x n n +∞ log x 2 log n 2
231 relogcl x + log x
232 231 ad2antrl A + 1 A x + 1 x log x
233 232 sqge0d A + 1 A x + 1 x 0 log x 2
234 54 a1i A + 1 A 1 +
235 simpl A + 1 A A +
236 1le1 1 1
237 236 a1i A + 1 A 1 1
238 simpr A + 1 A 1 A
239 9 rexrd A + 1 A A *
240 pnfge A * A +∞
241 239 240 syl A + 1 A A +∞
242 94 95 96 97 99 103 104 115 109 117 209 211 230 50 233 234 235 237 238 241 44 dvfsum2 A + 1 A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x A x + n = 1 x log n 2 x log x 2 + 2 - 2 log x 1 log A 2
243 92 242 eqbrtrrd A + 1 A n = 1 A log n 2 - A log A 2 + 2 - 2 log A - -2 log A 2
244 24 29 12 38 243 letrd A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 log A 2
245 13 a1i A + 1 A 2
246 22 245 12 lesubaddd A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A 2 log A 2 n = 1 A log n 2 A log A 2 + 2 - 2 log A log A 2 + 2
247 244 246 mpbid A + 1 A n = 1 A log n 2 A log A 2 + 2 - 2 log A log A 2 + 2