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

Theorem etransclem46 37412
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 6288 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  RR  e.  { RR ,  CC } )
8 ere 14031 . . . . . . . . . . . . . . . . . . . 20  |-  _e  e.  RR
98recni 9637 . . . . . . . . . . . . . . . . . . 19  |-  _e  e.  CC
109a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  _e  e.  CC )
11 recn 9611 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  x  e.  CC )
1211negcld 9953 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  -u x  e.  CC )
1310, 12cxpcld 23381 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  (
_e  ^c  -u x
)  e.  CC )
1413adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( _e 
^c  -u x
)  e.  CC )
15 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
16 fzfid 12122 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( 0 ... R )  e. 
Fin )
17 elfznn0 11824 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0 ... R )  ->  i  e.  NN0 )
186adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  RR  e.  { RR ,  CC }
)
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  RR  e.  ( (
TopOpen ` fld )t  RR ) )
2019adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  RR  e.  ( ( TopOpen ` fld )t  RR ) )
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  e.  NN )
2221adantr 463 . . . . . . . . . . . . . . . . . . . . . . 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 3425 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  Q  e.  (Poly `  ZZ ) )
26 dgrcl 22920 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Q  e.  (Poly `  ZZ )  ->  (deg `  Q
)  e.  NN0 )
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  (deg `  Q )  e.  NN0 )
2823, 27syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  NN0 )
2928adantr 463 . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  NN0 )  ->  i  e.  NN0 )
3218, 20, 22, 29, 30, 31etransclem33 37399 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  NN0 )  ->  ( ( RR  Dn F ) `
 i ) : RR --> CC )
3317, 32sylan2 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
3433adantlr 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
35 simplr 754 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  x  e.  RR )
3634, 35ffvelrnd 6009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  i ) `  x
)  e.  CC )
3716, 36fsumcl 13702 . . . . . . . . . . . . . . . . . 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 5940 . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( G `
 x )  = 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  x ) )
4140, 37eqeltrd 2490 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( G `
 x )  e.  CC )
4214, 41mulcld 9645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
4342negcld 9953 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
4443adantlr 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
456, 19dvdmsscn 37082 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  C_  CC )
4645, 21, 30etransclem8 37374 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : RR --> CC )
4746ffvelrnda 6008 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  CC )
4814, 47mulcld 9645 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
4948negcld 9953 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
5049negcld 9953 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  -u -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
5150adantlr 713 . . . . . . . . . . . . 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 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
54 epos 14147 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  _e
5553, 8, 54ltleii 9738 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  _e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  0  <_  _e )
57 renegcl 9917 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  -u x  e.  RR )
5852, 56, 57recxpcld 23396 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
_e  ^c  -u x
)  e.  RR )
5958renegcld 10026 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  -u (
_e  ^c  -u x
)  e.  RR )
6059adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
_e  ^c  -u x
)  e.  RR )
61 reelprrecn 9613 . . . . . . . . . . . . . . . . . . . . . 22  |-  RR  e.  { RR ,  CC }
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  RR  e.  { RR ,  CC } )
63 cnelprrecn 9614 . . . . . . . . . . . . . . . . . . . . . 22  |-  CC  e.  { RR ,  CC }
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  CC  e.  { RR ,  CC } )
6512adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  RR )  ->  -u x  e.  CC )
66 neg1rr 10680 . . . . . . . . . . . . . . . . . . . . . 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 23381 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  (
_e  ^c  y )  e.  CC )
7170adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  y  e.  CC )  ->  (
_e  ^c  y )  e.  CC )
7211adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  x  e.  CC )
73 1red 9640 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  RR )  ->  1  e.  RR )
7462dvmptid 22650 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
7562, 72, 73, 74dvmptneg 22659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  -u x ) )  =  ( x  e.  RR  |->  -u 1 ) )
76 epr 14148 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  _e  e.  RR+
77 dvcxp2 23409 . . . . . . . . . . . . . . . . . . . . . . . 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 23264 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( log `  _e )  =  1
8079oveq1i 6287 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( log `  _e )  x.  ( _e  ^c  y ) )  =  ( 1  x.  ( _e  ^c 
y ) )
8170mulid2d 9643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  CC  ->  (
1  x.  ( _e 
^c  y ) )  =  ( _e 
^c  y ) )
8280, 81syl5eq 2455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  CC  ->  (
( log `  _e )  x.  ( _e  ^c  y ) )  =  ( _e  ^c  y ) )
8382mpteq2ia 4476 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  CC  |->  ( ( log `  _e )  x.  ( _e  ^c  y ) ) )  =  ( y  e.  CC  |->  ( _e 
^c  y ) )
8478, 83eqtri 2431 . . . . . . . . . . . . . . . . . . . . . 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 6285 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  -u x  ->  (
_e  ^c  y )  =  ( _e  ^c  -u x ) )
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 22665 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( RR  _D  (
x  e.  RR  |->  ( _e  ^c  -u x ) ) )  =  ( x  e.  RR  |->  ( ( _e 
^c  -u x
)  x.  -u 1
) ) )
8887trud 1414 . . . . . . . . . . . . . . . . . . 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 9651 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  -u 1  e.  CC )
9113, 90mulcomd 9646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  (
( _e  ^c  -u x )  x.  -u 1
)  =  ( -u
1  x.  ( _e 
^c  -u x
) ) )
9213mulm1d 10048 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  ( -u 1  x.  ( _e 
^c  -u x
) )  =  -u ( _e  ^c  -u x ) )
9391, 92eqtrd 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  ->  (
( _e  ^c  -u x )  x.  -u 1
)  =  -u (
_e  ^c  -u x
) )
9493mpteq2ia 4476 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  |->  ( ( _e  ^c  -u x )  x.  -u 1
) )  =  ( x  e.  RR  |->  -u ( _e  ^c  -u x ) )
9588, 94eqtri 2431 . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  i  e.  NN0 )
98 peano2nn0 10876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
i  +  1 )  e.  NN0 )
100 ovex 6305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  +  1 )  e. 
_V
101 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  ( i  +  1 )  ->  (
j  e.  NN0  <->  ( i  +  1 )  e. 
NN0 ) )
102101anbi2d 702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( i  +  1 )  ->  (
( ph  /\  j  e.  NN0 )  <->  ( ph  /\  ( i  +  1 )  e.  NN0 )
) )
103 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  ( i  +  1 )  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  ( i  +  1 ) ) )
104103feq1d 5699 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( i  +  1 )  ->  (
( ( RR  Dn F ) `  j ) : RR --> CC 
<->  ( ( RR  Dn F ) `  ( i  +  1 ) ) : RR --> CC ) )
105102, 104imbi12d 318 . . . . . . . . . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  j  ->  (
i  e.  NN0  <->  j  e.  NN0 ) )
107106anbi2d 702 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  j  ->  (
( ph  /\  i  e.  NN0 )  <->  ( ph  /\  j  e.  NN0 )
) )
108 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  j  ->  (
( RR  Dn
F ) `  i
)  =  ( ( RR  Dn F ) `  j ) )
109108feq1d 5699 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  j  ->  (
( ( RR  Dn F ) `  i ) : RR --> CC 
<->  ( ( RR  Dn F ) `  j ) : RR --> CC ) )
110107, 109imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . 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 2041 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( RR  Dn F ) `
 j ) : RR --> CC )
112100, 105, 111vtocl 3110 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( i  +  1 )  e. 
NN0 )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
11399, 112syldan 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
114113adantlr 713 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  (
i  +  1 ) ) : RR --> CC )
115114, 35ffvelrnd 6009 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  ( i  +  1 ) ) `  x
)  e.  CC )
11616, 115fsumcl 13702 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x )  e.  CC )
11721, 28, 30, 38etransclem39 37405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G : RR --> CC )
118117feqmptd 5901 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  G  =  ( x  e.  RR  |->  ( G `
 x ) ) )
119118eqcomd 2410 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  ( G `  x ) )  =  G )
120119oveq2d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  (
x  e.  RR  |->  ( G `  x ) ) )  =  ( RR  _D  G ) )
121 nfcv 2564 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x F
122 elfznn0 11824 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 0 ... ( R  +  1 ) )  ->  i  e.  NN0 )
123122, 32sylan2 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
124121, 46, 123, 38etransclem2 37368 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  G
)  =  ( x  e.  RR  |->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  ( i  +  1 ) ) `
 x ) ) )
125120, 124eqtrd 2443 . . . . . . . . . . . . . . . . 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 22654 . . . . . . . . . . . . . . . 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 9646 . . . . . . . . . . . . . . . . . . 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 6293 . . . . . . . . . . . . . . . . . 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 9953 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  -u (
_e  ^c  -u x
)  e.  CC )
130129, 41mulcld 9645 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  ( -u ( _e  ^c  -u x )  x.  ( G `  x )
)  e.  CC )
13114, 116mulcld 9645 . . . . . . . . . . . . . . . . . . 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 9815 . . . . . . . . . . . . . . . . . 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 9972 . . . . . . . . . . . . . . . . . . . 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 10049 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( -u ( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u (
( _e  ^c  -u x )  x.  ( G `  x )
) )
135134oveq2d 6293 . . . . . . . . . . . . . . . . . . . 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 36860 . . . . . . . . . . . . . . . . . . . 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 2453 . . . . . . . . . . . . . . . . . . 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 6293 . . . . . . . . . . . . . . . . . . . . 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 13752 . . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  i  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  i ) )
141140fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  i  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  i
) `  x )
)
142103fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( i  +  1 )  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  (
i  +  1 ) ) `  x ) )
143 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  0 ) )
144143fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( ( RR  Dn F ) `  j ) `  x
)  =  ( ( ( RR  Dn
F ) `  0
) `  x )
)
145 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  ( R  + 
1 )  ->  (
( RR  Dn
F ) `  j
)  =  ( ( RR  Dn F ) `  ( R  +  1 ) ) )
146145fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . 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 10892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  P  e.  NN0 )
14928, 148nn0mulcld 10897 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( M  x.  P
)  e.  NN0 )
150 nnm1nn0 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
152149, 151nn0addcld 10896 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( M  x.  P )  +  ( P  -  1 ) )  e.  NN0 )
153147, 152syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  R  e.  NN0 )
154153adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  R  e. 
NN0 )
155154nn0zd 11005 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  R  e.  ZZ )
156 peano2nn0 10876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( R  e.  NN0  ->  ( R  +  1 )  e. 
NN0 )
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( R  +  1 )  e.  NN0 )
158 nn0uz 11160 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  =  ( ZZ>= `  0 )
159157, 158syl6eleq 2500 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( R  +  1 )  e.  ( ZZ>= ` 
0 ) )
160159adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( R  +  1 )  e.  ( ZZ>= `  0 )
)
161 elfznn0 11824 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  e.  ( 0 ... ( R  +  1 ) )  ->  j  e.  NN0 )
162161, 111sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  j
) : RR --> CC )
163162adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( RR  Dn
F ) `  j
) : RR --> CC )
164 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  x  e.  RR )
165163, 164ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  ( 0 ... ( R  +  1 ) ) )  ->  (
( ( RR  Dn F ) `  j ) `  x
)  e.  CC )
166141, 142, 144, 146, 155, 160, 165telfsum2 13768 . . . . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . . . 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 6293 . . . . . . . . . . . . . . . . . . 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 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  R  e.  RR )
170169ltp1d 10515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  R  <  ( R  +  1 ) )
171147, 170syl5eqbrr 4428 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( M  x.  P )  +  ( P  -  1 ) )  <  ( R  +  1 ) )
172 etransclem5 37371 . . . . . . . . . . . . . . . . . . . . . . . . 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 37398 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  Dn F ) `  ( R  +  1
) )  =  ( x  e.  RR  |->  0 ) )
174173fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 ( R  + 
1 ) ) `  x )  =  ( ( x  e.  RR  |->  0 ) `  x
) )
175 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  |->  0 )  =  ( x  e.  RR  |->  0 )
176175fvmpt2 5940 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  0  e.  RR )  ->  ( ( x  e.  RR  |->  0 ) `  x )  =  0 )
17753, 176mpan2 669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( x  e.  RR  |->  0 ) `  x
)  =  0 )
178174, 177sylan9eq 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( RR  Dn
F ) `  ( R  +  1 ) ) `  x )  =  0 )
179 cnex 9602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  CC  e.  _V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  CC  e.  _V )
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  RR  C_  RR )
1826, 181ssexd 4540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  RR  e.  _V )
183 elpm2r 7473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( CC  e.  _V  /\  RR  e.  _V )  /\  ( F : RR --> CC  /\  RR  C_  RR ) )  ->  F  e.  ( CC  ^pm  RR ) )
184180, 182, 46, 181, 183syl22anc 1231 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
185 dvn0 22617 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  C_  CC  /\  F  e.  ( CC  ^pm  RR ) )  ->  (
( RR  Dn
F ) `  0
)  =  F )
18645, 184, 185syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  Dn F ) ` 
0 )  =  F )
187186fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 0 ) `  x )  =  ( F `  x ) )
188187adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( RR  Dn
F ) `  0
) `  x )  =  ( F `  x ) )
189178, 188oveq12d 6295 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( ( RR  Dn F ) `  ( R  +  1
) ) `  x
)  -  ( ( ( RR  Dn
F ) `  0
) `  x )
)  =  ( 0  -  ( F `  x ) ) )
190 df-neg 9843 . . . . . . . . . . . . . . . . . . . . 21  |-  -u ( F `  x )  =  ( 0  -  ( F `  x
) )
191189, 190syl6eqr 2461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( ( RR  Dn F ) `  ( R  +  1
) ) `  x
)  -  ( ( ( RR  Dn
F ) `  0
) `  x )
)  =  -u ( F `  x )
)
192191oveq2d 6293 . . . . . . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( _e  ^c  -u x )  x.  -u ( F `  x )
)  =  -u (
( _e  ^c  -u x )  x.  ( F `  x )
) )
197196mpteq2dva 4480 . . . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . . . 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 22659 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . 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 9626 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  RR )
202 elfzelz 11740 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
203202zred 11007 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
204203adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  RR )
205201, 204iccssred 36888 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 [,] j ) 
C_  RR )
206 eqid 2402 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
207206tgioo2 21598 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
208 0red 9626 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  0  e.  RR )
209 iccntr 21616 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  j  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
210208, 203, 209syl2anc 659 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
211210adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] j ) )  =  ( 0 (,) j
) )
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 22655 . . . . . . . . . . . 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 11611 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 0 (,) j )  ->  x  e.  RR )
215214recnd 9651 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( 0 (,) j )  ->  x  e.  CC )
216215adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  CC )
217216negcld 9953 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  -u x  e.  CC )
218213, 217cxpcld 23381 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  (
_e  ^c  -u x
)  e.  CC )
21946adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  F : RR --> CC )
220214adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  RR )
221219, 220ffvelrnd 6009 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  ( F `  x )  e.  CC )
222218, 221mulcld 9645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
223222negnegd 9957 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  -u -u (
( _e  ^c  -u x )  x.  ( F `  x )
)  =  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
224223mpteq2dva 4480 . . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 2447 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  =  ( x  e.  ( 0 (,) j ) 
|->  ( ( _e  ^c  -u x )  x.  ( F `  x
) ) ) )
227226fveq1d 5850 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( RR  _D  O
) `  x )  =  ( ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) ) `  x
) )
228227adantr 463 . . . . . . . . 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 459 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 0 (,) j
) )  ->  x  e.  ( 0 (,) j
) )
230 eqid 2402 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  =  ( x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )
231230fvmpt2 5940 . . . . . . . . . . 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 659 . . . . . . . . . 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 713 . . . . . . . . 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 2444 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  =  ( ( RR  _D  O ) `
 x ) )
235234itgeq2d 37131 . . . . . . 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 11741 . . . . . . . . 9  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
237236adantl 464 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  <_  j )
238 eqid 2402 . . . . . . . . . 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 2403 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( y  e.  CC  |->  ( _e  ^c  y ) )  =  ( y  e.  CC  |->  ( _e  ^c  y ) ) )
24086adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  /\  y  = 
-u x )  -> 
( _e  ^c 
y )  =  ( _e  ^c  -u x ) )
241208, 203iccssred 36888 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  (
0 [,] j ) 
C_  RR )
242 ax-resscn 9578 . . . . . . . . . . . . . . . . . . 19  |-  RR  C_  CC
243241, 242syl6ss 3453 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
0 [,] j ) 
C_  CC )
244243sselda 3441 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  x  e.  CC )
245244negcld 9953 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  -u x  e.  CC )
2469a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  ->  _e  e.  CC )
247 negcl 9855 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  ->  -u x  e.  CC )
248246, 247cxpcld 23381 . . . . . . . . . . . . . . . . 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 5937 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( ( y  e.  CC  |->  ( _e 
^c  y ) ) `  -u x
)  =  ( _e 
^c  -u x
) )
251250eqcomd 2410 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  ( _e  ^c  -u x )  =  ( ( y  e.  CC  |->  ( _e  ^c  y ) ) `
 -u x ) )
252251adantll 712 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  (
_e  ^c  -u x
)  =  ( ( y  e.  CC  |->  ( _e  ^c  y ) ) `  -u x
) )
253252mpteq2dva 4480 . . . . . . . . . . . 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 11375 . . . . . . . . . . . . . . . . . 18  |- -oo  e.  RR*
255254a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  -> -oo  e.  RR* )
256 0red 9626 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  0  e.  RR )
257 rpxr 11271 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  _e  e.  RR* )
258 rpgt0 11275 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  RR+  ->  0  < 
_e )
259255, 256, 257, 258gtnelioc 36872 . . . . . . . . . . . . . . . 16  |-  ( _e  e.  RR+  ->  -.  _e  e.  ( -oo (,] 0
) )
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15  |-  -.  _e  e.  ( -oo (,] 0
)
261 eldif 3423 . . . . . . . . . . . . . . 15  |-  ( _e  e.  ( CC  \ 
( -oo (,] 0 ) )  <->  ( _e  e.  CC  /\  -.  _e  e.  ( -oo (,] 0 ) ) )
2629, 260, 261mpbir2an 921 . . . . . . . . . . . . . 14  |-  _e  e.  ( CC  \  ( -oo (,] 0 ) )
263 cxpcncf2 37052 . . . . . . . . . . . . . 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 2402 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0 [,] j )  |->  -u x
)  =  ( x  e.  ( 0 [,] j )  |->  -u x
)
266265negcncf 21712 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  -u x )  e.  ( ( 0 [,] j
) -cn-> CC ) )
269264, 268cncfmpt1f 21707 . . . . . . . . . . . 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 2490 . . . . . . . . . . 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 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN )
27328ad2antrr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  M  e.  NN0 )
274 etransclem6 37372 . . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . . 14  |-  F  =  ( y  e.  RR  |->  ( ( y ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( y  -  k ) ^ P ) ) )
276241sselda 3441 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  x  e.  ( 0 [,] j ) )  ->  x  e.  RR )
277276adantll 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  x  e.  RR )
278271, 272, 273, 275, 277etransclem13 37379 . . . . . . . . . . . . 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 4480 . . . . . . . . . . . 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 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 [,] j ) 
C_  CC )
281 fzfid 12122 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 ... M )  e. 
Fin )
282277recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  x  e.  CC )
2832823adant3 1017 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  x  e.  CC )
284 elfzelz 11740 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... M )  ->  k  e.  ZZ )
285284zcnd 11008 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... M )  ->  k  e.  CC )
2862853ad2ant3 1020 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  k  e.  CC )
287283, 286subcld 9966 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  (
x  -  k )  e.  CC )
28821adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN )
289288, 150syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  ( P  -  1 )  e.  NN0 )
290148adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  P  e.  NN0 )
291289, 290ifcld 3927 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 0 [,] j
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
2922913adant3 1017 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
2932923adant1r 1223 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
)  /\  k  e.  ( 0 ... M
) )  ->  if ( k  =  0 ,  ( P  - 
1 ) ,  P
)  e.  NN0 )
294287, 293expcld 12352 . . . . . . . . . . . . 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 1728 . . . . . . . . . . . . . 14  |-  F/ x
( ( ph  /\  j  e.  ( 0 ... M ) )  /\  k  e.  ( 0 ... M ) )
296243adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( 0 [,] j )  C_  CC )
297 ssid 3460 . . . . . . . . . . . . . . . . . 18  |-  CC  C_  CC
298297a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  CC  C_  CC )
299296, 298idcncfg 37023 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  x )  e.  ( ( 0 [,] j ) -cn-> CC ) )
300285adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  CC )
301296, 300, 298constcncfg 37022 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  k )  e.  ( ( 0 [,] j ) -cn-> CC ) )
302299, 301subcncf 37020 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  ( 0 ... M )  /\  k  e.  ( 0 ... M ) )  ->  ( x  e.  ( 0 [,] j
)  |->  ( x  -  k ) )  e.  ( ( 0 [,] j ) -cn-> CC ) )
303302adantll 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  k  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( x  -  k ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
304151, 148ifcld 3927 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( k  =  0 ,  ( P  -  1 ) ,  P )  e.  NN0 )
305 expcncf 21716 . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . 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 6284 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  -  k )  ->  (
y ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) )  =  ( ( x  -  k ) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) )
310295, 303, 307, 308, 309cncfcompt2 37051 . . . . . . . . . . . . 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 37053 . . . . . . . . . . . 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 2490 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( F `  x ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
313270, 312mulcncf 22149 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
314 ioossicc 11662 . . . . . . . . . . 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 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 (,) j
) )  ->  (
( _e  ^c  -u x )  x.  ( F `  x )
)  e.  CC )
318238, 313, 315, 316, 317cncfmptssg 37021 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  ( ( 0 (,) j
) -cn-> CC ) )
319226, 318eqeltrd 2490 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  e.  ( ( 0 (,) j ) -cn-> CC ) )
32019adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  RR  e.  ( ( TopOpen ` fld )t  RR ) )
32121adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  P  e.  NN )
32228adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  M  e.  NN0 )
323 oveq2 6285 . . . . . . . . . . . . . . 15  |-  ( j  =  k  ->  (
x  -  j )  =  ( x  -  k ) )
324323oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  (
( x  -  j
) ^ P )  =  ( ( x  -  k ) ^ P ) )
325324cbvprodv 13873 . . . . . . . . . . . . 13  |-  prod_ j  e.  ( 1 ... M
) ( ( x  -  j ) ^ P )  =  prod_ k  e.  ( 1 ... M ) ( ( x  -  k ) ^ P )
326325oveq2i 6288 . . . . . . . . . . . 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 4477 . . . . . . . . . . 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 2431 . . . . . . . . . 10  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ k  e.  ( 1 ... M ) ( ( x  -  k ) ^ P ) ) )
3297, 320, 321, 322, 328, 201, 204etransclem18 37384 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 (,) j )  |->  ( ( _e  ^c  -u x )  x.  ( F `  x )
) )  e.  L^1 )
330226, 329eqeltrd 2490 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( RR  _D  O )  e.  L^1 )
331 eqid 2402 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  ( G `
 x ) )  =  ( x  e.  RR  |->  ( G `  x ) )
3326, 19, 21, 28, 30, 38etransclem43 37409 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  e.  ( RR
-cn-> CC ) )
333119, 332eqeltrd 2490 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  RR  |->  ( G `  x ) )  e.  ( RR
-cn-> CC ) )
334333adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  RR  |->  ( G `  x ) )  e.  ( RR
-cn-> CC ) )
335117ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  G : RR --> CC )
336335, 277ffvelrnd 6009 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  e.  ( 0 [,] j
) )  ->  ( G `  x )  e.  CC )
337331, 334, 205, 316, 336cncfmptssg 37021 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( G `  x ) )  e.  ( ( 0 [,] j )
-cn-> CC ) )
338270, 337mulcncf 22149 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
x  e.  ( 0 [,] j )  |->  ( ( _e  ^c  -u x )  x.  ( G `  x )
) )  e.  ( ( 0 [,] j
) -cn-> CC ) )
339338negcncfg 37032 . . . . . . . . 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 2494 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  O  e.  ( ( 0 [,] j ) -cn-> CC ) )
341201, 204, 237, 319, 330, 340ftc2 22735 . . . . . . 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 9847 . . . . . . . . . . . . . 14  |-  ( x  =  j  ->  -u x  =  -u j )
344343oveq2d 6293 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  (
_e  ^c  -u x
)  =  ( _e 
^c  -u j
) )
345 fveq2 5848 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  ( G `  x )  =  ( G `  j ) )
346344, 345oveq12d 6295 . . . . . . . . . . . 12  |-  ( x  =  j  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( ( _e  ^c  -u j )  x.  ( G `  j )
) )
347346negeqd 9849 . . . . . . . . . . 11  |-  ( x  =  j  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u (
( _e  ^c  -u j )  x.  ( G `  j )
) )
348347adantl 464 . . . . . . . . . 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 9672 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  RR* )
350204rexrd 9672 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  RR* )
351 ubicc2 11689 . . . . . . . . . . 11  |-  ( ( 0  e.  RR*  /\  j  e.  RR*  /\  0  <_ 
j )  ->  j  e.  ( 0 [,] j
) )
352349, 350, 237, 351syl3anc 1230 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  ( 0 [,] j
) )
3539a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  _e  e.  CC )
354203recnd 9651 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
355354negcld 9953 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  -u j  e.  CC )
356353, 355cxpcld 23381 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  -u j
)  e.  CC )
357356adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
_e  ^c  -u j
)  e.  CC )
358117adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  G : RR --> CC )
359358, 204ffvelrnd 6009 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  j )  e.  CC )
360357, 359mulcld 9645 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( _e  ^c  -u j )  x.  ( G `  j )
)  e.  CC )
361360negcld 9953 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  -u (
( _e  ^c  -u j )  x.  ( G `  j )
)  e.  CC )
362342, 348, 352, 361fvmptd 5937 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( O `  j )  =  -u ( ( _e 
^c  -u j
)  x.  ( G `
 j ) ) )
363 negeq 9847 . . . . . . . . . . . . . . . 16  |-  ( x  =  0  ->  -u x  =  -u 0 )
364363oveq2d 6293 . . . . . . . . . . . . . . 15  |-  ( x  =  0  ->  (
_e  ^c  -u x
)  =  ( _e 
^c  -u 0
) )
365 neg0 9900 . . . . . . . . . . . . . . . . 17  |-  -u 0  =  0
366365oveq2i 6288 . . . . . . . . . . . . . . . 16  |-  ( _e 
^c  -u 0
)  =  ( _e 
^c  0 )
367 cxp0 23343 . . . . . . . . . . . . . . . . 17  |-  ( _e  e.  CC  ->  (
_e  ^c  0 )  =  1 )
3689, 367ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( _e 
^c  0 )  =  1
369366, 368eqtri 2431 . . . . . . . . . . . . . . 15  |-  ( _e 
^c  -u 0
)  =  1
370364, 369syl6eq 2459 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  (
_e  ^c  -u x
)  =  1 )
371 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  ( G `  x )  =  ( G ` 
0 ) )
372370, 371oveq12d 6295 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( 1  x.  ( G ` 
0 ) ) )
373 0red 9626 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  RR )
374117, 373ffvelrnd 6009 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  0
)  e.  CC )
375374mulid2d 9643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  x.  ( G `  0 )
)  =  ( G `
 0 ) )
376372, 375sylan9eqr 2465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  = 
0 )  ->  (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  ( G `
 0 ) )
377376negeqd 9849 . . . . . . . . . . 11  |-  ( (
ph  /\  x  = 
0 )  ->  -u (
( _e  ^c  -u x )  x.  ( G `  x )
)  =  -u ( G `  0 )
)
378377adantlr 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  x  =  0 )  ->  -u ( ( _e  ^c  -u x )  x.  ( G `  x
) )  =  -u ( G `  0 ) )
379 lbicc2 11688 . . . . . . . . . . 11  |-  ( ( 0  e.  RR*  /\  j  e.  RR*  /\  0  <_ 
j )  ->  0  e.  ( 0 [,] j
) )
380349, 350, 237, 379syl3anc 1230 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  ( 0 [,] j
) )
381374negcld 9953 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( G ` 
0 )  e.  CC )
382381adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  -u ( G `  0 )  e.  CC )
383342, 378, 380, 382fvmptd 5937 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( O `  0 )  =  -u ( G ` 
0 ) )
384362, 383oveq12d 6295 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( O `  j
)  -  ( O `
 0 ) )  =  ( -u (
( _e  ^c  -u j )  x.  ( G `  j )
)  -  -u ( G `  0 )
) )
385374adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  0 )  e.  CC )
386361, 385subnegd 9973 . . . . . . . 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 9815 . . . . . . . . 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 9972 . . . . . . . . 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 2443 . . . . . . . 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 2447 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( O `  j
)  -  ( O `
 0 ) )  =  ( ( G `
 0 )  -  ( ( _e  ^c  -u j )  x.  ( G `  j
) ) ) )
391235, 341, 3903eqtrd 2447 . . . . . 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 6293 . . . . 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 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  Q  e.  (Poly `  ZZ )
)
394 0zd 10916 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  ZZ )
395 etransclem46.a . . . . . . . . . . 11  |-  A  =  (coeff `  Q )
396395coef2 22918 . . . . . . . . . 10  |-  ( ( Q  e.  (Poly `  ZZ )  /\  0  e.  ZZ )  ->  A : NN0 --> ZZ )
397393, 394, 396syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  A : NN0 --> ZZ )
398 elfznn0 11824 . . . . . . . . . 10  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
399398adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  NN0 )
400397, 399ffvelrnd 6009 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( A `  j )  e.  ZZ )
401400zcnd 11008 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( A `  j )  e.  CC )
402353, 354cxpcld 23381 . . . . . . . 8  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  j )  e.  CC )
403402adantl 464 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
_e  ^c  j )  e.  CC )
404401, 403mulcld 9645 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( A `  j
)  x.  ( _e 
^c  j ) )  e.  CC )
405404, 385, 360subdid 10052 . . . . 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 2443 . . . 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 13672 . . 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 12122 . . . . 5  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
409404, 385mulcld 9645 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( A `  j )  x.  (
_e  ^c  j ) )  x.  ( G `
 0 ) )  e.  CC )
410404, 360mulcld 9645 . . . . 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 13752 . . . 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 2410 . . . . . . . 8  |-  ( ph  ->  0  =  ( Q `
 _e ) )
414395, 23coeid2 22926 . . . . . . . . 9  |-  ( ( Q  e.  (Poly `  ZZ )  /\  _e  e.  CC )  ->  ( Q `
 _e )  = 
sum_ j  e.  ( 0 ... M ) ( ( A `  j )  x.  (
_e ^ j ) ) )
41525, 9, 414sylancl 660 . . . . . . . 8  |-  ( ph  ->  ( Q `  _e )  =  sum_ j  e.  ( 0 ... M
) ( ( A `
 j )  x.  ( _e ^ j
) ) )
416 cxpexp 23341 . . . . . . . . . . . . 13  |-  ( ( _e  e.  CC  /\  j  e.  NN0 )  -> 
( _e  ^c 
j )  =  ( _e ^ j ) )
417353, 398, 416syl2anc 659 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  j )  =  ( _e ^
j ) )
418417eqcomd 2410 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  (
_e ^ j )  =  ( _e  ^c  j ) )
419418oveq2d 6293 . . . . . . . . . 10  |-  ( j  e.  ( 0 ... M )  ->  (
( A `  j
)  x.  ( _e
^ j ) )  =  ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
420419adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( A `  j
)  x.  ( _e
^ j ) )  =  ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
421420sumeq2dv 13672 . . . . . . . 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 2447 . . . . . . 7  |-  ( ph  ->  0  =  sum_ j  e.  ( 0 ... M
) ( ( A `
 j )  x.  ( _e  ^c 
j ) ) )
423422oveq1d 6292 . . . . . 6  |-  ( ph  ->  ( 0  x.  ( G `  0 )
)  =  ( sum_ j  e.  ( 0 ... M ) ( ( A `  j
)  x.  ( _e 
^c  j ) )  x.  ( G `
 0 ) ) )
424374mul02d 9811 . . . . . 6  |-  ( ph  ->  ( 0  x.  ( G `  0 )
)  =  0 )
425408, 374, 404fsummulc1 13749 . . . . . 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 2452 . . . . 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 5848 . . . . . . . . . . . . 13  |-  ( x  =  j  ->  (
( ( RR  Dn F ) `  i ) `  x
)  =  ( ( ( RR  Dn
F ) `  i
) `  j )
)
429428sumeq2sdv 13673 . . . . . . . . . . . 12  |-  ( x  =  j  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 x )  = 
sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )
430429adantl 464 . . . . . . . . . . 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 12122 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
0 ... R )  e. 
Fin )
43233adantlr 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  (
( RR  Dn
F ) `  i
) : RR --> CC )
433204adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  j  e.  RR )
434432, 433ffvelrnd 6009 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  i  e.  ( 0 ... R
) )  ->  (
( ( RR  Dn F ) `  i ) `  j
)  e.  CC )
435431, 434fsumcl 13702 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  sum_ i  e.  ( 0 ... R
) ( ( ( RR  Dn F ) `  i ) `
 j )  e.  CC )
436427, 430, 204, 435fvmptd 5937 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( G `  j )  =  sum_ i  e.  ( 0 ... R ) ( ( ( RR  Dn F ) `
 i ) `  j ) )
437436oveq2d 6293 . . . . . . . . 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 6293 . . . . . . . 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 9645 . . . . . . . . 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 9648 . . . . . . . 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 2415 . . . . . . . . . . . . . . 15  |-  1  =  ( _e  ^c  0 )
442441a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  1  =  ( _e  ^c  0 ) )
443354negidd 9956 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  (
j  +  -u j
)  =  0 )
444443eqcomd 2410 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  0  =  ( j  + 
-u j ) )
445444oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  0 )  =  ( _e  ^c  ( j  + 
-u j ) ) )
44653, 54gtneii 9727 . . . . . . . . . . . . . . . 16  |-  _e  =/=  0
447446a1i 11 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  _e  =/=  0 )
448353, 447, 354, 355cxpaddd 23390 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
_e  ^c  ( j  +  -u j ) )  =  ( ( _e 
^c  j )  x.  ( _e  ^c  -u j ) ) )
449442, 445, 4483eqtrd 2447 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  1  =  ( ( _e 
^c  j )  x.  ( _e  ^c  -u j ) ) )
450449oveq1d 6292 . . . . . . . . . . . 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 464 . . . . . . . . . . 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 9643 . . . . . . . . . . 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 9648 . . . . . . . . . . 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 2452 . . . . . . . . . 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