Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem46 Structured version   Visualization version   Unicode version

Theorem etransclem46 38257
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 non-zero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem46.q  |-  ( ph  ->  Q  e.  ( (Poly `  ZZ )  \  {
0p } ) )
etransclem46.qe0  |-  ( ph  ->  ( Q `  _e )  =  0 )
etransclem46.a  |-  A  =  (coeff `  Q )
etransclem46.m  |-  M  =  (deg `  Q )
etransclem46.rex  |-  ( ph  ->  RR  C_  RR )
etransclem46.s  |-  ( ph  ->  RR  e.  { RR ,  CC } )
etransclem46.x  |-  ( ph  ->  RR  e.  ( (
TopOpen ` fld )t  RR ) )
etransclem46.p  |-  ( ph  ->  P  e.  NN )
etransclem46.f  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P ) ) )
etransclem46.l  |-  L  = 
sum_ j  e.  ( 0 ... M ) ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x )
)  _d x )
etransclem46.r  |-  R  =  ( ( M  x.  P )  +  ( P  -  1 ) )
etransclem46.g  |-  G  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
) )
etransclem46.h  |-  O  =  ( x  e.  ( 0 [,] j ) 
|->  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) )
Assertion
Ref Expression
etransclem46  |-  ( ph  ->  ( L  /  ( ! `  ( P  -  1 ) ) )  =  ( -u sum_ k  e.  ( ( 0 ... M )  X.  ( 0 ... R ) ) ( ( A `  ( 1st `  k ) )  x.  ( ( ( RR  Dn F ) `  ( 2nd `  k ) ) `  ( 1st `  k ) ) )  /  ( ! `  ( P  -  1 ) ) ) )
Distinct variable groups:    A, i,
j, k    i, F, j, k, x    j, G, x    i, M, j, k, x    x, O    P, j, k, x    Q, j    R, i, j, k, x    ph, i, j, k, x
Allowed substitution hints:    A( x)    P( i)    Q( x, i, k)    G( i, k)    L( x, i, j, k)    O( i, j, k)

Proof of Theorem etransclem46
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 etransclem46.l . . . 4  |-  L  = 
sum_ j  e.  ( 0 ... M ) ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x )
)  _d x )
21a1i 11 . . 3  |-  ( ph  ->  L  =  sum_ j  e.  ( 0 ... M
) ( ( ( A `  j )  x.  ( _e  ^c  j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x )
)  _d x ) )
3 etransclem46.h . . . . . . . . . . . . . 14  |-  O  =  ( x  e.  ( 0 [,] j ) 
|->  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) )
43oveq2i 6319 . . . . . . . . . . . . 13  |-  ( RR 
_D  O )  =  ( RR  _D  (
x  e.  ( 0 [,] j )  |->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) ) ) )
54a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  =  ( RR  _D  (
x  e.  ( 0 [,] j )  |->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) ) ) ) )
6 etransclem46.s . . . . . . . . . . . . . 14  |-  ( ph  ->  RR  e.  { RR ,  CC } )
76adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  RR  e.  { RR ,  CC } )
8 ere 14220 . . . . . . . . . . . . . . . . . . . 20  |-  _e  e.  RR
98recni 9673 . . . . . . . . . . . . . . . . . . 19  |-  _e  e.  CC
109a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  _e  e.  CC )
11 recn 9647 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  x  e.  CC )
1211negcld 9992 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  -u x  e.  CC )
1310, 12cxpcld 23732 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  (
_e  ^c  -u x
)  e.  CC )
1413adantl 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( _e 
^c  -u x
)  e.  CC )
15 simpr 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
16 fzfid 12224 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( 0 ... R )  e. 
Fin )
17 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... R )  ->  i  e.  NN0 )
186adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  RR  e.  { RR ,  CC }
)
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  RR  e.  ( (
TopOpen ` fld )t  RR ) )
2019adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  RR  e.  ( ( TopOpen ` fld )t  RR ) )
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  e.  NN )
2221adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  P  e.  NN )
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  =  (deg `  Q )
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  Q  e.  ( (Poly `  ZZ )  \  {
0p } ) )
2524eldifad 3402 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  Q  e.  (Poly `  ZZ ) )
26 dgrcl 23266 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Q  e.  (Poly `  ZZ )  ->  (deg `  Q
)  e.  NN0 )
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  (deg `  Q )  e.  NN0 )
2823, 27syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  NN0 )
2928adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  M  e.  NN0 )
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P ) ) )
31 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  i  e.  NN0 )
3218, 20, 22, 29, 30, 31etransclem33 38244 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  NN0 )  ->  ( ( RR  Dn F ) `
 i ) : RR --> CC )
3317, 32sylan2 482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
3433adantlr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
35 simplr 770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  x  e.  RR )
3634, 35ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  i ) `  x
)  e.  CC )
3716, 36fsumcl 13876 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 x )  e.  CC )
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19  |-  G  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
) )
3938fvmpt2 5972 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  RR  /\  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
)  e.  CC )  ->  ( G `  x )  =  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
) )
4015, 37, 39syl2anc 673 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( G `
 x )  = 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  x ) )
4140, 37eqeltrd 2549 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( G `
 x )  e.  CC )
4214, 41mulcld 9681 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
4342negcld 9992 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
4443adantlr 729 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
456, 19dvdmsscn 37908 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  C_  CC )
4645, 21, 30etransclem8 38219 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : RR --> CC )
4746ffvelrnda 6037 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  CC )
4814, 47mulcld 9681 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
4948negcld 9992 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
5049negcld 9992 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  -u -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
5150adantlr 729 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  RR )  ->  -u -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
528a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  _e  e.  RR )
53 0re 9661 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
54 epos 14336 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  _e
5553, 8, 54ltleii 9775 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  _e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  0  <_  _e )
57 renegcl 9957 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  -u x  e.  RR )
5852, 56, 57recxpcld 23747 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
_e  ^c  -u x
)  e.  RR )
5958renegcld 10067 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  -u (
_e  ^c  -u x
)  e.  RR )
6059adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
_e  ^c  -u x
)  e.  RR )
61 reelprrecn 9649 . . . . . . . . . . . . . . . . . . . . . 22  |-  RR  e.  { RR ,  CC }
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  RR  e.  { RR ,  CC } )
63 cnelprrecn 9650 . . . . . . . . . . . . . . . . . . . . . 22  |-  CC  e.  { RR ,  CC }
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  CC  e.  { RR ,  CC } )
6512adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  RR )  ->  -u x  e.  CC )
66 neg1rr 10736 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u 1  e.  RR
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  RR )  ->  -u 1  e.  RR )
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  CC  ->  _e  e.  CC )
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  CC  ->  y  e.  CC )
7068, 69cxpcld 23732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  (
_e  ^c  y )  e.  CC )
7170adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  y  e.  CC )  ->  (
_e  ^c  y )  e.  CC )
7211adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  x  e.  CC )
73 1red 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  1  e.  RR )
7462dvmptid 22990 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
7562, 72, 73, 74dvmptneg 22999 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  -u x ) )  =  ( x  e.  RR  |->  -u 1 ) )
76 epr 14337 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  _e  e.  RR+
77 dvcxp2 23760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( _e  e.  RR+  ->  ( CC 
_D  ( y  e.  CC  |->  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( ( log `  _e )  x.  ( _e  ^c  y ) ) ) )
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( CC 
_D  ( y  e.  CC  |->  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( ( log `  _e )  x.  ( _e  ^c  y ) ) )
79 loge 23615 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( log `  _e )  =  1
8079oveq1i 6318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( log `  _e )  x.  ( _e  ^c  y ) )  =  ( 1  x.  ( _e  ^c 
y ) )
8170mulid2d 9679 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  CC  ->  (
1  x.  ( _e 
^c  y ) )  =  ( _e 
^c  y ) )
8280, 81syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  CC  ->  (
( log `  _e )  x.  ( _e  ^c  y ) )  =  ( _e  ^c  y ) )
8382mpteq2ia 4478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  CC  |->  ( ( log `  _e )  x.  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( _e 
^c  y ) )
8478, 83eqtri 2493 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( CC 
_D  ( y  e.  CC  |->  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( _e 
^c  y ) )
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( CC  _D  (
y  e.  CC  |->  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( _e  ^c 
y ) ) )
86 oveq2 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  -u x  ->  (
_e  ^c  y )  =  ( _e  ^c  -u x ) )
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 23005 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  ( _e  ^c  -u x ) ) )  =  ( x  e.  RR  |->  ( ( _e 
^c  -u x
)  x.  -u 1
) ) )
8887trud 1461 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
_D  ( x  e.  RR  |->  ( _e  ^c  -u x ) ) )  =  ( x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  -u 1
) )
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  -u 1  e.  RR )
9089recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  -u 1  e.  CC )
9113, 90mulcomd 9682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  (
( _e  ^c  -u x )  x.  -u 1
)  =  ( -u
1  x.  ( _e 
^c  -u x
) ) )
9213mulm1d 10091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  ( -u 1  x.  ( _e 
^c  -u x
) )  =  -u ( _e  ^c  -u x ) )
9391, 92eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  (
( _e  ^c  -u x )  x.  -u 1
)  =  -u (
_e  ^c  -u x
) )
9493mpteq2ia 4478 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  -u 1
) )  =  ( x  e.  RR  |->  -u ( _e  ^c  -u x ) )
9588, 94eqtri 2493 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
_D  ( x  e.  RR  |->  ( _e  ^c  -u x ) ) )  =  ( x  e.  RR  |->  -u (
_e  ^c  -u x
) )
9695a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( _e  ^c  -u x ) ) )  =  ( x  e.  RR  |->  -u ( _e  ^c  -u x ) ) )
9717adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  i  e.  NN0 )
98 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
i  +  1 )  e.  NN0 )
100 ovex 6336 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  +  1 )  e. 
_V
101 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  ( i  +  1 )  ->  (
j  e.  NN0  <->  ( i  +  1 )  e. 
NN0 ) )
102101anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( i  +  1 )  ->  (
( ph  /\  j  e.  NN0 )  <->  ( ph  /\  ( i  +  1 )  e.  NN0 )
) )
103 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  ( i  +  1 )  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  ( i  +  1 ) ) )
104103feq1d 5724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( i  +  1 )  ->  (
( ( RR  Dn F ) `  j ) : RR --> CC 
<->  ( ( RR  Dn F ) `  ( i  +  1 ) ) : RR --> CC ) )
105102, 104imbi12d 327 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( i  +  1 )  ->  (
( ( ph  /\  j  e.  NN0 )  -> 
( ( RR  Dn F ) `  j ) : RR --> CC )  <->  ( ( ph  /\  ( i  +  1 )  e.  NN0 )  ->  ( ( RR  Dn F ) `  ( i  +  1 ) ) : RR --> CC ) ) )
106 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  j  ->  (
i  e.  NN0  <->  j  e.  NN0 ) )
107106anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  j  ->  (
( ph  /\  i  e.  NN0 )  <->  ( ph  /\  j  e.  NN0 )
) )
108 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  j  ->  (
( RR  Dn
F ) `  i
)  =  ( ( RR  Dn F ) `  j ) )
109108feq1d 5724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  j  ->  (
( ( RR  Dn F ) `  i ) : RR --> CC 
<->  ( ( RR  Dn F ) `  j ) : RR --> CC ) )
110107, 109imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  NN0 )  -> 
( ( RR  Dn F ) `  i ) : RR --> CC )  <->  ( ( ph  /\  j  e.  NN0 )  ->  ( ( RR  Dn F ) `  j ) : RR --> CC ) ) )
111110, 32chvarv 2120 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( RR  Dn F ) `
 j ) : RR --> CC )
112100, 105, 111vtocl 3086 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( i  +  1 )  e. 
NN0 )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
11399, 112syldan 478 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
114113adantlr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
115114, 35ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  e.  CC )
11616, 115fsumcl 13876 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  e.  CC )
11721, 28, 30, 38etransclem39 38250 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G : RR --> CC )
118117feqmptd 5932 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  G  =  ( x  e.  RR  |->  ( G `
 x ) ) )
119118eqcomd 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  ( G `  x ) )  =  G )
120119oveq2d 6324 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( G `  x ) ) )  =  ( RR  _D  G ) )
121 nfcv 2612 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x F
122 elfznn0 11913 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 0 ... ( R  +  1 ) )  ->  i  e.  NN0 )
123122, 32sylan2 482 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
124121, 46, 123, 38etransclem2 38213 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  G
)  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) ) )
125120, 124eqtrd 2505 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( G `  x ) ) )  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) ) )
1266, 14, 60, 96, 41, 116, 125dvmptmul 22994 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  ( G `  x )
) ) )  =  ( x  e.  RR  |->  ( ( -u (
_e  ^c  -u x
)  x.  ( G `
 x ) )  +  ( sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  x.  ( _e  ^c  -u x ) ) ) ) )
127116, 14mulcomd 9682 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  x.  ( _e 
^c  -u x
) )  =  ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) ) )
128127oveq2d 6324 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( _e  ^c  -u x )  x.  ( G `  x
) )  +  (
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 ( i  +  1 ) ) `  x )  x.  (
_e  ^c  -u x
) ) )  =  ( ( -u (
_e  ^c  -u x
)  x.  ( G `
 x ) )  +  ( ( _e 
^c  -u x
)  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) ) ) )
12914negcld 9992 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
_e  ^c  -u x
)  e.  CC )
130129, 41mulcld 9681 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( -u ( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
13114, 116mulcld 9681 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  e.  CC )
132130, 131addcomd 9853 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( _e  ^c  -u x )  x.  ( G `  x
) )  +  ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) ) )  =  ( ( ( _e 
^c  -u x
)  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) )  +  ( -u (
_e  ^c  -u x
)  x.  ( G `
 x ) ) ) )
133131, 42negsubd 10011 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  +  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) ) )  =  ( ( ( _e 
^c  -u x
)  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) )  -  ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) ) )
13414, 41mulneg1d 10092 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( -u ( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u (
( _e  ^c  -u x )  x.  ( G `  x )
) )
135134oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  +  (
-u ( _e  ^c  -u x )  x.  ( G `  x
) ) )  =  ( ( ( _e 
^c  -u x
)  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) )  +  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) ) )
136116, 41, 14subdir2d 37617 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  -  ( G `
 x ) ) )  =  ( ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  -  (
( _e  ^c  -u x )  x.  ( G `  x )
) ) )
137133, 135, 1363eqtr4d 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  +  (
-u ( _e  ^c  -u x )  x.  ( G `  x
) ) )  =  ( ( _e  ^c  -u x )  x.  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 ( i  +  1 ) ) `  x )  -  ( G `  x )
) ) )
13840oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  -  ( G `
 x ) )  =  ( sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  -  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
) ) )
13916, 115, 36fsumsub 13926 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( ( RR  Dn
F ) `  (
i  +  1 ) ) `  x )  -  ( ( ( RR  Dn F ) `  i ) `
 x ) )  =  ( sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  -  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
) ) )
140 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  i  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  i ) )
141140fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  i  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  i
) `  x )
)
142103fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( i  +  1 )  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  (
i  +  1 ) ) `  x ) )
143 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  0 ) )
144143fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  0
) `  x )
)
145 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( R  + 
1 )  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  ( R  +  1 ) ) )
146145fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( R  + 
1 )  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  ( R  +  1 ) ) `  x ) )
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  R  =  ( ( M  x.  P )  +  ( P  -  1 ) )
14821nnnn0d 10949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  P  e.  NN0 )
14928, 148nn0mulcld 10954 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( M  x.  P
)  e.  NN0 )
150 nnm1nn0 10935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
152149, 151nn0addcld 10953 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( M  x.  P )  +  ( P  -  1 ) )  e.  NN0 )
153147, 152syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  R  e.  NN0 )
154153adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  R  e. 
NN0 )
155154nn0zd 11061 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  R  e.  ZZ )
156 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( R  e.  NN0  ->  ( R  +  1 )  e. 
NN0 )
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( R  +  1 )  e.  NN0 )
158 nn0uz 11217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  =  ( ZZ>= `  0 )
159157, 158syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( R  +  1 )  e.  ( ZZ>= ` 
0 ) )
160159adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( R  +  1 )  e.  ( ZZ>= `  0 )
)
161 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  e.  ( 0 ... ( R  +  1 ) )  ->  j  e.  NN0 )
162161, 111sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  j
) : RR --> CC )
163162adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  j
) : RR --> CC )
164 simplr 770 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  x  e.  RR )
165163, 164ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( ( RR  Dn F ) `  j ) `  x
)  e.  CC )
166141, 142, 144, 146, 155, 160, 165telfsum2 13942 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( ( RR  Dn
F ) `  (
i  +  1 ) ) `  x )  -  ( ( ( RR  Dn F ) `  i ) `
 x ) )  =  ( ( ( ( RR  Dn
F ) `  ( R  +  1 ) ) `  x )  -  ( ( ( RR  Dn F ) `  0 ) `
 x ) ) )
167138, 139, 1663eqtr2d 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  -  ( G `
 x ) )  =  ( ( ( ( RR  Dn
F ) `  ( R  +  1 ) ) `  x )  -  ( ( ( RR  Dn F ) `  0 ) `
 x ) ) )
168167oveq2d 6324 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  -  ( G `
 x ) ) )  =  ( ( _e  ^c  -u x )  x.  (
( ( ( RR  Dn F ) `
 ( R  + 
1 ) ) `  x )  -  (
( ( RR  Dn F ) ` 
0 ) `  x
) ) ) )
169153nn0red 10950 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  R  e.  RR )
170169ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  R  <  ( R  +  1 ) )
171147, 170syl5eqbrr 4430 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( M  x.  P )  +  ( P  -  1 ) )  <  ( R  +  1 ) )
172 etransclem5 38216 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( 0 ... M )  |->  ( y  e.  RR  |->  ( ( y  -  k ) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) ) )  =  ( j  e.  ( 0 ... M )  |->  ( x  e.  RR  |->  ( ( x  -  j
) ^ if ( j  =  0 ,  ( P  -  1 ) ,  P ) ) ) )
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 38243 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  Dn F ) `  ( R  +  1
) )  =  ( x  e.  RR  |->  0 ) )
174173fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 ( R  + 
1 ) ) `  x )  =  ( ( x  e.  RR  |->  0 ) `  x
) )
175 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  |->  0 )  =  ( x  e.  RR  |->  0 )
176175fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  0  e.  RR )  ->  ( ( x  e.  RR  |->  0 ) `  x )  =  0 )
17753, 176mpan2 685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( x  e.  RR  |->  0 ) `  x
)  =  0 )
178174, 177sylan9eq 2525 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( RR  Dn
F ) `  ( R  +  1 ) ) `  x )  =  0 )
179 cnex 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  CC  e.  _V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  CC  e.  _V )
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  RR  C_  RR )
1826, 181ssexd 4543 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  RR  e.  _V )
183 elpm2r 7507 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( CC  e.  _V  /\  RR  e.  _V )  /\  ( F : RR --> CC  /\  RR  C_  RR ) )  ->  F  e.  ( CC  ^pm  RR ) )
184180, 182, 46, 181, 183syl22anc 1293 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
185 dvn0 22957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  C_  CC  /\  F  e.  ( CC  ^pm  RR ) )  ->  (
( RR  Dn
F ) `  0
)  =  F )
18645, 184, 185syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  Dn F ) ` 
0 )  =  F )
187186fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 0 ) `  x )  =  ( F `  x ) )
188187adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( RR  Dn
F ) `  0
) `  x )  =  ( F `  x ) )
189178, 188oveq12d 6326 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( ( RR  Dn F ) `  ( R  +  1
) ) `  x
)  -  ( ( ( RR  Dn
F ) `  0
) `  x )
)  =  ( 0  -  ( F `  x ) ) )
190 df-neg 9883 . . . . . . . . . . . . . . . . . . . . 21  |-  -u ( F `  x )  =  ( 0  -  ( F `  x
) )
191189, 190syl6eqr 2523 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( ( RR  Dn F ) `  ( R  +  1
) ) `  x
)  -  ( ( ( RR  Dn
F ) `  0
) `  x )
)  =  -u ( F `  x )
)
192191oveq2d 6324 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  (
( ( ( RR  Dn F ) `
 ( R  + 
1 ) ) `  x )  -  (
( ( RR  Dn F ) ` 
0 ) `  x
) ) )  =  ( ( _e  ^c  -u x )  x.  -u ( F `  x
) ) )
193137, 168, 1923eqtrd 2509 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( _e  ^c  -u x )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
) )  +  (
-u ( _e  ^c  -u x )  x.  ( G `  x
) ) )  =  ( ( _e  ^c  -u x )  x.  -u ( F `  x
) ) )
194128, 132, 1933eqtrd 2509 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( _e  ^c  -u x )  x.  ( G `  x
) )  +  (
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 ( i  +  1 ) ) `  x )  x.  (
_e  ^c  -u x
) ) )  =  ( ( _e  ^c  -u x )  x.  -u ( F `  x
) ) )
195194mpteq2dva 4482 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  RR  |->  ( ( -u (
_e  ^c  -u x
)  x.  ( G `
 x ) )  +  ( sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  x.  ( _e  ^c  -u x ) ) ) )  =  ( x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  -u ( F `  x )
) ) )
19614, 47mulneg2d 10093 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  -u ( F `  x )
)  =  -u (
( _e  ^c  -u x )  x.  ( F `  x )
) )
197196mpteq2dva 4482 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  -u ( F `  x
) ) )  =  ( x  e.  RR  |->  -u ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
198126, 195, 1973eqtrd 2509 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  ( G `  x )
) ) )  =  ( x  e.  RR  |->  -u ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
1996, 42, 49, 198dvmptneg 22999 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) ) ) )  =  ( x  e.  RR  |->  -u -u ( ( _e 
^c  -u x
)  x.  ( F `
 x ) ) ) )
200199adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  ( x  e.  RR  |->  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) ) )  =  ( x  e.  RR  |->  -u -u ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
201 0red 9662 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  RR )
202 elfzelz 11826 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
203202zred 11063 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
204203adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  RR )
205201, 204iccssred 37698 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 [,] j ) 
C_  RR )
206 eqid 2471 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
207206tgioo2 21899 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
208 0red 9662 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  0  e.  RR )
209 iccntr 21917 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  j  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
210208, 203, 209syl2anc 673 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
211210adantl 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 22995 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  ( x  e.  ( 0 [,] j
)  |->  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) ) )  =  ( x  e.  ( 0 (,) j )  |->  -u -u ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
2139a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  _e  e.  CC )
214 elioore 11691 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 0 (,) j )  ->  x  e.  RR )
215214recnd 9687 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( 0 (,) j )  ->  x  e.  CC )
216215adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  CC )
217216negcld 9992 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  -u x  e.  CC )
218213, 217cxpcld 23732 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  (
_e  ^c  -u x
)  e.  CC )
21946adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  F : RR --> CC )
220214adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  RR )
221219, 220ffvelrnd 6038 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  ( F `  x )  e.  CC )
222218, 221mulcld 9681 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
223222negnegd 9996 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  -u -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  =  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
224223mpteq2dva 4482 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  ( 0 (,) j ) 
|->  -u -u ( ( _e 
^c  -u x
)  x.  ( F `
 x ) ) )  =  ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) ) )
225224adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 (,) j )  |->  -u -u ( ( _e  ^c  -u x )  x.  ( F `  x
) ) )  =  ( x  e.  ( 0 (,) j ) 
|->  ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
2265, 212, 2253eqtrd 2509 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  =  ( x  e.  ( 0 (,) j ) 
|->  ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
227226fveq1d 5881 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( RR  _D  O
) `  x )  =  ( ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) ) `  x
) )
228227adantr 472 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( RR  _D  O
) `  x )  =  ( ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) ) `  x
) )
229 simpr 468 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  ( 0 (,) j
) )
230 eqid 2471 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  =  ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
231230fvmpt2 5972 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 (,) j )  /\  ( ( _e  ^c  -u x )  x.  ( F `  x
) )  e.  CC )  ->  ( ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) ) `  x
)  =  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
232229, 222, 231syl2anc 673 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  (
( x  e.  ( 0 (,) j ) 
|->  ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) `  x )  =  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
233232adantlr 729 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( x  e.  ( 0 (,) j ) 
|->  ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) `  x )  =  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
234228, 233eqtr2d 2506 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  =  ( ( RR  _D  O ) `
 x ) )
235234itgeq2d 37957 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  S. ( 0 (,) j
) ( ( _e 
^c  -u x
)  x.  ( F `
 x ) )  _d x  =  S. ( 0 (,) j
) ( ( RR 
_D  O ) `  x )  _d x )
236 elfzle1 11828 . . . . . . . . 9  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
237236adantl 473 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  <_  j )
238 eqid 2471 . . . . . . . . . 10  |-  ( x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  =  ( x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
239 eqidd 2472 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( y  e.  CC  |->  ( _e  ^c  y ) )  =  ( y  e.  CC  |->  ( _e  ^c  y ) ) )
24086adantl 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  /\  y  = 
-u x )  -> 
( _e  ^c 
y )  =  ( _e  ^c  -u x ) )
241208, 203iccssred 37698 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  (
0 [,] j ) 
C_  RR )
242 ax-resscn 9614 . . . . . . . . . . . . . . . . . . 19  |-  RR  C_  CC
243241, 242syl6ss 3430 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
0 [,] j ) 
C_  CC )
244243sselda 3418 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  x  e.  CC )
245244negcld 9992 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  -u x  e.  CC )
2469a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  ->  _e  e.  CC )
247 negcl 9895 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  ->  -u x  e.  CC )
248246, 247cxpcld 23732 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  CC  ->  (
_e  ^c  -u x
)  e.  CC )
249244, 248syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( _e  ^c  -u x )  e.  CC )
250239, 240, 245, 249fvmptd 5969 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( ( y  e.  CC  |->  ( _e 
^c  y ) ) `  -u x
)  =  ( _e 
^c  -u x
) )
251250eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( _e  ^c  -u x )  =  ( ( y  e.  CC  |->  ( _e  ^c  y ) ) `
 -u x ) )
252251adantll 728 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  (
_e  ^c  -u x
)  =  ( ( y  e.  CC  |->  ( _e  ^c  y ) ) `  -u x
) )
253252mpteq2dva 4482 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( _e  ^c  -u x ) )  =  ( x  e.  ( 0 [,] j ) 
|->  ( ( y  e.  CC  |->  ( _e  ^c  y ) ) `
 -u x ) ) )
254 mnfxr 11437 . . . . . . . . . . . . . . . . . 18  |- -oo  e.  RR*
255254a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  -> -oo  e.  RR* )
256 0red 9662 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  0  e.  RR )
257 rpxr 11332 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  _e  e.  RR* )
258 rpgt0 11336 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  0  < 
_e )
259255, 256, 257, 258gtnelioc 37683 . . . . . . . . . . . . . . . 16  |-  ( _e  e.  RR+  ->  -.  _e  e.  ( -oo (,] 0
) )
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15  |-  -.  _e  e.  ( -oo (,] 0
)
261 eldif 3400 . . . . . . . . . . . . . . 15  |-  ( _e  e.  ( CC  \ 
( -oo (,] 0 ) )  <->  ( _e  e.  CC  /\  -.  _e  e.  ( -oo (,] 0 ) ) )
2629, 260, 261mpbir2an 934 . . . . . . . . . . . . . 14  |-  _e  e.  ( CC  \  ( -oo (,] 0 ) )
263 cxpcncf2 37875 . . . . . . . . . . . . . 14  |-  ( _e  e.  ( CC  \ 
( -oo (,] 0 ) )  ->  ( y  e.  CC  |->  ( _e  ^c  y ) )  e.  ( CC -cn-> CC ) )
264262, 263mp1i 13 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
y  e.  CC  |->  ( _e  ^c  y ) )  e.  ( CC -cn-> CC ) )
265 eqid 2471 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0 [,] j )  |->  -u x
)  =  ( x  e.  ( 0 [,] j )  |->  -u x
)
266265negcncf 22028 . . . . . . . . . . . . . . 15  |-  ( ( 0 [,] j ) 
C_  CC  ->  ( x  e.  ( 0 [,] j )  |->  -u x
)  e.  ( ( 0 [,] j )
-cn-> CC ) )
267243, 266syl 17 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
x  e.  ( 0 [,] j )  |->  -u x )  e.  ( ( 0 [,] j
) -cn-> CC ) )
268267adantl 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  -u x )  e.  ( ( 0 [,] j
) -cn-> CC ) )
269264, 268cncfmpt1f 22023 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( y  e.  CC  |->  ( _e  ^c 
y ) ) `  -u x ) )  e.  ( ( 0 [,] j ) -cn-> CC ) )
270253, 269eqeltrd 2549 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( _e  ^c  -u x ) )  e.  ( ( 0 [,] j ) -cn-> CC ) )
271242a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  RR  C_  CC )
27221ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN )
27328ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  M  e.  NN0 )
274 etransclem6 38217 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  |->  ( ( x ^ ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P
) ) )  =  ( y  e.  RR  |->  ( ( y ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( y  -  k ) ^ P ) ) )
27530, 274eqtri 2493 . . . . . . . . . . . . . 14  |-  F  =  ( y  e.  RR  |->  ( ( y ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( y  -  k ) ^ P ) ) )
276241sselda 3418 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  x  e.  RR )
277276adantll 728 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  x  e.  RR )
278271, 272, 273, 275, 277etransclem13 38224 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  ( F `  x )  =  prod_ k  e.  ( 0 ... M ) ( ( x  -  k ) ^ if ( k  =  0 ,  ( P  - 
1 ) ,  P
) ) )
279278mpteq2dva 4482 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( F `  x ) )  =  ( x  e.  ( 0 [,] j )  |->  prod_ k  e.  ( 0 ... M
) ( ( x  -  k ) ^ if ( k  =  0 ,  ( P  - 
1 ) ,  P
) ) ) )
280243adantl 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 [,] j ) 
C_  CC )
281 fzfid 12224 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 ... M )  e. 
Fin )
282277recnd 9687 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  x  e.  CC )
2832823adant3 1050 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  x  e.  CC )
284 elfzelz 11826 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... M )  ->  k  e.  ZZ )
285284zcnd 11064 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... M )  ->  k  e.  CC )
2862853ad2ant3 1053 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  k  e.  CC )
287283, 286subcld 10005 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  (
x  -  k )  e.  CC )
28821adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN )
289288, 150syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  ( P  -  1 )  e.  NN0 )
290148adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN0 )
291289, 290ifcld 3915 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
2922913adant3 1050 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
2932923adant1r 1285 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
294287, 293expcld 12454 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  (
( x  -  k
) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) )  e.  CC )
295 nfv 1769 . . . . . . . . . . . . . 14  |-  F/ x
( ( ph  /\  j  e.  ( 0 ... M ) )  /\  k  e.  ( 0 ... M ) )
296243adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( 0 [,] j )  C_  CC )
297 ssid 3437 . . . . . . . . . . . . . . . . . 18  |-  CC  C_  CC
298297a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  CC  C_  CC )
299296, 298idcncfg 37846 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  x )  e.  ( ( 0 [,] j ) -cn-> CC ) )
300285adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  CC )
301296, 300, 298constcncfg 37845 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  k )  e.  ( ( 0 [,] j ) -cn-> CC ) )
302299, 301subcncf 37843 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  ( x  -  k ) )  e.  ( ( 0 [,] j ) -cn-> CC ) )
303302adantll 728 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  k  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( x  -  k ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
304151, 148ifcld 3915 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( k  =  0 ,  ( P  -  1 ) ,  P )  e.  NN0 )
305 expcncf 22032 . . . . . . . . . . . . . . . 16  |-  ( if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0  ->  ( y  e.  CC  |->  ( y ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )  e.  ( CC -cn-> CC ) )
306304, 305syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  CC  |->  ( y ^ if ( k  =  0 ,  ( P  - 
1 ) ,  P
) ) )  e.  ( CC -cn-> CC ) )
307306ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  k  e.  ( 0 ... M
) )  ->  (
y  e.  CC  |->  ( y ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )  e.  ( CC -cn-> CC ) )
308297a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  k  e.  ( 0 ... M
) )  ->  CC  C_  CC )
309 oveq1 6315 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  k )  ->  (
y ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) )  =  ( ( x  -  k ) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )
310295, 303, 307, 308, 309cncfcompt2 37874 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  k  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( x  -  k
) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
311280, 281, 294, 310fprodcncf 37876 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  prod_
k  e.  ( 0 ... M ) ( ( x  -  k
) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
312279, 311eqeltrd 2549 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( F `  x ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
313270, 312mulcncf 22476 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
314 ioossicc 11745 . . . . . . . . . . 11  |-  ( 0 (,) j )  C_  ( 0 [,] j
)
315314a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 (,) j ) 
C_  ( 0 [,] j ) )
316297a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  CC  C_  CC )
317222adantlr 729 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
318238, 313, 315, 316, 317cncfmptssg 37844 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  ( ( 0 (,) j
) -cn-> CC ) )
319226, 318eqeltrd 2549 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  e.  ( ( 0 (,) j ) -cn-> CC ) )
32019adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  RR  e.  ( ( TopOpen ` fld )t  RR ) )
32121adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  P  e.  NN )
32228adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  M  e.  NN0 )
323 oveq2 6316 . . . . . . . . . . . . . . 15  |-  ( j  =  k  ->  (
x  -  j )  =  ( x  -  k ) )
324323oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  (
( x  -  j
) ^ P )  =  ( ( x  -  k ) ^ P ) )
325324cbvprodv 14047 . . . . . . . . . . . . 13  |-  prod_ j  e.  ( 1 ... M
) ( ( x  -  j ) ^ P )  =  prod_ k  e.  ( 1 ... M ) ( ( x  -  k ) ^ P )
326325oveq2i 6319 . . . . . . . . . . . 12  |-  ( ( x ^ ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P
) )  =  ( ( x ^ ( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M
) ( ( x  -  k ) ^ P ) )
327326mpteq2i 4479 . . . . . . . . . . 11  |-  ( x  e.  RR  |->  ( ( x ^ ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P
) ) )  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( x  -  k ) ^ P ) ) )
32830, 327eqtri 2493 . . . . . . . . . 10  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( x  -  k ) ^ P ) ) )
3297, 320, 321, 322, 328, 201, 204etransclem18 38229 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  L^1 )
330226, 329eqeltrd 2549 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  e.  L^1 )
331 eqid 2471 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  ( G `
 x ) )  =  ( x  e.  RR  |->  ( G `  x ) )
3326, 19, 21, 28, 30, 38etransclem43 38254 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  e.  ( RR
-cn-> CC ) )
333119, 332eqeltrd 2549 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  RR  |->  ( G `  x ) )  e.  ( RR
-cn-> CC ) )
334333adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  RR  |->  ( G `  x ) )  e.  ( RR
-cn-> CC ) )
335117ad2antrr 740 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  G : RR --> CC )
336335, 277ffvelrnd 6038 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  ( G `  x )  e.  CC )
337331, 334, 205, 316, 336cncfmptssg 37844 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( G `  x ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
338270, 337mulcncf 22476 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( G `  x )
) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
339338negcncfg 37855 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) ) )  e.  ( ( 0 [,] j ) -cn-> CC ) )
3403, 339syl5eqel 2553 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  O  e.  ( ( 0 [,] j ) -cn-> CC ) )
341201, 204, 237, 319, 330, 340ftc2 23075 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  S. ( 0 (,) j
) ( ( RR 
_D  O ) `  x )  _d x  =  ( ( O `
 j )  -  ( O `  0 ) ) )
3423a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  O  =  ( x  e.  ( 0 [,] j
)  |->  -u ( ( _e 
^c  -u x
)  x.  ( G `
 x ) ) ) )
343 negeq 9887 . . . . . . . . . . . . . 14  |-  ( x  =  j  ->  -u x  =  -u j )
344343oveq2d 6324 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  (
_e  ^c  -u x
)  =  ( _e 
^c  -u j
) )
345 fveq2 5879 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  ( G `  x )  =  ( G `  j ) )
346344, 345oveq12d 6326 . . . . . . . . . . . 12  |-  ( x  =  j  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( ( _e  ^c  -u j )  x.  ( G `  j )
) )
347346negeqd 9889 . . . . . . . . . . 11  |-  ( x  =  j  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u (
( _e  ^c  -u j )  x.  ( G `  j )
) )
348347adantl 473 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  =  j )  ->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) )  =  -u ( ( _e  ^c  -u j )  x.  ( G `  j
) ) )
349201rexrd 9708 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  RR* )
350204rexrd 9708 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  RR* )
351 ubicc2 11775 . . . . . . . . . . 11  |-  ( ( 0  e.  RR*  /\  j  e.  RR*  /\  0  <_ 
j )  ->  j  e.  ( 0 [,] j
) )
352349, 350, 237, 351syl3anc 1292 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  ( 0 [,] j
) )
3539a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  _e  e.  CC )
354203recnd 9687 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
355354negcld 9992 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  -u j  e.  CC )
356353, 355cxpcld 23732 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  -u j
)  e.  CC )
357356adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
_e  ^c  -u j
)  e.  CC )
358117adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  G : RR --> CC )
359358, 204ffvelrnd 6038 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  j )  e.  CC )
360357, 359mulcld 9681 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( _e  ^c  -u j )  x.  ( G `  j )
)  e.  CC )
361360negcld 9992 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  -u (
( _e  ^c  -u j )  x.  ( G `  j )
)  e.  CC )
362342, 348, 352, 361fvmptd 5969 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( O `  j )  =  -u ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) )
363 negeq 9887 . . . . . . . . . . . . . . . 16  |-  ( x  =  0  ->  -u x  =  -u 0 )
364363oveq2d 6324 . . . . . . . . . . . . . . 15  |-  ( x  =  0  ->  (
_e  ^c  -u x
)  =  ( _e 
^c  -u 0
) )
365 neg0 9940 . . . . . . . . . . . . . . . . 17  |-  -u 0  =  0
366365oveq2i 6319 . . . . . . . . . . . . . . . 16  |-  ( _e 
^c  -u 0
)  =  ( _e 
^c  0 )
367 cxp0 23694 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  CC  ->  (
_e  ^c  0 )  =  1 )
3689, 367ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( _e 
^c  0 )  =  1
369366, 368eqtri 2493 . . . . . . . . . . . . . . 15  |-  ( _e 
^c  -u 0
)  =  1
370364, 369syl6eq 2521 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  (
_e  ^c  -u x
)  =  1 )
371 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  ( G `  x )  =  ( G ` 
0 ) )
372370, 371oveq12d 6326 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( 1  x.  ( G ` 
0 ) ) )
373 0red 9662 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  RR )
374117, 373ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  0
)  e.  CC )
375374mulid2d 9679 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  x.  ( G `  0 )
)  =  ( G `
 0 ) )
376372, 375sylan9eqr 2527 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  = 
0 )  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( G `
 0 ) )
377376negeqd 9889 . . . . . . . . . . 11  |-  ( (
ph  /\  x  = 
0 )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u ( G `  0 )
)
378377adantlr 729 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  =  0 )  ->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) )  =  -u ( G `  0 ) )
379 lbicc2 11774 . . . . . . . . . . 11  |-  ( ( 0  e.  RR*  /\  j  e.  RR*  /\  0  <_ 
j )  ->  0  e.  ( 0 [,] j
) )
380349, 350, 237, 379syl3anc 1292 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  ( 0 [,] j
) )
381374negcld 9992 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( G ` 
0 )  e.  CC )
382381adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  -u ( G `  0 )  e.  CC )
383342, 378, 380, 382fvmptd 5969 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( O `  0 )  =  -u ( G ` 
0 ) )
384362, 383oveq12d 6326 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( O `  j
)  -  ( O `
 0 ) )  =  ( -u (
( _e  ^c  -u j )  x.  ( G `  j )
)  -  -u ( G `  0 )
) )
385374adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  0 )  e.  CC )
386361, 385subnegd 10012 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( -u ( ( _e  ^c  -u j )  x.  ( G `  j
) )  -  -u ( G `  0 )
)  =  ( -u ( ( _e  ^c  -u j )  x.  ( G `  j
) )  +  ( G `  0 ) ) )
387361, 385addcomd 9853 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( -u ( ( _e  ^c  -u j )  x.  ( G `  j
) )  +  ( G `  0 ) )  =  ( ( G `  0 )  +  -u ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) ) )
388385, 360negsubd 10011 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( G `  0
)  +  -u (
( _e  ^c  -u j )  x.  ( G `  j )
) )  =  ( ( G `  0
)  -  ( ( _e  ^c  -u j )  x.  ( G `  j )
) ) )
389387, 388eqtrd 2505 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( -u ( ( _e  ^c  -u j )  x.  ( G `  j
) )  +  ( G `  0 ) )  =  ( ( G `  0 )  -  ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) ) )
390384, 386, 3893eqtrd 2509 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( O `  j
)  -  ( O `
 0 ) )  =  ( ( G `
 0 )  -  ( ( _e  ^c  -u j )  x.  ( G `  j
) ) ) )
391235, 341, 3903eqtrd 2509 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  S. ( 0 (,) j
) ( ( _e 
^c  -u x
)  x.  ( F `
 x ) )  _d x  =  ( ( G `  0
)  -  ( ( _e  ^c  -u j )  x.  ( G `  j )
) ) )
392391oveq2d 6324 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x
) )  _d x )  =  ( ( ( A `  j
)  x.  ( _e 
^c  j ) )  x.  ( ( G `  0 )  -  ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) ) ) )
39325adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  Q  e.  (Poly `  ZZ )
)
394 0zd 10973 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  ZZ )
395 etransclem46.a . . . . . . . . . . 11  |-  A  =  (coeff `  Q )
396395coef2 23264 . . . . . . . . . 10  |-  ( ( Q  e.  (Poly `  ZZ )  /\  0  e.  ZZ )  ->  A : NN0 --> ZZ )
397393, 394, 396syl2anc 673 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  A : NN0 --> ZZ )
398 elfznn0 11913 . . . . . . . . . 10  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
399398adantl 473 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  NN0 )
400397, 399ffvelrnd 6038 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( A `  j )  e.  ZZ )
401400zcnd 11064 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( A `  j )  e.  CC )
402353, 354cxpcld 23732 . . . . . . . 8  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  j )  e.  CC )
403402adantl 473 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
_e  ^c  j )  e.  CC )
404401, 403mulcld 9681 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( A `  j
)  x.  ( _e 
^c  j ) )  e.  CC )
405404, 385, 360subdid 10095 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( G `  0 )  -  ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) ) )  =  ( ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  ( G `  0
) )  -  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j )
) ) ) )
406392, 405eqtrd 2505 . . . 4  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x
) )  _d x )  =  ( ( ( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( G `
 0 ) )  -  ( ( ( A `  j )  x.  ( _e  ^c  j ) )  x.  ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) ) ) )
407406sumeq2dv 13846 . . 3  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  S. ( 0 (,) j ) ( ( _e  ^c  -u x )  x.  ( F `  x )
)  _d x )  =  sum_ j  e.  ( 0 ... M ) ( ( ( ( A `  j )  x.  ( _e  ^c  j ) )  x.  ( G ` 
0 ) )  -  ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j
) ) ) ) )
408 fzfid 12224 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
409404, 385mulcld 9681 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( G `
 0 ) )  e.  CC )
410404, 360mulcld 9681 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j )
) )  e.  CC )
411408, 409, 410fsumsub 13926 . . . 4  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( ( ( ( A `  j )  x.  ( _e  ^c  j ) )  x.  ( G ` 
0 ) )  -  ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j
) ) ) )  =  ( sum_ j  e.  ( 0 ... M
) ( ( ( A `  j )  x.  ( _e  ^c  j ) )  x.  ( G ` 
0 ) )  -  sum_ j  e.  ( 0 ... M ) ( ( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j )
) ) ) )
412 etransclem46.qe0 . . . . . . . . 9  |-  ( ph  ->  ( Q `  _e )  =  0 )
413412eqcomd 2477 . . . . . . . 8  |-  ( ph  ->  0  =  ( Q `
 _e ) )
414395, 23coeid2 23272 . . . . . . . . 9  |-  ( ( Q  e.  (Poly `  ZZ )  /\  _e  e.  CC )  ->  ( Q `
 _e )  = 
sum_ j  e.  ( 0 ... M ) ( ( A `  j )  x.  (
_e ^ j ) ) )
41525, 9, 414sylancl 675 . . . . . . . 8  |-  ( ph  ->  ( Q `  _e )  =  sum_ j  e.  ( 0 ... M
) ( ( A `
 j )  x.  ( _e ^ j
) ) )
416 cxpexp 23692 . . . . . . . . . . . . 13  |-  ( ( _e  e.  CC  /\  j  e.  NN0 )  -> 
( _e  ^c 
j )  =  ( _e ^ j ) )
417353, 398, 416syl2anc 673 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  j )  =  ( _e ^
j ) )
418417eqcomd 2477 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  (
_e ^ j )  =  ( _e  ^c  j ) )
419418oveq2d 6324 . . . . . . . . . 10  |-  ( j  e.  ( 0 ... M )  ->  (
( A `  j
)  x.  ( _e
^ j ) )  =  ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
420419adantl 473 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( A `  j
)  x.  ( _e
^ j ) )  =  ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
421420sumeq2dv 13846 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( ( A `  j )  x.  (
_e ^ j ) )  =  sum_ j  e.  ( 0 ... M
) ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
422413, 415, 4213eqtrd 2509 . . . . . . 7  |-  ( ph  ->  0  =  sum_ j  e.  ( 0 ... M
) ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
423422oveq1d 6323 . . . . . 6  |-  ( ph  ->  ( 0  x.  ( G `  0 )
)  =  ( sum_ j  e.  ( 0 ... M ) ( ( A `  j
)  x.  ( _e 
^c  j ) )  x.  ( G `
 0 ) ) )
424374mul02d 9849 . . . . . 6  |-  ( ph  ->  ( 0  x.  ( G `  0 )
)  =  0 )
425408, 374, 404fsummulc1 13923 . . . . . 6  |-  ( ph  ->  ( sum_ j  e.  ( 0 ... M ) ( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( G `
 0 ) )  =  sum_ j  e.  ( 0 ... M ) ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  ( G `  0
) ) )
426423, 424, 4253eqtr3rd 2514 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( ( ( A `
 j )  x.  ( _e  ^c 
j ) )  x.  ( G `  0
) )  =  0 )
42738a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  G  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  x ) ) )
428 fveq2 5879 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  (
( ( RR  Dn F ) `  i ) `  x
)  =  ( ( ( RR  Dn
F ) `  i
) `  j )
)
429428sumeq2sdv 13847 . . . . . . . . . . . 12  |-  ( x  =  j  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 x )  = 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )
430429adantl 473 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  =  j )  ->  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  x
)  =  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j ) )
431 fzfid 12224 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 ... R )  e. 
Fin )
43233adantlr 729 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
433204adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  j  e.  RR )
434432, 433ffvelrnd 6038 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  i ) `  j
)  e.  CC )
435431, 434fsumcl 13876 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j )  e.  CC )
436427, 430, 204, 435fvmptd 5969 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  j )  =  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )
437436oveq2d 6324 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( _e  ^c  -u j )  x.  ( G `  j )
)  =  ( ( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) )
438437oveq2d 6324 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  ( G `  j )
) )  =  ( ( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) ) )
439357, 435mulcld 9681 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) )  e.  CC )
440401, 403, 439mulassd 9684 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( ( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) )  =  ( ( A `  j )  x.  (
( _e  ^c 
j )  x.  (
( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) ) ) )
441368eqcomi 2480 . . . . . . . . . . . . . . 15  |-  1  =  ( _e  ^c  0 )
442441a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  1  =  ( _e  ^c  0 ) )
443354negidd 9995 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  (
j  +  -u j
)  =  0 )
444443eqcomd 2477 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  0  =  ( j  + 
-u j ) )
445444oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  0 )  =  ( _e  ^c  ( j  + 
-u j ) ) )
44653, 54gtneii 9764 . . . . . . . . . . . . . . . 16  |-  _e  =/=  0
447446a1i 11 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  _e  =/=  0 )
448353, 447, 354, 355cxpaddd 23741 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  ( j  +  -u j ) )  =  ( ( _e 
^c  j )  x.  ( _e  ^c  -u j ) ) )
449442, 445, 4483eqtrd 2509 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  1  =  ( ( _e 
^c  j )  x.  ( _e  ^c  -u j ) ) )
450449oveq1d 6323 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
1  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j ) )  =  ( ( ( _e  ^c  j )  x.  ( _e 
^c  -u j
) )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) )
451450adantl 473 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j ) )  =  ( ( ( _e  ^c  j )  x.  ( _e 
^c  -u j
) )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) )
452435mulid2d 9679 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1  x.  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j ) )  =  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )
453403, 357, 435mulassd 9684 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( _e  ^c  j )  x.  ( _e  ^c  -u j ) )  x. 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )  =  ( ( _e  ^c  j )  x.  ( ( _e  ^c  -u j )  x. 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) ) ) )
454451, 452, 4533eqtr3rd 2514 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( _e  ^c 
j )  x.  (
( _e  ^c  -u j )  x.  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `  i ) `  j
) ) )  = 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  D