Metamath Proof Explorer


Theorem chpdifbndlem1

Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses chpdifbnd.a φA+
chpdifbnd.1 φ1A
chpdifbnd.b φB+
chpdifbnd.2 φz1+∞ψzlogz+m=1zΛmψzmz2logzB
chpdifbnd.c C=BA+1+2AlogA
chpdifbnd.x φX1+∞
chpdifbnd.y φYXAX
Assertion chpdifbndlem1 φψYψX2YX+CXlogX

Proof

Step Hyp Ref Expression
1 chpdifbnd.a φA+
2 chpdifbnd.1 φ1A
3 chpdifbnd.b φB+
4 chpdifbnd.2 φz1+∞ψzlogz+m=1zΛmψzmz2logzB
5 chpdifbnd.c C=BA+1+2AlogA
6 chpdifbnd.x φX1+∞
7 chpdifbnd.y φYXAX
8 ioossre 1+∞
9 8 6 sselid φX
10 1 rpred φA
11 10 9 remulcld φAX
12 elicc2 XAXYXAXYXYYAX
13 9 11 12 syl2anc φYXAXYXYYAX
14 7 13 mpbid φYXYYAX
15 14 simp1d φY
16 chpcl YψY
17 15 16 syl φψY
18 chpcl XψX
19 9 18 syl φψX
20 17 19 resubcld φψYψX
21 0red φ0
22 1re 1
23 22 a1i φ1
24 0lt1 0<1
25 24 a1i φ0<1
26 eliooord X1+∞1<XX<+∞
27 6 26 syl φ1<XX<+∞
28 27 simpld φ1<X
29 21 23 9 25 28 lttrd φ0<X
30 9 29 elrpd φX+
31 30 relogcld φlogX
32 20 31 remulcld φψYψXlogX
33 2re 2
34 15 9 resubcld φYX
35 remulcl 2YX2YX
36 33 34 35 sylancr φ2YX
37 36 31 remulcld φ2YXlogX
38 3 rpred φB
39 15 9 readdcld φY+X
40 38 39 remulcld φBY+X
41 1 relogcld φlogA
42 remulcl 2logA2logA
43 33 41 42 sylancr φ2logA
44 43 15 remulcld φ2logAY
45 40 44 readdcld φBY+X+2logAY
46 37 45 readdcld φ2YXlogX+BY+X+2logAY
47 peano2re AA+1
48 10 47 syl φA+1
49 38 48 remulcld φBA+1
50 remulcl 2A2A
51 33 10 50 sylancr φ2A
52 51 41 remulcld φ2AlogA
53 49 52 readdcld φBA+1+2AlogA
54 5 53 eqeltrid φC
55 54 9 remulcld φCX
56 37 55 readdcld φ2YXlogX+CX
57 17 31 remulcld φψYlogX
58 fzfid φ1XFin
59 14 simp2d φXY
60 flword2 XYXYYX
61 9 15 59 60 syl3anc φYX
62 fzss2 YX1X1Y
63 61 62 syl φ1X1Y
64 63 sselda φn1Xn1Y
65 elfznn n1Yn
66 65 adantl φn1Yn
67 vmacl nΛn
68 66 67 syl φn1YΛn
69 nndivre XnXn
70 9 65 69 syl2an φn1YXn
71 chpcl XnψXn
72 70 71 syl φn1YψXn
73 68 72 remulcld φn1YΛnψXn
74 64 73 syldan φn1XΛnψXn
75 58 74 fsumrecl φn=1XΛnψXn
76 57 75 readdcld φψYlogX+n=1XΛnψXn
77 remulcl 2logX2logX
78 33 31 77 sylancr φ2logX
79 78 38 resubcld φ2logXB
80 79 9 remulcld φ2logXBX
81 1 30 rpmulcld φAX+
82 81 relogcld φlogAX
83 remulcl 2logAX2logAX
84 33 82 83 sylancr φ2logAX
85 38 84 readdcld φB+2logAX
86 85 15 remulcld φB+2logAXY
87 19 31 remulcld φψXlogX
88 87 75 readdcld φψXlogX+n=1XΛnψXn
89 21 9 15 29 59 ltletrd φ0<Y
90 15 89 elrpd φY+
91 90 relogcld φlogY
92 17 91 remulcld φψYlogY
93 fzfid φ1YFin
94 nndivre YnYn
95 15 65 94 syl2an φn1YYn
96 chpcl YnψYn
97 95 96 syl φn1YψYn
98 68 97 remulcld φn1YΛnψYn
99 93 98 fsumrecl φn=1YΛnψYn
100 92 99 readdcld φψYlogY+n=1YΛnψYn
101 chpge0 Y0ψY
102 15 101 syl φ0ψY
103 30 90 logled φXYlogXlogY
104 59 103 mpbid φlogXlogY
105 31 91 17 102 104 lemul2ad φψYlogXψYlogY
106 93 73 fsumrecl φn=1YΛnψXn
107 vmage0 n0Λn
108 66 107 syl φn1Y0Λn
109 chpge0 Xn0ψXn
110 70 109 syl φn1Y0ψXn
111 68 72 108 110 mulge0d φn1Y0ΛnψXn
112 93 73 111 63 fsumless φn=1XΛnψXnn=1YΛnψXn
113 9 adantr φn1YX
114 15 adantr φn1YY
115 66 nnrpd φn1Yn+
116 59 adantr φn1YXY
117 113 114 115 116 lediv1dd φn1YXnYn
118 chpwordi XnYnXnYnψXnψYn
119 70 95 117 118 syl3anc φn1YψXnψYn
120 72 97 68 108 119 lemul2ad φn1YΛnψXnΛnψYn
121 93 73 98 120 fsumle φn=1YΛnψXnn=1YΛnψYn
122 75 106 99 112 121 letrd φn=1XΛnψXnn=1YΛnψYn
123 57 75 92 99 105 122 le2addd φψYlogX+n=1XΛnψXnψYlogY+n=1YΛnψYn
124 100 90 rerpdivcld φψYlogY+n=1YΛnψYnY
125 remulcl 2logY2logY
126 33 91 125 sylancr φ2logY
127 38 126 readdcld φB+2logY
128 124 126 resubcld φψYlogY+n=1YΛnψYnY2logY
129 128 recnd φψYlogY+n=1YΛnψYnY2logY
130 129 abscld φψYlogY+n=1YΛnψYnY2logY
131 128 leabsd φψYlogY+n=1YΛnψYnY2logYψYlogY+n=1YΛnψYnY2logY
132 fveq2 z=Yψz=ψY
133 fveq2 z=Ylogz=logY
134 132 133 oveq12d z=Yψzlogz=ψYlogY
135 fveq2 m=nΛm=Λn
136 oveq2 m=nzm=zn
137 136 fveq2d m=nψzm=ψzn
138 135 137 oveq12d m=nΛmψzm=Λnψzn
139 138 cbvsumv m=1zΛmψzm=n=1zΛnψzn
140 fveq2 z=Yz=Y
141 140 oveq2d z=Y1z=1Y
142 simpl z=Yn1Yz=Y
143 142 fvoveq1d z=Yn1Yψzn=ψYn
144 143 oveq2d z=Yn1YΛnψzn=ΛnψYn
145 141 144 sumeq12rdv z=Yn=1zΛnψzn=n=1YΛnψYn
146 139 145 eqtrid z=Ym=1zΛmψzm=n=1YΛnψYn
147 134 146 oveq12d z=Yψzlogz+m=1zΛmψzm=ψYlogY+n=1YΛnψYn
148 id z=Yz=Y
149 147 148 oveq12d z=Yψzlogz+m=1zΛmψzmz=ψYlogY+n=1YΛnψYnY
150 133 oveq2d z=Y2logz=2logY
151 149 150 oveq12d z=Yψzlogz+m=1zΛmψzmz2logz=ψYlogY+n=1YΛnψYnY2logY
152 151 fveq2d z=Yψzlogz+m=1zΛmψzmz2logz=ψYlogY+n=1YΛnψYnY2logY
153 152 breq1d z=Yψzlogz+m=1zΛmψzmz2logzBψYlogY+n=1YΛnψYnY2logYB
154 23 9 28 ltled φ1X
155 23 9 15 154 59 letrd φ1Y
156 elicopnf 1Y1+∞Y1Y
157 22 156 ax-mp Y1+∞Y1Y
158 15 155 157 sylanbrc φY1+∞
159 153 4 158 rspcdva φψYlogY+n=1YΛnψYnY2logYB
160 128 130 38 131 159 letrd φψYlogY+n=1YΛnψYnY2logYB
161 124 126 38 lesubaddd φψYlogY+n=1YΛnψYnY2logYBψYlogY+n=1YΛnψYnYB+2logY
162 160 161 mpbid φψYlogY+n=1YΛnψYnYB+2logY
163 14 simp3d φYAX
164 90 81 logled φYAXlogYlogAX
165 163 164 mpbid φlogYlogAX
166 2pos 0<2
167 33 166 pm3.2i 20<2
168 167 a1i φ20<2
169 lemul2 logYlogAX20<2logYlogAX2logY2logAX
170 91 82 168 169 syl3anc φlogYlogAX2logY2logAX
171 165 170 mpbid φ2logY2logAX
172 126 84 38 171 leadd2dd φB+2logYB+2logAX
173 124 127 85 162 172 letrd φψYlogY+n=1YΛnψYnYB+2logAX
174 100 85 90 ledivmul2d φψYlogY+n=1YΛnψYnYB+2logAXψYlogY+n=1YΛnψYnB+2logAXY
175 173 174 mpbid φψYlogY+n=1YΛnψYnB+2logAXY
176 76 100 86 123 175 letrd φψYlogX+n=1XΛnψXnB+2logAXY
177 fveq2 z=Xψz=ψX
178 fveq2 z=Xlogz=logX
179 177 178 oveq12d z=Xψzlogz=ψXlogX
180 fveq2 z=Xz=X
181 180 oveq2d z=X1z=1X
182 simpl z=Xn1Xz=X
183 182 fvoveq1d z=Xn1Xψzn=ψXn
184 183 oveq2d z=Xn1XΛnψzn=ΛnψXn
185 181 184 sumeq12rdv z=Xn=1zΛnψzn=n=1XΛnψXn
186 139 185 eqtrid z=Xm=1zΛmψzm=n=1XΛnψXn
187 179 186 oveq12d z=Xψzlogz+m=1zΛmψzm=ψXlogX+n=1XΛnψXn
188 id z=Xz=X
189 187 188 oveq12d z=Xψzlogz+m=1zΛmψzmz=ψXlogX+n=1XΛnψXnX
190 178 oveq2d z=X2logz=2logX
191 189 190 oveq12d z=Xψzlogz+m=1zΛmψzmz2logz=ψXlogX+n=1XΛnψXnX2logX
192 191 fveq2d z=Xψzlogz+m=1zΛmψzmz2logz=ψXlogX+n=1XΛnψXnX2logX
193 192 breq1d z=Xψzlogz+m=1zΛmψzmz2logzBψXlogX+n=1XΛnψXnX2logXB
194 elicopnf 1X1+∞X1X
195 22 194 ax-mp X1+∞X1X
196 9 154 195 sylanbrc φX1+∞
197 193 4 196 rspcdva φψXlogX+n=1XΛnψXnX2logXB
198 88 30 rerpdivcld φψXlogX+n=1XΛnψXnX
199 198 78 38 absdifled φψXlogX+n=1XΛnψXnX2logXB2logXBψXlogX+n=1XΛnψXnXψXlogX+n=1XΛnψXnX2logX+B
200 197 199 mpbid φ2logXBψXlogX+n=1XΛnψXnXψXlogX+n=1XΛnψXnX2logX+B
201 200 simpld φ2logXBψXlogX+n=1XΛnψXnX
202 79 88 30 lemuldivd φ2logXBXψXlogX+n=1XΛnψXn2logXBψXlogX+n=1XΛnψXnX
203 201 202 mpbird φ2logXBXψXlogX+n=1XΛnψXn
204 76 80 86 88 176 203 le2subd φψYlogX+n=1XΛnψXn-ψXlogX+n=1XΛnψXnB+2logAXY2logXBX
205 57 recnd φψYlogX
206 87 recnd φψXlogX
207 75 recnd φn=1XΛnψXn
208 205 206 207 pnpcan2d φψYlogX+n=1XΛnψXn-ψXlogX+n=1XΛnψXn=ψYlogXψXlogX
209 17 recnd φψY
210 19 recnd φψX
211 31 recnd φlogX
212 209 210 211 subdird φψYψXlogX=ψYlogXψXlogX
213 208 212 eqtr4d φψYlogX+n=1XΛnψXn-ψXlogX+n=1XΛnψXn=ψYψXlogX
214 78 15 remulcld φ2logXY
215 214 recnd φ2logXY
216 38 43 readdcld φB+2logA
217 216 15 remulcld φB+2logAY
218 217 recnd φB+2logAY
219 78 9 remulcld φ2logXX
220 219 recnd φ2logXX
221 38 9 remulcld φBX
222 221 recnd φBX
223 222 negcld φBX
224 215 218 220 223 addsub4d φ2logXY+B+2logAY-2logXX+BX=2logXY2logXX+B+2logAY-BX
225 41 recnd φlogA
226 1 30 relogmuld φlogAX=logA+logX
227 225 211 226 comraddd φlogAX=logX+logA
228 227 oveq2d φ2logAX=2logX+logA
229 2cnd φ2
230 229 211 225 adddid φ2logX+logA=2logX+2logA
231 228 230 eqtrd φ2logAX=2logX+2logA
232 231 oveq2d φB+2logAX=B+2logX+2logA
233 38 recnd φB
234 78 recnd φ2logX
235 43 recnd φ2logA
236 233 234 235 add12d φB+2logX+2logA=2logX+B+2logA
237 232 236 eqtrd φB+2logAX=2logX+B+2logA
238 237 oveq1d φB+2logAXY=2logX+B+2logAY
239 216 recnd φB+2logA
240 15 recnd φY
241 234 239 240 adddird φ2logX+B+2logAY=2logXY+B+2logAY
242 238 241 eqtrd φB+2logAXY=2logXY+B+2logAY
243 9 recnd φX
244 234 233 243 subdird φ2logXBX=2logXXBX
245 220 222 negsubd φ2logXX+BX=2logXXBX
246 244 245 eqtr4d φ2logXBX=2logXX+BX
247 242 246 oveq12d φB+2logAXY2logXBX=2logXY+B+2logAY-2logXX+BX
248 34 recnd φYX
249 229 248 211 mul32d φ2YXlogX=2logXYX
250 234 240 243 subdid φ2logXYX=2logXY2logXX
251 249 250 eqtrd φ2YXlogX=2logXY2logXX
252 38 15 remulcld φBY
253 252 recnd φBY
254 44 recnd φ2logAY
255 253 222 254 add32d φBY+BX+2logAY=BY+2logAY+BX
256 233 240 243 adddid φBY+X=BY+BX
257 256 oveq1d φBY+X+2logAY=BY+BX+2logAY
258 233 235 240 adddird φB+2logAY=BY+2logAY
259 258 oveq1d φB+2logAY+BX=BY+2logAY+BX
260 255 257 259 3eqtr4d φBY+X+2logAY=B+2logAY+BX
261 218 222 subnegd φB+2logAYBX=B+2logAY+BX
262 260 261 eqtr4d φBY+X+2logAY=B+2logAYBX
263 251 262 oveq12d φ2YXlogX+BY+X+2logAY=2logXY2logXX+B+2logAY-BX
264 224 247 263 3eqtr4d φB+2logAXY2logXBX=2YXlogX+BY+X+2logAY
265 204 213 264 3brtr3d φψYψXlogX2YXlogX+BY+X+2logAY
266 49 9 remulcld φBA+1X
267 52 9 remulcld φ2AlogAX
268 15 11 9 163 leadd1dd φY+XAX+X
269 10 recnd φA
270 269 243 adddirp1d φA+1X=AX+X
271 268 270 breqtrrd φY+XA+1X
272 48 9 remulcld φA+1X
273 39 272 3 lemul2d φY+XA+1XBY+XBA+1X
274 271 273 mpbid φBY+XBA+1X
275 48 recnd φA+1
276 233 275 243 mulassd φBA+1X=BA+1X
277 274 276 breqtrrd φBY+XBA+1X
278 33 a1i φ2
279 0le2 02
280 279 a1i φ02
281 log1 log1=0
282 1rp 1+
283 logleb 1+A+1Alog1logA
284 282 1 283 sylancr φ1Alog1logA
285 2 284 mpbid φlog1logA
286 281 285 eqbrtrrid φ0logA
287 278 41 280 286 mulge0d φ02logA
288 15 11 43 287 163 lemul2ad φ2logAY2logAAX
289 51 recnd φ2A
290 289 225 243 mulassd φ2AlogAX=2AlogAX
291 229 269 225 243 mul4d φ2AlogAX=2logAAX
292 290 291 eqtrd φ2AlogAX=2logAAX
293 288 292 breqtrrd φ2logAY2AlogAX
294 40 44 266 267 277 293 le2addd φBY+X+2logAYBA+1X+2AlogAX
295 5 oveq1i CX=BA+1+2AlogAX
296 49 recnd φBA+1
297 52 recnd φ2AlogA
298 296 297 243 adddird φBA+1+2AlogAX=BA+1X+2AlogAX
299 295 298 eqtrid φCX=BA+1X+2AlogAX
300 294 299 breqtrrd φBY+X+2logAYCX
301 45 55 37 300 leadd2dd φ2YXlogX+BY+X+2logAY2YXlogX+CX
302 32 46 56 265 301 letrd φψYψXlogX2YXlogX+CX
303 36 recnd φ2YX
304 9 28 rplogcld φlogX+
305 9 304 rerpdivcld φXlogX
306 54 305 remulcld φCXlogX
307 306 recnd φCXlogX
308 303 307 211 adddird φ2YX+CXlogXlogX=2YXlogX+CXlogXlogX
309 54 recnd φC
310 305 recnd φXlogX
311 309 310 211 mulassd φCXlogXlogX=CXlogXlogX
312 304 rpne0d φlogX0
313 243 211 312 divcan1d φXlogXlogX=X
314 313 oveq2d φCXlogXlogX=CX
315 311 314 eqtrd φCXlogXlogX=CX
316 315 oveq2d φ2YXlogX+CXlogXlogX=2YXlogX+CX
317 308 316 eqtrd φ2YX+CXlogXlogX=2YXlogX+CX
318 302 317 breqtrrd φψYψXlogX2YX+CXlogXlogX
319 36 306 readdcld φ2YX+CXlogX
320 20 319 304 lemul1d φψYψX2YX+CXlogXψYψXlogX2YX+CXlogXlogX
321 318 320 mpbird φψYψX2YX+CXlogX