Metamath Proof Explorer


Theorem etransclem46

Description: This is the proof for equation *(7) in Juillerat p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large P , but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem46.q φ Q Poly 0 𝑝
etransclem46.qe0 φ Q e = 0
etransclem46.a A = coeff Q
etransclem46.m M = deg Q
etransclem46.rex φ
etransclem46.s φ
etransclem46.x φ TopOpen fld 𝑡
etransclem46.p φ P
etransclem46.f F = x x P 1 j = 1 M x j P
etransclem46.l L = j = 0 M A j e j 0 j e x F x dx
etransclem46.r R = M P + P - 1
etransclem46.g G = x i = 0 R D n F i x
etransclem46.h O = x 0 j e x G x
Assertion etransclem46 φ L P 1 ! = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !

Proof

Step Hyp Ref Expression
1 etransclem46.q φ Q Poly 0 𝑝
2 etransclem46.qe0 φ Q e = 0
3 etransclem46.a A = coeff Q
4 etransclem46.m M = deg Q
5 etransclem46.rex φ
6 etransclem46.s φ
7 etransclem46.x φ TopOpen fld 𝑡
8 etransclem46.p φ P
9 etransclem46.f F = x x P 1 j = 1 M x j P
10 etransclem46.l L = j = 0 M A j e j 0 j e x F x dx
11 etransclem46.r R = M P + P - 1
12 etransclem46.g G = x i = 0 R D n F i x
13 etransclem46.h O = x 0 j e x G x
14 10 a1i φ L = j = 0 M A j e j 0 j e x F x dx
15 13 oveq2i D O = dx 0 j e x G x d x
16 15 a1i φ j 0 M D O = dx 0 j e x G x d x
17 6 adantr φ j 0 M
18 ere e
19 18 recni e
20 19 a1i x e
21 recn x x
22 21 negcld x x
23 20 22 cxpcld x e x
24 23 adantl φ x e x
25 simpr φ x x
26 fzfid φ x 0 R Fin
27 elfznn0 i 0 R i 0
28 6 adantr φ i 0
29 7 adantr φ i 0 TopOpen fld 𝑡
30 8 adantr φ i 0 P
31 1 eldifad φ Q Poly
32 dgrcl Q Poly deg Q 0
33 31 32 syl φ deg Q 0
34 4 33 eqeltrid φ M 0
35 34 adantr φ i 0 M 0
36 simpr φ i 0 i 0
37 28 29 30 35 9 36 etransclem33 φ i 0 D n F i :
38 27 37 sylan2 φ i 0 R D n F i :
39 38 adantlr φ x i 0 R D n F i :
40 simplr φ x i 0 R x
41 39 40 ffvelrnd φ x i 0 R D n F i x
42 26 41 fsumcl φ x i = 0 R D n F i x
43 12 fvmpt2 x i = 0 R D n F i x G x = i = 0 R D n F i x
44 25 42 43 syl2anc φ x G x = i = 0 R D n F i x
45 44 42 eqeltrd φ x G x
46 24 45 mulcld φ x e x G x
47 46 negcld φ x e x G x
48 47 adantlr φ j 0 M x e x G x
49 6 7 dvdmsscn φ
50 49 8 9 etransclem8 φ F :
51 50 ffvelrnda φ x F x
52 24 51 mulcld φ x e x F x
53 52 negcld φ x e x F x
54 53 negcld φ x e x F x
55 54 adantlr φ j 0 M x e x F x
56 18 a1i x e
57 0re 0
58 epos 0 < e
59 57 18 58 ltleii 0 e
60 59 a1i x 0 e
61 renegcl x x
62 56 60 61 recxpcld x e x
63 62 renegcld x e x
64 63 adantl φ x e x
65 reelprrecn
66 65 a1i
67 cnelprrecn
68 67 a1i
69 22 adantl x x
70 neg1rr 1
71 70 a1i x 1
72 19 a1i y e
73 id y y
74 72 73 cxpcld y e y
75 74 adantl y e y
76 21 adantl x x
77 1red x 1
78 66 dvmptid dx x d x = x 1
79 66 76 77 78 dvmptneg dx x d x = x 1
80 epr e +
81 dvcxp2 e + dy e y d y = y log e e y
82 80 81 ax-mp dy e y d y = y log e e y
83 loge log e = 1
84 83 oveq1i log e e y = 1 e y
85 74 mulid2d y 1 e y = e y
86 84 85 syl5eq y log e e y = e y
87 86 mpteq2ia y log e e y = y e y
88 82 87 eqtri dy e y d y = y e y
89 88 a1i dy e y d y = y e y
90 oveq2 y = x e y = e x
91 66 68 69 71 75 75 79 89 90 90 dvmptco dx e x d x = x e x -1
92 91 mptru dx e x d x = x e x -1
93 70 a1i x 1
94 93 recnd x 1
95 23 94 mulcomd x e x -1 = -1 e x
96 23 mulm1d x -1 e x = e x
97 95 96 eqtrd x e x -1 = e x
98 97 mpteq2ia x e x -1 = x e x
99 92 98 eqtri dx e x d x = x e x
100 99 a1i φ dx e x d x = x e x
101 27 adantl φ i 0 R i 0
102 peano2nn0 i 0 i + 1 0
103 101 102 syl φ i 0 R i + 1 0
104 ovex i + 1 V
105 eleq1 j = i + 1 j 0 i + 1 0
106 105 anbi2d j = i + 1 φ j 0 φ i + 1 0
107 fveq2 j = i + 1 D n F j = D n F i + 1
108 107 feq1d j = i + 1 D n F j : D n F i + 1 :
109 106 108 imbi12d j = i + 1 φ j 0 D n F j : φ i + 1 0 D n F i + 1 :
110 eleq1 i = j i 0 j 0
111 110 anbi2d i = j φ i 0 φ j 0
112 fveq2 i = j D n F i = D n F j
113 112 feq1d i = j D n F i : D n F j :
114 111 113 imbi12d i = j φ i 0 D n F i : φ j 0 D n F j :
115 114 37 chvarvv φ j 0 D n F j :
116 104 109 115 vtocl φ i + 1 0 D n F i + 1 :
117 103 116 syldan φ i 0 R D n F i + 1 :
118 117 adantlr φ x i 0 R D n F i + 1 :
119 118 40 ffvelrnd φ x i 0 R D n F i + 1 x
120 26 119 fsumcl φ x i = 0 R D n F i + 1 x
121 8 34 9 12 etransclem39 φ G :
122 121 feqmptd φ G = x G x
123 122 eqcomd φ x G x = G
124 123 oveq2d φ dx G x d x = D G
125 nfcv _ x F
126 elfznn0 i 0 R + 1 i 0
127 126 37 sylan2 φ i 0 R + 1 D n F i :
128 125 50 127 12 etransclem2 φ D G = x i = 0 R D n F i + 1 x
129 124 128 eqtrd φ dx G x d x = x i = 0 R D n F i + 1 x
130 6 24 64 100 45 120 129 dvmptmul φ dx e x G x d x = x e x G x + i = 0 R D n F i + 1 x e x
131 120 24 mulcomd φ x i = 0 R D n F i + 1 x e x = e x i = 0 R D n F i + 1 x
132 131 oveq2d φ x e x G x + i = 0 R D n F i + 1 x e x = e x G x + e x i = 0 R D n F i + 1 x
133 24 negcld φ x e x
134 133 45 mulcld φ x e x G x
135 24 120 mulcld φ x e x i = 0 R D n F i + 1 x
136 134 135 addcomd φ x e x G x + e x i = 0 R D n F i + 1 x = e x i = 0 R D n F i + 1 x + e x G x
137 135 46 negsubd φ x e x i = 0 R D n F i + 1 x + e x G x = e x i = 0 R D n F i + 1 x e x G x
138 24 45 mulneg1d φ x e x G x = e x G x
139 138 oveq2d φ x e x i = 0 R D n F i + 1 x + e x G x = e x i = 0 R D n F i + 1 x + e x G x
140 24 120 45 subdid φ x e x i = 0 R D n F i + 1 x G x = e x i = 0 R D n F i + 1 x e x G x
141 137 139 140 3eqtr4d φ x e x i = 0 R D n F i + 1 x + e x G x = e x i = 0 R D n F i + 1 x G x
142 44 oveq2d φ x i = 0 R D n F i + 1 x G x = i = 0 R D n F i + 1 x i = 0 R D n F i x
143 26 119 41 fsumsub φ x i = 0 R D n F i + 1 x D n F i x = i = 0 R D n F i + 1 x i = 0 R D n F i x
144 fveq2 j = i D n F j = D n F i
145 144 fveq1d j = i D n F j x = D n F i x
146 107 fveq1d j = i + 1 D n F j x = D n F i + 1 x
147 fveq2 j = 0 D n F j = D n F 0
148 147 fveq1d j = 0 D n F j x = D n F 0 x
149 fveq2 j = R + 1 D n F j = D n F R + 1
150 149 fveq1d j = R + 1 D n F j x = D n F R + 1 x
151 8 nnnn0d φ P 0
152 34 151 nn0mulcld φ M P 0
153 nnm1nn0 P P 1 0
154 8 153 syl φ P 1 0
155 152 154 nn0addcld φ M P + P - 1 0
156 11 155 eqeltrid φ R 0
157 156 adantr φ x R 0
158 157 nn0zd φ x R
159 peano2nn0 R 0 R + 1 0
160 156 159 syl φ R + 1 0
161 nn0uz 0 = 0
162 160 161 eleqtrdi φ R + 1 0
163 162 adantr φ x R + 1 0
164 elfznn0 j 0 R + 1 j 0
165 164 115 sylan2 φ j 0 R + 1 D n F j :
166 165 adantlr φ x j 0 R + 1 D n F j :
167 simplr φ x j 0 R + 1 x
168 166 167 ffvelrnd φ x j 0 R + 1 D n F j x
169 145 146 148 150 158 163 168 telfsum2 φ x i = 0 R D n F i + 1 x D n F i x = D n F R + 1 x D n F 0 x
170 142 143 169 3eqtr2d φ x i = 0 R D n F i + 1 x G x = D n F R + 1 x D n F 0 x
171 170 oveq2d φ x e x i = 0 R D n F i + 1 x G x = e x D n F R + 1 x D n F 0 x
172 156 nn0red φ R
173 172 ltp1d φ R < R + 1
174 11 173 eqbrtrrid φ M P + P - 1 < R + 1
175 etransclem5 k 0 M y y k if k = 0 P 1 P = j 0 M x x j if j = 0 P 1 P
176 6 7 8 34 9 160 174 175 etransclem32 φ D n F R + 1 = x 0
177 176 fveq1d φ D n F R + 1 x = x 0 x
178 eqid x 0 = x 0
179 178 fvmpt2 x 0 x 0 x = 0
180 57 179 mpan2 x x 0 x = 0
181 177 180 sylan9eq φ x D n F R + 1 x = 0
182 cnex V
183 182 a1i φ V
184 6 5 ssexd φ V
185 elpm2r V V F : F 𝑝𝑚
186 183 184 50 5 185 syl22anc φ F 𝑝𝑚
187 dvn0 F 𝑝𝑚 D n F 0 = F
188 49 186 187 syl2anc φ D n F 0 = F
189 188 fveq1d φ D n F 0 x = F x
190 189 adantr φ x D n F 0 x = F x
191 181 190 oveq12d φ x D n F R + 1 x D n F 0 x = 0 F x
192 df-neg F x = 0 F x
193 191 192 eqtr4di φ x D n F R + 1 x D n F 0 x = F x
194 193 oveq2d φ x e x D n F R + 1 x D n F 0 x = e x F x
195 141 171 194 3eqtrd φ x e x i = 0 R D n F i + 1 x + e x G x = e x F x
196 132 136 195 3eqtrd φ x e x G x + i = 0 R D n F i + 1 x e x = e x F x
197 196 mpteq2dva φ x e x G x + i = 0 R D n F i + 1 x e x = x e x F x
198 24 51 mulneg2d φ x e x F x = e x F x
199 198 mpteq2dva φ x e x F x = x e x F x
200 130 197 199 3eqtrd φ dx e x G x d x = x e x F x
201 6 46 53 200 dvmptneg φ dx e x G x d x = x e x F x
202 201 adantr φ j 0 M dx e x G x d x = x e x F x
203 0red φ j 0 M 0
204 elfzelz j 0 M j
205 204 zred j 0 M j
206 205 adantl φ j 0 M j
207 203 206 iccssred φ j 0 M 0 j
208 eqid TopOpen fld = TopOpen fld
209 208 tgioo2 topGen ran . = TopOpen fld 𝑡
210 0red j 0 M 0
211 iccntr 0 j int topGen ran . 0 j = 0 j
212 210 205 211 syl2anc j 0 M int topGen ran . 0 j = 0 j
213 212 adantl φ j 0 M int topGen ran . 0 j = 0 j
214 17 48 55 202 207 209 208 213 dvmptres2 φ j 0 M dx 0 j e x G x d x = x 0 j e x F x
215 19 a1i φ x 0 j e
216 elioore x 0 j x
217 216 recnd x 0 j x
218 217 adantl φ x 0 j x
219 218 negcld φ x 0 j x
220 215 219 cxpcld φ x 0 j e x
221 50 adantr φ x 0 j F :
222 216 adantl φ x 0 j x
223 221 222 ffvelrnd φ x 0 j F x
224 220 223 mulcld φ x 0 j e x F x
225 224 negnegd φ x 0 j e x F x = e x F x
226 225 mpteq2dva φ x 0 j e x F x = x 0 j e x F x
227 226 adantr φ j 0 M x 0 j e x F x = x 0 j e x F x
228 16 214 227 3eqtrd φ j 0 M D O = x 0 j e x F x
229 228 fveq1d φ j 0 M O x = x 0 j e x F x x
230 229 adantr φ j 0 M x 0 j O x = x 0 j e x F x x
231 simpr φ x 0 j x 0 j
232 eqid x 0 j e x F x = x 0 j e x F x
233 232 fvmpt2 x 0 j e x F x x 0 j e x F x x = e x F x
234 231 224 233 syl2anc φ x 0 j x 0 j e x F x x = e x F x
235 234 adantlr φ j 0 M x 0 j x 0 j e x F x x = e x F x
236 230 235 eqtr2d φ j 0 M x 0 j e x F x = O x
237 236 itgeq2dv φ j 0 M 0 j e x F x dx = 0 j O x dx
238 elfzle1 j 0 M 0 j
239 238 adantl φ j 0 M 0 j
240 eqid x 0 j e x F x = x 0 j e x F x
241 eqidd j 0 M x 0 j y e y = y e y
242 90 adantl j 0 M x 0 j y = x e y = e x
243 210 205 iccssred j 0 M 0 j
244 ax-resscn
245 243 244 sstrdi j 0 M 0 j
246 245 sselda j 0 M x 0 j x
247 246 negcld j 0 M x 0 j x
248 19 a1i x e
249 negcl x x
250 248 249 cxpcld x e x
251 246 250 syl j 0 M x 0 j e x
252 241 242 247 251 fvmptd j 0 M x 0 j y e y x = e x
253 252 eqcomd j 0 M x 0 j e x = y e y x
254 253 adantll φ j 0 M x 0 j e x = y e y x
255 254 mpteq2dva φ j 0 M x 0 j e x = x 0 j y e y x
256 mnfxr −∞ *
257 256 a1i e + −∞ *
258 0red e + 0
259 rpxr e + e *
260 rpgt0 e + 0 < e
261 257 258 259 260 gtnelioc e + ¬ e −∞ 0
262 80 261 ax-mp ¬ e −∞ 0
263 eldif e −∞ 0 e ¬ e −∞ 0
264 19 262 263 mpbir2an e −∞ 0
265 cxpcncf2 e −∞ 0 y e y : cn
266 264 265 mp1i φ j 0 M y e y : cn
267 eqid x 0 j x = x 0 j x
268 267 negcncf 0 j x 0 j x : 0 j cn
269 245 268 syl j 0 M x 0 j x : 0 j cn
270 269 adantl φ j 0 M x 0 j x : 0 j cn
271 266 270 cncfmpt1f φ j 0 M x 0 j y e y x : 0 j cn
272 255 271 eqeltrd φ j 0 M x 0 j e x : 0 j cn
273 244 a1i φ j 0 M x 0 j
274 8 ad2antrr φ j 0 M x 0 j P
275 34 ad2antrr φ j 0 M x 0 j M 0
276 etransclem6 x x P 1 j = 1 M x j P = y y P 1 k = 1 M y k P
277 9 276 eqtri F = y y P 1 k = 1 M y k P
278 243 sselda j 0 M x 0 j x
279 278 adantll φ j 0 M x 0 j x
280 273 274 275 277 279 etransclem13 φ j 0 M x 0 j F x = k = 0 M x k if k = 0 P 1 P
281 280 mpteq2dva φ j 0 M x 0 j F x = x 0 j k = 0 M x k if k = 0 P 1 P
282 245 adantl φ j 0 M 0 j
283 fzfid φ j 0 M 0 M Fin
284 279 recnd φ j 0 M x 0 j x
285 284 3adant3 φ j 0 M x 0 j k 0 M x
286 elfzelz k 0 M k
287 286 zcnd k 0 M k
288 287 3ad2ant3 φ j 0 M x 0 j k 0 M k
289 285 288 subcld φ j 0 M x 0 j k 0 M x k
290 8 adantr φ x 0 j P
291 290 153 syl φ x 0 j P 1 0
292 151 adantr φ x 0 j P 0
293 291 292 ifcld φ x 0 j if k = 0 P 1 P 0
294 293 3adant3 φ x 0 j k 0 M if k = 0 P 1 P 0
295 294 3adant1r φ j 0 M x 0 j k 0 M if k = 0 P 1 P 0
296 289 295 expcld φ j 0 M x 0 j k 0 M x k if k = 0 P 1 P
297 nfv x φ j 0 M k 0 M
298 245 adantr j 0 M k 0 M 0 j
299 ssid
300 299 a1i j 0 M k 0 M
301 298 300 idcncfg j 0 M k 0 M x 0 j x : 0 j cn
302 287 adantl j 0 M k 0 M k
303 298 302 300 constcncfg j 0 M k 0 M x 0 j k : 0 j cn
304 301 303 subcncf j 0 M k 0 M x 0 j x k : 0 j cn
305 304 adantll φ j 0 M k 0 M x 0 j x k : 0 j cn
306 154 151 ifcld φ if k = 0 P 1 P 0
307 expcncf if k = 0 P 1 P 0 y y if k = 0 P 1 P : cn
308 306 307 syl φ y y if k = 0 P 1 P : cn
309 308 ad2antrr φ j 0 M k 0 M y y if k = 0 P 1 P : cn
310 299 a1i φ j 0 M k 0 M
311 oveq1 y = x k y if k = 0 P 1 P = x k if k = 0 P 1 P
312 297 305 309 310 311 cncfcompt2 φ j 0 M k 0 M x 0 j x k if k = 0 P 1 P : 0 j cn
313 282 283 296 312 fprodcncf φ j 0 M x 0 j k = 0 M x k if k = 0 P 1 P : 0 j cn
314 281 313 eqeltrd φ j 0 M x 0 j F x : 0 j cn
315 272 314 mulcncf φ j 0 M x 0 j e x F x : 0 j cn
316 ioossicc 0 j 0 j
317 316 a1i φ j 0 M 0 j 0 j
318 299 a1i φ j 0 M
319 224 adantlr φ j 0 M x 0 j e x F x
320 240 315 317 318 319 cncfmptssg φ j 0 M x 0 j e x F x : 0 j cn
321 228 320 eqeltrd φ j 0 M O : 0 j cn
322 7 adantr φ j 0 M TopOpen fld 𝑡
323 8 adantr φ j 0 M P
324 34 adantr φ j 0 M M 0
325 oveq2 j = k x j = x k
326 325 oveq1d j = k x j P = x k P
327 326 cbvprodv j = 1 M x j P = k = 1 M x k P
328 327 oveq2i x P 1 j = 1 M x j P = x P 1 k = 1 M x k P
329 328 mpteq2i x x P 1 j = 1 M x j P = x x P 1 k = 1 M x k P
330 9 329 eqtri F = x x P 1 k = 1 M x k P
331 17 322 323 324 330 203 206 etransclem18 φ j 0 M x 0 j e x F x 𝐿 1
332 228 331 eqeltrd φ j 0 M D O 𝐿 1
333 eqid x G x = x G x
334 6 7 8 34 9 12 etransclem43 φ G : cn
335 123 334 eqeltrd φ x G x : cn
336 335 adantr φ j 0 M x G x : cn
337 121 ad2antrr φ j 0 M x 0 j G :
338 337 279 ffvelrnd φ j 0 M x 0 j G x
339 333 336 207 318 338 cncfmptssg φ j 0 M x 0 j G x : 0 j cn
340 272 339 mulcncf φ j 0 M x 0 j e x G x : 0 j cn
341 340 negcncfg φ j 0 M x 0 j e x G x : 0 j cn
342 13 341 eqeltrid φ j 0 M O : 0 j cn
343 203 206 239 321 332 342 ftc2 φ j 0 M 0 j O x dx = O j O 0
344 negeq x = j x = j
345 344 oveq2d x = j e x = e j
346 fveq2 x = j G x = G j
347 345 346 oveq12d x = j e x G x = e j G j
348 347 negeqd x = j e x G x = e j G j
349 203 rexrd φ j 0 M 0 *
350 206 rexrd φ j 0 M j *
351 ubicc2 0 * j * 0 j j 0 j
352 349 350 239 351 syl3anc φ j 0 M j 0 j
353 19 a1i j 0 M e
354 205 recnd j 0 M j
355 354 negcld j 0 M j
356 353 355 cxpcld j 0 M e j
357 356 adantl φ j 0 M e j
358 121 adantr φ j 0 M G :
359 358 206 ffvelrnd φ j 0 M G j
360 357 359 mulcld φ j 0 M e j G j
361 360 negcld φ j 0 M e j G j
362 13 348 352 361 fvmptd3 φ j 0 M O j = e j G j
363 13 a1i φ j 0 M O = x 0 j e x G x
364 negeq x = 0 x = 0
365 364 oveq2d x = 0 e x = e 0
366 neg0 0 = 0
367 366 oveq2i e 0 = e 0
368 cxp0 e e 0 = 1
369 19 368 ax-mp e 0 = 1
370 367 369 eqtri e 0 = 1
371 365 370 eqtrdi x = 0 e x = 1
372 fveq2 x = 0 G x = G 0
373 371 372 oveq12d x = 0 e x G x = 1 G 0
374 0red φ 0
375 121 374 ffvelrnd φ G 0
376 375 mulid2d φ 1 G 0 = G 0
377 373 376 sylan9eqr φ x = 0 e x G x = G 0
378 377 negeqd φ x = 0 e x G x = G 0
379 378 adantlr φ j 0 M x = 0 e x G x = G 0
380 lbicc2 0 * j * 0 j 0 0 j
381 349 350 239 380 syl3anc φ j 0 M 0 0 j
382 375 negcld φ G 0
383 382 adantr φ j 0 M G 0
384 363 379 381 383 fvmptd φ j 0 M O 0 = G 0
385 362 384 oveq12d φ j 0 M O j O 0 = - e j G j - G 0
386 375 adantr φ j 0 M G 0
387 361 386 subnegd φ j 0 M - e j G j - G 0 = - e j G j + G 0
388 361 386 addcomd φ j 0 M - e j G j + G 0 = G 0 + e j G j
389 386 360 negsubd φ j 0 M G 0 + e j G j = G 0 e j G j
390 388 389 eqtrd φ j 0 M - e j G j + G 0 = G 0 e j G j
391 385 387 390 3eqtrd φ j 0 M O j O 0 = G 0 e j G j
392 237 343 391 3eqtrd φ j 0 M 0 j e x F x dx = G 0 e j G j
393 392 oveq2d φ j 0 M A j e j 0 j e x F x dx = A j e j G 0 e j G j
394 31 adantr φ j 0 M Q Poly
395 0zd φ j 0 M 0
396 3 coef2 Q Poly 0 A : 0
397 394 395 396 syl2anc φ j 0 M A : 0
398 elfznn0 j 0 M j 0
399 398 adantl φ j 0 M j 0
400 397 399 ffvelrnd φ j 0 M A j
401 400 zcnd φ j 0 M A j
402 353 354 cxpcld j 0 M e j
403 402 adantl φ j 0 M e j
404 401 403 mulcld φ j 0 M A j e j
405 404 386 360 subdid φ j 0 M A j e j G 0 e j G j = A j e j G 0 A j e j e j G j
406 393 405 eqtrd φ j 0 M A j e j 0 j e x F x dx = A j e j G 0 A j e j e j G j
407 406 sumeq2dv φ j = 0 M A j e j 0 j e x F x dx = j = 0 M A j e j G 0 A j e j e j G j
408 fzfid φ 0 M Fin
409 404 386 mulcld φ j 0 M A j e j G 0
410 404 360 mulcld φ j 0 M A j e j e j G j
411 408 409 410 fsumsub φ j = 0 M A j e j G 0 A j e j e j G j = j = 0 M A j e j G 0 j = 0 M A j e j e j G j
412 2 eqcomd φ 0 = Q e
413 3 4 coeid2 Q Poly e Q e = j = 0 M A j e j
414 31 19 413 sylancl φ Q e = j = 0 M A j e j
415 cxpexp e j 0 e j = e j
416 353 398 415 syl2anc j 0 M e j = e j
417 416 eqcomd j 0 M e j = e j
418 417 oveq2d j 0 M A j e j = A j e j
419 418 adantl φ j 0 M A j e j = A j e j
420 419 sumeq2dv φ j = 0 M A j e j = j = 0 M A j e j
421 412 414 420 3eqtrd φ 0 = j = 0 M A j e j
422 421 oveq1d φ 0 G 0 = j = 0 M A j e j G 0
423 375 mul02d φ 0 G 0 = 0
424 408 375 404 fsummulc1 φ j = 0 M A j e j G 0 = j = 0 M A j e j G 0
425 422 423 424 3eqtr3rd φ j = 0 M A j e j G 0 = 0
426 fveq2 x = j D n F i x = D n F i j
427 426 sumeq2sdv x = j i = 0 R D n F i x = i = 0 R D n F i j
428 fzfid φ j 0 M 0 R Fin
429 38 adantlr φ j 0 M i 0 R D n F i :
430 206 adantr φ j 0 M i 0 R j
431 429 430 ffvelrnd φ j 0 M i 0 R D n F i j
432 428 431 fsumcl φ j 0 M i = 0 R D n F i j
433 12 427 206 432 fvmptd3 φ j 0 M G j = i = 0 R D n F i j
434 433 oveq2d φ j 0 M e j G j = e j i = 0 R D n F i j
435 434 oveq2d φ j 0 M A j e j e j G j = A j e j e j i = 0 R D n F i j
436 357 432 mulcld φ j 0 M e j i = 0 R D n F i j
437 401 403 436 mulassd φ j 0 M A j e j e j i = 0 R D n F i j = A j e j e j i = 0 R D n F i j
438 369 eqcomi 1 = e 0
439 438 a1i j 0 M 1 = e 0
440 354 negidd j 0 M j + j = 0
441 440 eqcomd j 0 M 0 = j + j
442 441 oveq2d j 0 M e 0 = e j + j
443 57 58 gtneii e 0
444 443 a1i j 0 M e 0
445 353 444 354 355 cxpaddd j 0 M e j + j = e j e j
446 439 442 445 3eqtrd j 0 M 1 = e j e j
447 446 oveq1d j 0 M 1 i = 0 R D n F i j = e j e j i = 0 R D n F i j
448 447 adantl φ j 0 M 1 i = 0 R D n F i j = e j e j i = 0 R D n F i j
449 432 mulid2d φ j 0 M 1 i = 0 R D n F i j = i = 0 R D n F i j
450 403 357 432 mulassd φ j 0 M e j e j i = 0 R D n F i j = e j e j i = 0 R D n F i j
451 448 449 450 3eqtr3rd φ j 0 M e j e j i = 0 R D n F i j = i = 0 R D n F i j
452 451 oveq2d φ j 0 M A j e j e j i = 0 R D n F i j = A j i = 0 R D n F i j
453 428 401 431 fsummulc2 φ j 0 M A j i = 0 R D n F i j = i = 0 R A j D n F i j
454 452 453 eqtrd φ j 0 M A j e j e j i = 0 R D n F i j = i = 0 R A j D n F i j
455 435 437 454 3eqtrd φ j 0 M A j e j e j G j = i = 0 R A j D n F i j
456 455 sumeq2dv φ j = 0 M A j e j e j G j = j = 0 M i = 0 R A j D n F i j
457 vex j V
458 vex i V
459 457 458 op1std k = j i 1 st k = j
460 459 fveq2d k = j i A 1 st k = A j
461 457 458 op2ndd k = j i 2 nd k = i
462 461 fveq2d k = j i D n F 2 nd k = D n F i
463 462 459 fveq12d k = j i D n F 2 nd k 1 st k = D n F i j
464 460 463 oveq12d k = j i A 1 st k D n F 2 nd k 1 st k = A j D n F i j
465 fzfid φ 0 R Fin
466 401 adantrr φ j 0 M i 0 R A j
467 431 anasss φ j 0 M i 0 R D n F i j
468 466 467 mulcld φ j 0 M i 0 R A j D n F i j
469 464 408 465 468 fsumxp φ j = 0 M i = 0 R A j D n F i j = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
470 456 469 eqtrd φ j = 0 M A j e j e j G j = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
471 425 470 oveq12d φ j = 0 M A j e j G 0 j = 0 M A j e j e j G j = 0 k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
472 df-neg k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k = 0 k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
473 472 eqcomi 0 k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
474 473 a1i φ 0 k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
475 411 471 474 3eqtrd φ j = 0 M A j e j G 0 A j e j e j G j = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
476 14 407 475 3eqtrd φ L = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
477 476 oveq1d φ L P 1 ! = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !