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+1An=1Alogn2AlogA2+2-2logAlogA2+2

Proof

Step Hyp Ref Expression
1 fzfid A+1A1AFin
2 elfznn n1An
3 2 adantl A+1An1An
4 3 nnrpd A+1An1An+
5 4 relogcld A+1An1Alogn
6 5 resqcld A+1An1Alogn2
7 1 6 fsumrecl A+1An=1Alogn2
8 rpre A+A
9 8 adantr A+1AA
10 relogcl A+logA
11 10 adantr A+1AlogA
12 11 resqcld A+1AlogA2
13 2re 2
14 remulcl 2logA2logA
15 13 11 14 sylancr A+1A2logA
16 resubcl 22logA22logA
17 13 15 16 sylancr A+1A22logA
18 12 17 readdcld A+1AlogA2+2-2logA
19 9 18 remulcld A+1AAlogA2+2-2logA
20 7 19 resubcld A+1An=1Alogn2AlogA2+2-2logA
21 20 recnd A+1An=1Alogn2AlogA2+2-2logA
22 21 abscld A+1An=1Alogn2AlogA2+2-2logA
23 resubcl n=1Alogn2AlogA2+2-2logA2n=1Alogn2AlogA2+2-2logA2
24 22 13 23 sylancl A+1An=1Alogn2AlogA2+2-2logA2
25 2cn 2
26 25 negcli 2
27 subcl n=1Alogn2AlogA2+2-2logA2n=1Alogn2-AlogA2+2-2logA--2
28 21 26 27 sylancl A+1An=1Alogn2-AlogA2+2-2logA--2
29 28 abscld A+1An=1Alogn2-AlogA2+2-2logA--2
30 25 absnegi 2=2
31 0le2 02
32 absid 2022=2
33 13 31 32 mp2an 2=2
34 30 33 eqtri 2=2
35 34 oveq2i n=1Alogn2AlogA2+2-2logA2=n=1Alogn2AlogA2+2-2logA2
36 abs2dif n=1Alogn2AlogA2+2-2logA2n=1Alogn2AlogA2+2-2logA2n=1Alogn2-AlogA2+2-2logA--2
37 21 26 36 sylancl A+1An=1Alogn2AlogA2+2-2logA2n=1Alogn2-AlogA2+2-2logA--2
38 35 37 eqbrtrrid A+1An=1Alogn2AlogA2+2-2logA2n=1Alogn2-AlogA2+2-2logA--2
39 fveq2 x=Ax=A
40 39 oveq2d x=A1x=1A
41 40 sumeq1d x=An=1xlogn2=n=1Alogn2
42 id x=Ax=A
43 fveq2 x=Alogx=logA
44 43 oveq1d x=Alogx2=logA2
45 43 oveq2d x=A2logx=2logA
46 45 oveq2d x=A22logx=22logA
47 44 46 oveq12d x=Alogx2+2-2logx=logA2+2-2logA
48 42 47 oveq12d x=Axlogx2+2-2logx=AlogA2+2-2logA
49 41 48 oveq12d x=An=1xlogn2xlogx2+2-2logx=n=1Alogn2AlogA2+2-2logA
50 eqid x+n=1xlogn2xlogx2+2-2logx=x+n=1xlogn2xlogx2+2-2logx
51 ovex n=1xlogn2xlogx2+2-2logxV
52 49 50 51 fvmpt3i A+x+n=1xlogn2xlogx2+2-2logxA=n=1Alogn2AlogA2+2-2logA
53 52 adantr A+1Ax+n=1xlogn2xlogx2+2-2logxA=n=1Alogn2AlogA2+2-2logA
54 1rp 1+
55 fveq2 x=1x=1
56 1z 1
57 flid 11=1
58 56 57 ax-mp 1=1
59 55 58 eqtrdi x=1x=1
60 59 oveq2d x=11x=11
61 60 sumeq1d x=1n=1xlogn2=n=11logn2
62 0cn 0
63 fveq2 n=1logn=log1
64 log1 log1=0
65 63 64 eqtrdi n=1logn=0
66 65 sq0id n=1logn2=0
67 66 fsum1 10n=11logn2=0
68 56 62 67 mp2an n=11logn2=0
69 61 68 eqtrdi x=1n=1xlogn2=0
70 id x=1x=1
71 fveq2 x=1logx=log1
72 71 64 eqtrdi x=1logx=0
73 72 sq0id x=1logx2=0
74 72 oveq2d x=12logx=20
75 2t0e0 20=0
76 74 75 eqtrdi x=12logx=0
77 76 oveq2d x=122logx=20
78 25 subid1i 20=2
79 77 78 eqtrdi x=122logx=2
80 73 79 oveq12d x=1logx2+2-2logx=0+2
81 25 addid2i 0+2=2
82 80 81 eqtrdi x=1logx2+2-2logx=2
83 70 82 oveq12d x=1xlogx2+2-2logx=12
84 25 mulid2i 12=2
85 83 84 eqtrdi x=1xlogx2+2-2logx=2
86 69 85 oveq12d x=1n=1xlogn2xlogx2+2-2logx=02
87 df-neg 2=02
88 86 87 eqtr4di x=1n=1xlogn2xlogx2+2-2logx=2
89 88 50 51 fvmpt3i 1+x+n=1xlogn2xlogx2+2-2logx1=2
90 54 89 mp1i A+1Ax+n=1xlogn2xlogx2+2-2logx1=2
91 53 90 oveq12d A+1Ax+n=1xlogn2xlogx2+2-2logxAx+n=1xlogn2xlogx2+2-2logx1=n=1Alogn2-AlogA2+2-2logA--2
92 91 fveq2d A+1Ax+n=1xlogn2xlogx2+2-2logxAx+n=1xlogn2xlogx2+2-2logx1=n=1Alogn2-AlogA2+2-2logA--2
93 ioorp 0+∞=+
94 93 eqcomi +=0+∞
95 nnuz =1
96 56 a1i A+1A1
97 1red A+1A1
98 pnfxr +∞*
99 98 a1i A+1A+∞*
100 1re 1
101 1nn0 10
102 100 101 nn0addge1i 11+1
103 102 a1i A+1A11+1
104 0red A+1A0
105 rpre x+x
106 105 adantl A+1Ax+x
107 simpr A+1Ax+x+
108 107 relogcld A+1Ax+logx
109 108 resqcld A+1Ax+logx2
110 remulcl 2logx2logx
111 13 108 110 sylancr A+1Ax+2logx
112 resubcl 22logx22logx
113 13 111 112 sylancr A+1Ax+22logx
114 109 113 readdcld A+1Ax+logx2+2-2logx
115 106 114 remulcld A+1Ax+xlogx2+2-2logx
116 nnrp xx+
117 116 109 sylan2 A+1Axlogx2
118 reelprrecn
119 118 a1i A+1A
120 106 recnd A+1Ax+x
121 1red A+1Ax+1
122 recn xx
123 122 adantl A+1Axx
124 1red A+1Ax1
125 119 dvmptid A+1Adxxdx=x1
126 rpssre +
127 126 a1i A+1A+
128 eqid TopOpenfld=TopOpenfld
129 128 tgioo2 topGenran.=TopOpenfld𝑡
130 iooretop 0+∞topGenran.
131 93 130 eqeltrri +topGenran.
132 131 a1i A+1A+topGenran.
133 119 123 124 125 127 129 128 132 dvmptres A+1Adx+xdx=x+1
134 114 recnd A+1Ax+logx2+2-2logx
135 resubcl 2logx22logx2
136 111 13 135 sylancl A+1Ax+2logx2
137 136 107 rerpdivcld A+1Ax+2logx2x
138 109 recnd A+1Ax+logx2
139 111 recnd A+1Ax+2logx
140 107 rpreccld A+1Ax+1x+
141 140 rpcnd A+1Ax+1x
142 139 141 mulcld A+1Ax+2logx1x
143 cnelprrecn
144 143 a1i A+1A
145 108 recnd A+1Ax+logx
146 sqcl yy2
147 146 adantl A+1Ayy2
148 simpr A+1Ayy
149 mulcl 2y2y
150 25 148 149 sylancr A+1Ay2y
151 relogf1o log+:+1-1 onto
152 f1of log+:+1-1 ontolog+:+
153 151 152 mp1i A+1Alog+:+
154 153 feqmptd A+1Alog+=x+log+x
155 fvres x+log+x=logx
156 155 mpteq2ia x+log+x=x+logx
157 154 156 eqtrdi A+1Alog+=x+logx
158 157 oveq2d A+1ADlog+=dx+logxdx
159 dvrelog Dlog+=x+1x
160 158 159 eqtr3di A+1Adx+logxdx=x+1x
161 2nn 2
162 dvexp 2dyy2dy=y2y21
163 161 162 mp1i A+1Adyy2dy=y2y21
164 2m1e1 21=1
165 164 oveq2i y21=y1
166 exp1 yy1=y
167 165 166 eqtrid yy21=y
168 167 oveq2d y2y21=2y
169 168 mpteq2ia y2y21=y2y
170 163 169 eqtrdi A+1Adyy2dy=y2y
171 oveq1 y=logxy2=logx2
172 oveq2 y=logx2y=2logx
173 119 144 145 140 147 150 160 170 171 172 dvmptco A+1Adx+logx2dx=x+2logx1x
174 113 recnd A+1Ax+22logx
175 ovexd A+1Ax+021xV
176 2cnd A+1Ax+2
177 0red A+1Ax+0
178 2cnd A+1Ax2
179 0red A+1Ax0
180 2cnd A+1A2
181 119 180 dvmptc A+1Adx2dx=x0
182 119 178 179 181 127 129 128 132 dvmptres A+1Adx+2dx=x+0
183 mulcl 21x21x
184 25 141 183 sylancr A+1Ax+21x
185 119 145 140 160 180 dvmptcmul A+1Adx+2logxdx=x+21x
186 119 176 177 182 139 184 185 dvmptsub A+1Adx+22logxdx=x+021x
187 119 138 142 173 174 175 186 dvmptadd A+1Adx+logx2+2-2logxdx=x+2logx1x+0-21x
188 139 176 141 subdird A+1Ax+2logx21x=2logx1x21x
189 136 recnd A+1Ax+2logx2
190 rpne0 x+x0
191 190 adantl A+1Ax+x0
192 189 120 191 divrecd A+1Ax+2logx2x=2logx21x
193 df-neg 21x=021x
194 193 oveq2i 2logx1x+21x=2logx1x+0-21x
195 142 184 negsubd A+1Ax+2logx1x+21x=2logx1x21x
196 194 195 eqtr3id A+1Ax+2logx1x+0-21x=2logx1x21x
197 188 192 196 3eqtr4rd A+1Ax+2logx1x+0-21x=2logx2x
198 197 mpteq2dva A+1Ax+2logx1x+0-21x=x+2logx2x
199 187 198 eqtrd A+1Adx+logx2+2-2logxdx=x+2logx2x
200 119 120 121 133 134 137 199 dvmptmul A+1Adx+xlogx2+2-2logxdx=x+1logx2+2-2logx+2logx2xx
201 134 mulid2d A+1Ax+1logx2+2-2logx=logx2+2-2logx
202 138 139 176 subsub2d A+1Ax+logx22logx2=logx2+2-2logx
203 201 202 eqtr4d A+1Ax+1logx2+2-2logx=logx22logx2
204 189 120 191 divcan1d A+1Ax+2logx2xx=2logx2
205 203 204 oveq12d A+1Ax+1logx2+2-2logx+2logx2xx=logx22logx2+2logx-2
206 138 189 npcand A+1Ax+logx22logx2+2logx-2=logx2
207 205 206 eqtrd A+1Ax+1logx2+2-2logx+2logx2xx=logx2
208 207 mpteq2dva A+1Ax+1logx2+2-2logx+2logx2xx=x+logx2
209 200 208 eqtrd A+1Adx+xlogx2+2-2logxdx=x+logx2
210 fveq2 x=nlogx=logn
211 210 oveq1d x=nlogx2=logn2
212 simp32 A+1Ax+n+1xxnn+∞xn
213 simp2l A+1Ax+n+1xxnn+∞x+
214 simp2r A+1Ax+n+1xxnn+∞n+
215 213 214 logled A+1Ax+n+1xxnn+∞xnlogxlogn
216 212 215 mpbid A+1Ax+n+1xxnn+∞logxlogn
217 213 relogcld A+1Ax+n+1xxnn+∞logx
218 214 relogcld A+1Ax+n+1xxnn+∞logn
219 simp31 A+1Ax+n+1xxnn+∞1x
220 logleb 1+x+1xlog1logx
221 54 213 220 sylancr A+1Ax+n+1xxnn+∞1xlog1logx
222 219 221 mpbid A+1Ax+n+1xxnn+∞log1logx
223 64 222 eqbrtrrid A+1Ax+n+1xxnn+∞0logx
224 214 rpred A+1Ax+n+1xxnn+∞n
225 1red A+1Ax+n+1xxnn+∞1
226 213 rpred A+1Ax+n+1xxnn+∞x
227 225 226 224 219 212 letrd A+1Ax+n+1xxnn+∞1n
228 224 227 logge0d A+1Ax+n+1xxnn+∞0logn
229 217 218 223 228 le2sqd A+1Ax+n+1xxnn+∞logxlognlogx2logn2
230 216 229 mpbid A+1Ax+n+1xxnn+∞logx2logn2
231 relogcl x+logx
232 231 ad2antrl A+1Ax+1xlogx
233 232 sqge0d A+1Ax+1x0logx2
234 54 a1i A+1A1+
235 simpl A+1AA+
236 1le1 11
237 236 a1i A+1A11
238 simpr A+1A1A
239 9 rexrd A+1AA*
240 pnfge A*A+∞
241 239 240 syl A+1AA+∞
242 94 95 96 97 99 103 104 115 109 117 209 211 230 50 233 234 235 237 238 241 44 dvfsum2 A+1Ax+n=1xlogn2xlogx2+2-2logxAx+n=1xlogn2xlogx2+2-2logx1logA2
243 92 242 eqbrtrrd A+1An=1Alogn2-AlogA2+2-2logA--2logA2
244 24 29 12 38 243 letrd A+1An=1Alogn2AlogA2+2-2logA2logA2
245 13 a1i A+1A2
246 22 245 12 lesubaddd A+1An=1Alogn2AlogA2+2-2logA2logA2n=1Alogn2AlogA2+2-2logAlogA2+2
247 244 246 mpbid A+1An=1Alogn2AlogA2+2-2logAlogA2+2