Metamath Proof Explorer

Theorem etransclem46

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

Ref Expression
Hypotheses etransclem46.q 
|- ( 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 ` CCfld ) |`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 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 ) ) ) )

Proof

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