MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pserdvlem2 Unicode version

Theorem pserdvlem2 19804
Description: Lemma for pserdv 19805. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
pserf.g  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
pserf.f  |-  F  =  ( y  e.  S  |-> 
sum_ j  e.  NN0  ( ( G `  y ) `  j
) )
pserf.a  |-  ( ph  ->  A : NN0 --> CC )
pserf.r  |-  R  =  sup ( { r  e.  RR  |  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
psercn.s  |-  S  =  ( `' abs " (
0 [,) R ) )
psercn.m  |-  M  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )
pserdv.b  |-  B  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a
)  +  M )  /  2 ) )
Assertion
Ref Expression
pserdvlem2  |-  ( (
ph  /\  a  e.  S )  ->  ( CC  _D  ( F  |`  B ) )  =  ( y  e.  B  |-> 
sum_ k  e.  NN0  ( ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) )  x.  (
y ^ k ) ) ) )
Distinct variable groups:    j, a,
k, n, r, x, y, A    j, M, k, y    B, j, k, x, y    j, G, k, r, y    S, a, j, k, y    F, a    ph, a, j, k, y
Allowed substitution hints:    ph( x, n, r)    B( n, r, a)    R( x, y, j, k, n, r, a)    S( x, n, r)    F( x, y, j, k, n, r)    G( x, n, a)    M( x, n, r, a)

Proof of Theorem pserdvlem2
Dummy variables  m  s  w  z  i are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 10262 . 2  |-  NN0  =  ( ZZ>= `  0 )
2 cnex 8818 . . . 4  |-  CC  e.  _V
32prid2 3735 . . 3  |-  CC  e.  { RR ,  CC }
43a1i 10 . 2  |-  ( (
ph  /\  a  e.  S )  ->  CC  e.  { RR ,  CC } )
5 0z 10035 . . 3  |-  0  e.  ZZ
65a1i 10 . 2  |-  ( (
ph  /\  a  e.  S )  ->  0  e.  ZZ )
7 fzfid 11035 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  ( 0 ... k )  e. 
Fin )
8 pserf.g . . . . . . . 8  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
9 pserf.a . . . . . . . . 9  |-  ( ph  ->  A : NN0 --> CC )
109ad3antrrr 710 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  A : NN0
--> CC )
11 pserdv.b . . . . . . . . . . 11  |-  B  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a
)  +  M )  /  2 ) )
12 cnxmet 18282 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
1312a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
14 0cn 8831 . . . . . . . . . . . . 13  |-  0  e.  CC
1514a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  0  e.  CC )
16 pserf.f . . . . . . . . . . . . . . 15  |-  F  =  ( y  e.  S  |-> 
sum_ j  e.  NN0  ( ( G `  y ) `  j
) )
17 pserf.r . . . . . . . . . . . . . . 15  |-  R  =  sup ( { r  e.  RR  |  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
18 psercn.s . . . . . . . . . . . . . . 15  |-  S  =  ( `' abs " (
0 [,) R ) )
19 psercn.m . . . . . . . . . . . . . . 15  |-  M  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )
208, 16, 9, 17, 18, 19pserdvlem1 19803 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( ( abs `  a )  +  M
)  /  2 )  e.  RR+  /\  ( abs `  a )  < 
( ( ( abs `  a )  +  M
)  /  2 )  /\  ( ( ( abs `  a )  +  M )  / 
2 )  <  R
) )
2120simp1d 967 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e.  RR+ )
2221rpxrd 10391 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )
23 blssm 17968 . . . . . . . . . . . 12  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  CC )
2413, 15, 22, 23syl3anc 1182 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  CC )
2511, 24syl5eqss 3222 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  CC )
2625adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  ->  B  C_  CC )
2726sselda 3180 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  y  e.  CC )
288, 10, 27psergf 19788 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  ( G `  y ) : NN0 --> CC )
29 elfznn0 10822 . . . . . . 7  |-  ( i  e.  ( 0 ... k )  ->  i  e.  NN0 )
30 ffvelrn 5663 . . . . . . 7  |-  ( ( ( G `  y
) : NN0 --> CC  /\  i  e.  NN0 )  -> 
( ( G `  y ) `  i
)  e.  CC )
3128, 29, 30syl2an 463 . . . . . 6  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  /\  i  e.  ( 0 ... k
) )  ->  (
( G `  y
) `  i )  e.  CC )
327, 31fsumcl 12206 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i )  e.  CC )
33 eqid 2283 . . . . 5  |-  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) )
3432, 33fmptd 5684 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  ->  (
y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y
) `  i )
) : B --> CC )
35 ovex 5883 . . . . . 6  |-  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  e.  _V
3611, 35eqeltri 2353 . . . . 5  |-  B  e. 
_V
372, 36elmap 6796 . . . 4  |-  ( ( y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y
) `  i )
)  e.  ( CC 
^m  B )  <->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) : B --> CC )
3834, 37sylibr 203 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  ->  (
y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y
) `  i )
)  e.  ( CC 
^m  B ) )
39 eqid 2283 . . 3  |-  ( k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) )  =  ( k  e. 
NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) )
4038, 39fmptd 5684 . 2  |-  ( (
ph  /\  a  e.  S )  ->  (
k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) : NN0 --> ( CC 
^m  B ) )
418, 16, 9, 17, 18, 19psercn 19802 . . . . 5  |-  ( ph  ->  F  e.  ( S
-cn-> CC ) )
42 cncff 18397 . . . . 5  |-  ( F  e.  ( S -cn-> CC )  ->  F : S
--> CC )
4341, 42syl 15 . . . 4  |-  ( ph  ->  F : S --> CC )
4443adantr 451 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  F : S --> CC )
458, 16, 9, 17, 18, 20psercnlem2 19800 . . . . . 6  |-  ( (
ph  /\  a  e.  S )  ->  (
a  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  /\  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M
)  /  2 ) ) )  /\  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M )  / 
2 ) ) ) 
C_  S ) )
4645simp2d 968 . . . . 5  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M
)  /  2 ) ) ) )
4711, 46syl5eqss 3222 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  ( `' abs " (
0 [,] ( ( ( abs `  a
)  +  M )  /  2 ) ) ) )
4845simp3d 969 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M )  / 
2 ) ) ) 
C_  S )
4947, 48sstrd 3189 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  S )
50 fssres 5408 . . 3  |-  ( ( F : S --> CC  /\  B  C_  S )  -> 
( F  |`  B ) : B --> CC )
5144, 49, 50syl2anc 642 . 2  |-  ( (
ph  /\  a  e.  S )  ->  ( F  |`  B ) : B --> CC )
525a1i 10 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  0  e.  ZZ )
53 eqidd 2284 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  j  e.  NN0 )  ->  ( ( G `  z ) `  j )  =  ( ( G `  z
) `  j )
)
549ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  A : NN0 --> CC )
5525sselda 3180 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  CC )
568, 54, 55psergf 19788 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( G `  z ) : NN0 --> CC )
57 ffvelrn 5663 . . . . . 6  |-  ( ( ( G `  z
) : NN0 --> CC  /\  j  e.  NN0 )  -> 
( ( G `  z ) `  j
)  e.  CC )
5856, 57sylan 457 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  j  e.  NN0 )  ->  ( ( G `  z ) `  j )  e.  CC )
5955abscld 11918 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  e.  RR )
6059rexrd 8881 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  e. 
RR* )
6122adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )
62 iccssxr 10732 . . . . . . . . 9  |-  ( 0 [,]  +oo )  C_  RR*
638, 9, 17radcnvcl 19793 . . . . . . . . 9  |-  ( ph  ->  R  e.  ( 0 [,]  +oo ) )
6462, 63sseldi 3178 . . . . . . . 8  |-  ( ph  ->  R  e.  RR* )
6564ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  R  e.  RR* )
66 eqid 2283 . . . . . . . . . . 11  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
6766cnmetdval 18280 . . . . . . . . . 10  |-  ( ( z  e.  CC  /\  0  e.  CC )  ->  ( z ( abs 
o.  -  ) 0 )  =  ( abs `  ( z  -  0 ) ) )
6855, 14, 67sylancl 643 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  =  ( abs `  (
z  -  0 ) ) )
6955subid1d 9146 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z  -  0 )  =  z )
7069fveq2d 5529 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  ( z  - 
0 ) )  =  ( abs `  z
) )
7168, 70eqtrd 2315 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  =  ( abs `  z
) )
72 simpr 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  B )
7372, 11syl6eleq 2373 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a
)  +  M )  /  2 ) ) )
7412a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
7514a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  0  e.  CC )
76 elbl3 17951 . . . . . . . . . 10  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  ( ( ( abs `  a )  +  M )  / 
2 )  e.  RR* )  /\  ( 0  e.  CC  /\  z  e.  CC ) )  -> 
( z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  <->  ( z ( abs  o.  -  )
0 )  <  (
( ( abs `  a
)  +  M )  /  2 ) ) )
7774, 61, 75, 55, 76syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  <->  ( z ( abs  o.  -  )
0 )  <  (
( ( abs `  a
)  +  M )  /  2 ) ) )
7873, 77mpbid 201 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  <  ( ( ( abs `  a )  +  M )  / 
2 ) )
7971, 78eqbrtrrd 4045 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  < 
( ( ( abs `  a )  +  M
)  /  2 ) )
8020simp3d 969 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
R )
8180adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
R )
8260, 61, 65, 79, 81xrlttrd 10490 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  < 
R )
838, 54, 17, 55, 82radcnvlt2 19795 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  e.  dom  ~~>  )
841, 52, 53, 58, 83isumclim2 12221 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  ~~>  sum_ j  e.  NN0  ( ( G `
 z ) `  j ) )
8549sselda 3180 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  S )
86 fveq2 5525 . . . . . . . 8  |-  ( y  =  z  ->  ( G `  y )  =  ( G `  z ) )
8786fveq1d 5527 . . . . . . 7  |-  ( y  =  z  ->  (
( G `  y
) `  j )  =  ( ( G `
 z ) `  j ) )
8887sumeq2sdv 12177 . . . . . 6  |-  ( y  =  z  ->  sum_ j  e.  NN0  ( ( G `
 y ) `  j )  =  sum_ j  e.  NN0  ( ( G `  z ) `
 j ) )
89 sumex 12160 . . . . . 6  |-  sum_ j  e.  NN0  ( ( G `
 z ) `  j )  e.  _V
9088, 16, 89fvmpt 5602 . . . . 5  |-  ( z  e.  S  ->  ( F `  z )  =  sum_ j  e.  NN0  ( ( G `  z ) `  j
) )
9185, 90syl 15 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( F `  z )  =  sum_ j  e.  NN0  ( ( G `  z ) `  j
) )
9284, 91breqtrrd 4049 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  ~~>  ( F `
 z ) )
93 oveq2 5866 . . . . . . . . . . 11  |-  ( k  =  m  ->  (
0 ... k )  =  ( 0 ... m
) )
9493sumeq1d 12174 . . . . . . . . . 10  |-  ( k  =  m  ->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i )  =  sum_ i  e.  ( 0 ... m ) ( ( G `  y
) `  i )
)
9594mpteq2dv 4107 . . . . . . . . 9  |-  ( k  =  m  ->  (
y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y
) `  i )
)  =  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i ) ) )
9636mptex 5746 . . . . . . . . 9  |-  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i ) )  e. 
_V
9795, 39, 96fvmpt 5602 . . . . . . . 8  |-  ( m  e.  NN0  ->  ( ( k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) `
 m )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) )
9897adantl 452 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( (
k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) `
 m )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) )
9998fveq1d 5527 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( (
( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m ) `  z
)  =  ( ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( G `  y
) `  i )
) `  z )
)
10086fveq1d 5527 . . . . . . . . 9  |-  ( y  =  z  ->  (
( G `  y
) `  i )  =  ( ( G `
 z ) `  i ) )
101100sumeq2sdv 12177 . . . . . . . 8  |-  ( y  =  z  ->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i )  =  sum_ i  e.  ( 0 ... m ) ( ( G `  z
) `  i )
)
102 eqid 2283 . . . . . . . 8  |-  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i ) )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) )
103 sumex 12160 . . . . . . . 8  |-  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i )  e.  _V
104101, 102, 103fvmpt 5602 . . . . . . 7  |-  ( z  e.  B  ->  (
( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) `  z
)  =  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i ) )
105104ad2antlr 707 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( (
y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( G `  y
) `  i )
) `  z )  =  sum_ i  e.  ( 0 ... m ) ( ( G `  z ) `  i
) )
106 eqidd 2284 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m
) )  ->  (
( G `  z
) `  i )  =  ( ( G `
 z ) `  i ) )
107 simpr 447 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  m  e.  NN0 )
108107, 1syl6eleq 2373 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  m  e.  ( ZZ>= `  0 )
)
10956adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( G `  z ) : NN0 --> CC )
110 elfznn0 10822 . . . . . . . 8  |-  ( i  e.  ( 0 ... m )  ->  i  e.  NN0 )
111 ffvelrn 5663 . . . . . . . 8  |-  ( ( ( G `  z
) : NN0 --> CC  /\  i  e.  NN0 )  -> 
( ( G `  z ) `  i
)  e.  CC )
112109, 110, 111syl2an 463 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m
) )  ->  (
( G `  z
) `  i )  e.  CC )
113106, 108, 112fsumser 12203 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i )  =  (  seq  0 (  +  ,  ( G `  z ) ) `  m ) )
11499, 105, 1133eqtrd 2319 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( (
( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m ) `  z
)  =  (  seq  0 (  +  , 
( G `  z
) ) `  m
) )
115114mpteq2dva 4106 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
m  e.  NN0  |->  ( ( ( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m ) `  z
) )  =  ( m  e.  NN0  |->  (  seq  0 (  +  , 
( G `  z
) ) `  m
) ) )
116 seqfn 11058 . . . . . . 7  |-  ( 0  e.  ZZ  ->  seq  0 (  +  , 
( G `  z
) )  Fn  ( ZZ>=
`  0 ) )
1175, 116ax-mp 8 . . . . . 6  |-  seq  0
(  +  ,  ( G `  z ) )  Fn  ( ZZ>= ` 
0 )
1181fneq2i 5339 . . . . . 6  |-  (  seq  0 (  +  , 
( G `  z
) )  Fn  NN0  <->  seq  0 (  +  , 
( G `  z
) )  Fn  ( ZZ>=
`  0 ) )
119117, 118mpbir 200 . . . . 5  |-  seq  0
(  +  ,  ( G `  z ) )  Fn  NN0
120 dffn5 5568 . . . . 5  |-  (  seq  0 (  +  , 
( G `  z
) )  Fn  NN0  <->  seq  0 (  +  , 
( G `  z
) )  =  ( m  e.  NN0  |->  (  seq  0 (  +  , 
( G `  z
) ) `  m
) ) )
121119, 120mpbi 199 . . . 4  |-  seq  0
(  +  ,  ( G `  z ) )  =  ( m  e.  NN0  |->  (  seq  0 (  +  , 
( G `  z
) ) `  m
) )
122115, 121syl6eqr 2333 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
m  e.  NN0  |->  ( ( ( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m ) `  z
) )  =  seq  0 (  +  , 
( G `  z
) ) )
123 fvres 5542 . . . 4  |-  ( z  e.  B  ->  (
( F  |`  B ) `
 z )  =  ( F `  z
) )
124123adantl 452 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( F  |`  B ) `
 z )  =  ( F `  z
) )
12592, 122, 1243brtr4d 4053 . 2  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
m  e.  NN0  |->  ( ( ( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m ) `  z
) )  ~~>  ( ( F  |`  B ) `  z ) )
12697adantl 452 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
( k  e.  NN0  |->  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... k ) ( ( G `  y ) `  i
) ) ) `  m )  =  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( G `  y
) `  i )
) )
127126oveq2d 5874 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  ( CC  _D  ( ( k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) `
 m ) )  =  ( CC  _D  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) ) )
128 eqid 2283 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
129128cnfldtop 18293 . . . . . . . 8  |-  ( TopOpen ` fld )  e.  Top
130128cnfldtopon 18292 . . . . . . . . . 10  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
131130toponunii 16670 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
132131restid 13338 . . . . . . . 8  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
133129, 132ax-mp 8 . . . . . . 7  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
134133eqcomi 2287 . . . . . 6  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
1353a1i 10 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  CC  e.  { RR ,  CC } )
136128cnfldtopn 18291 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
137136blopn 18046 . . . . . . . . 9  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  e.  ( TopOpen ` fld )
)
13813, 15, 22, 137syl3anc 1182 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  e.  ( TopOpen ` fld )
)
13911, 138syl5eqel 2367 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  B  e.  ( TopOpen ` fld ) )
140139adantr 451 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  B  e.  ( TopOpen ` fld ) )
141 fzfid 11035 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
0 ... m )  e. 
Fin )
1429ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  A : NN0 --> CC )
1431423ad2ant1 976 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  A : NN0
--> CC )
14425adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  B  C_  CC )
145144sselda 3180 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  y  e.  B
)  ->  y  e.  CC )
1461453adant2 974 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  y  e.  CC )
1478, 143, 146psergf 19788 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  ( G `  y ) : NN0 --> CC )
1481103ad2ant2 977 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  i  e.  NN0 )
149147, 148, 30syl2anc 642 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  ( ( G `  y ) `  i )  e.  CC )
1503a1i 10 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  CC  e.  { RR ,  CC }
)
151 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( A : NN0 --> CC  /\  i  e.  NN0 )  -> 
( A `  i
)  e.  CC )
152142, 110, 151syl2an 463 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( A `  i )  e.  CC )
153152adantr 451 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  ( A `  i )  e.  CC )
154145adantlr 695 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  y  e.  CC )
155 id 19 . . . . . . . . . . 11  |-  ( y  e.  CC  ->  y  e.  CC )
156110adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  i  e.  NN0 )
157 expcl 11121 . . . . . . . . . . 11  |-  ( ( y  e.  CC  /\  i  e.  NN0 )  -> 
( y ^ i
)  e.  CC )
158155, 156, 157syl2anr 464 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  CC )  ->  (
y ^ i )  e.  CC )
159154, 158syldan 456 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
y ^ i )  e.  CC )
160153, 159mulcld 8855 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( A `  i
)  x.  ( y ^ i ) )  e.  CC )
161 ovex 5883 . . . . . . . . 9  |-  ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ (
i  -  1 ) ) ) ) )  e.  _V
162161a1i 10 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( A `  i
)  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^
( i  -  1 ) ) ) ) )  e.  _V )
163 c0ex 8832 . . . . . . . . . . 11  |-  0  e.  _V
164 ovex 5883 . . . . . . . . . . 11  |-  ( i  x.  ( y ^
( i  -  1 ) ) )  e. 
_V
165163, 164ifex 3623 . . . . . . . . . 10  |-  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^
( i  -  1 ) ) ) )  e.  _V
166165a1i 10 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  e.  _V )
167165a1i 10 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  CC )  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  e.  _V )
168 dvexp2 19303 . . . . . . . . . . 11  |-  ( i  e.  NN0  ->  ( CC 
_D  ( y  e.  CC  |->  ( y ^
i ) ) )  =  ( y  e.  CC  |->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ (
i  -  1 ) ) ) ) ) )
169156, 168syl 15 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( CC  _D  ( y  e.  CC  |->  ( y ^ i
) ) )  =  ( y  e.  CC  |->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) )
17025ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  B  C_  CC )
171139ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  B  e.  ( TopOpen ` fld ) )
172150, 158, 167, 169, 170, 134, 128, 171dvmptres 19312 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( CC  _D  ( y  e.  B  |->  ( y ^ i
) ) )  =  ( y  e.  B  |->  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) ) )
173150, 159, 166, 172, 152dvmptcmul 19313 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( CC  _D  ( y  e.  B  |->  ( ( A `  i )  x.  (
y ^ i ) ) ) )  =  ( y  e.  B  |->  ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) )
174150, 160, 162, 173dvmptcl 19308 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( A `  i
)  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^
( i  -  1 ) ) ) ) )  e.  CC )
1751743impa 1146 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) )  e.  CC )
176110ad2antlr 707 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  i  e.  NN0 )
1778pserval2 19787 . . . . . . . . . 10  |-  ( ( y  e.  CC  /\  i  e.  NN0 )  -> 
( ( G `  y ) `  i
)  =  ( ( A `  i )  x.  ( y ^
i ) ) )
178154, 176, 177syl2anc 642 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( G `  y
) `  i )  =  ( ( A `
 i )  x.  ( y ^ i
) ) )
179178mpteq2dva 4106 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( y  e.  B  |->  ( ( G `  y ) `
 i ) )  =  ( y  e.  B  |->  ( ( A `
 i )  x.  ( y ^ i
) ) ) )
180179oveq2d 5874 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( CC  _D  ( y  e.  B  |->  ( ( G `  y ) `  i
) ) )  =  ( CC  _D  (
y  e.  B  |->  ( ( A `  i
)  x.  ( y ^ i ) ) ) ) )
181180, 173eqtrd 2315 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( CC  _D  ( y  e.  B  |->  ( ( G `  y ) `  i
) ) )  =  ( y  e.  B  |->  ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) )
182134, 128, 135, 140, 141, 149, 175, 181dvmptfsum 19322 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  ( CC  _D  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) )
183127, 182eqtrd 2315 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  ( CC  _D  ( ( k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) `
 m ) )  =  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) )
184183mpteq2dva 4106 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  (
m  e.  NN0  |->  ( CC 
_D  ( ( k  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i ) ) ) `
 m ) ) )  =  ( m  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( A `
 i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) ) ) ) )
185 nnssnn0 9968 . . . . . 6  |-  NN  C_  NN0
186 resmpt 5000 . . . . . 6  |-  ( NN  C_  NN0  ->  ( (
m  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( A `
 i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) ) ) )  |`  NN )  =  ( m  e.  NN  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) ) )
187185, 186ax-mp 8 . . . . 5  |-  ( ( m  e.  NN0  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( A `
 i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) ) ) )  |`  NN )  =  ( m  e.  NN  |->  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m ) ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) ) ) ) )
188 oveq1 5865 . . . . . . . . . . . 12  |-  ( a  =  x  ->  (
a ^ i )  =  ( x ^
i ) )
189188oveq2d 5874 . . . . . . . . . . 11  |-  ( a  =  x  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( x ^ i
) ) )
190189mpteq2dv 4107 . . . . . . . . . 10  |-  ( a  =  x  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( x ^ i
) ) ) )
191 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  (
i  +  1 )  =  ( n  + 
1 ) )
192191fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  ( A `  ( i  +  1 ) )  =  ( A `  ( n  +  1
) ) )
193191, 192oveq12d 5876 . . . . . . . . . . . . 13  |-  ( i  =  n  ->  (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  =  ( ( n  +  1 )  x.  ( A `  (
n  +  1 ) ) ) )
194 oveq2 5866 . . . . . . . . . . . . 13  |-  ( i  =  n  ->  (
x ^ i )  =  ( x ^
n ) )
195193, 194oveq12d 5876 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( x ^ i ) )  =  ( ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  x.  ( x ^ n
) ) )
196195cbvmptv 4111 . . . . . . . . . . 11  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( x ^
i ) ) )  =  ( n  e. 
NN0  |->  ( ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  x.  ( x ^ n
) ) )
197 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
m  +  1 )  =  ( n  + 
1 ) )
198197fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  ( A `  ( m  +  1 ) )  =  ( A `  ( n  +  1
) ) )
199197, 198oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
( m  +  1 )  x.  ( A `
 ( m  + 
1 ) ) )  =  ( ( n  +  1 )  x.  ( A `  (
n  +  1 ) ) ) )
200 eqid 2283 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) )  =  ( m  e. 
NN0  |->  ( ( m  +  1 )  x.  ( A `  (
m  +  1 ) ) ) )
201 ovex 5883 . . . . . . . . . . . . . 14  |-  ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  e. 
_V
202199, 200, 201fvmpt 5602 . . . . . . . . . . . . 13  |-  ( n  e.  NN0  ->  ( ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) `
 n )  =  ( ( n  + 
1 )  x.  ( A `  ( n  +  1 ) ) ) )
203202oveq1d 5873 . . . . . . . . . . . 12  |-  ( n  e.  NN0  ->  ( ( ( m  e.  NN0  |->  ( ( m  + 
1 )  x.  ( A `  ( m  +  1 ) ) ) ) `  n
)  x.  ( x ^ n ) )  =  ( ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  x.  ( x ^ n
) ) )
204203mpteq2ia 4102 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( ( ( m  e.  NN0  |->  ( ( m  + 
1 )  x.  ( A `  ( m  +  1 ) ) ) ) `  n
)  x.  ( x ^ n ) ) )  =  ( n  e.  NN0  |->  ( ( ( n  +  1 )  x.  ( A `
 ( n  + 
1 ) ) )  x.  ( x ^
n ) ) )
205196, 204eqtr4i 2306 . . . . . . . . . 10  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( x ^
i ) ) )  =  ( n  e. 
NN0  |->  ( ( ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) `
 n )  x.  ( x ^ n
) ) )
206190, 205syl6eq 2331 . . . . . . . . 9  |-  ( a  =  x  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) )  =  ( n  e. 
NN0  |->  ( ( ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) `
 n )  x.  ( x ^ n
) ) ) )
207206cbvmptv 4111 . . . . . . . 8  |-  ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) )  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( ( m  e.  NN0  |->  ( ( m  + 
1 )  x.  ( A `  ( m  +  1 ) ) ) ) `  n
)  x.  ( x ^ n ) ) ) )
208 fveq2 5525 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y )  =  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  z ) )
209208fveq1d 5527 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) `  k )  =  ( ( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 z ) `  k ) )
210209sumeq2sdv 12177 . . . . . . . . 9  |-  ( y  =  z  ->  sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) `
 k )  = 
sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) `
 k ) )
211210cbvmptv 4111 . . . . . . . 8  |-  ( y  e.  B  |->  sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) `
 k ) )  =  ( z  e.  B  |->  sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) `
 k ) )
212 peano2nn0 10004 . . . . . . . . . . . 12  |-  ( m  e.  NN0  ->  ( m  +  1 )  e. 
NN0 )
213212adantl 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  NN0 )
214213nn0cnd 10020 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  CC )
215 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( A : NN0 --> CC  /\  ( m  +  1
)  e.  NN0 )  ->  ( A `  (
m  +  1 ) )  e.  CC )
216142, 213, 215syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  ( A `  ( m  +  1 ) )  e.  CC )
217214, 216mulcld 8855 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  x.  ( A `
 ( m  + 
1 ) ) )  e.  CC )
218217, 200fmptd 5684 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) : NN0 --> CC )
219 fveq2 5525 . . . . . . . . . . . 12  |-  ( r  =  j  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  r )  =  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  j ) )
220219seqeq3d 11054 . . . . . . . . . . 11  |-  ( r  =  j  ->  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 r ) )  =  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  j ) ) )
221220eleq1d 2349 . . . . . . . . . 10  |-  ( r  =  j  ->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 r ) )  e.  dom  ~~>  <->  seq  0
(  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  j ) )  e. 
dom 
~~>  ) )
222221cbvrabv 2787 . . . . . . . . 9  |-  { r  e.  RR  |  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 r ) )  e.  dom  ~~>  }  =  { j  e.  RR  |  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  j ) )  e.  dom  ~~>  }
223222supeq1i 7200 . . . . . . . 8  |-  sup ( { r  e.  RR  |  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )  =  sup ( { j  e.  RR  |  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 j ) )  e.  dom  ~~>  } ,  RR* ,  <  )
224208seqeq3d 11054 . . . . . . . . . . . 12  |-  ( y  =  z  ->  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) )  =  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) ) )
225224fveq1d 5527 . . . . . . . . . . 11  |-  ( y  =  z  ->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j )  =  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) ) `  j ) )
226225cbvmptv 4111 . . . . . . . . . 10  |-  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) )  =  ( z  e.  B  |->  (  seq  0
(  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  z ) ) `  j ) )
227 fveq2 5525 . . . . . . . . . . 11  |-  ( j  =  m  ->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 z ) ) `
 j )  =  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) ) `  m ) )
228227mpteq2dv 4107 . . . . . . . . . 10  |-  ( j  =  m  ->  (
z  e.  B  |->  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  z ) ) `  j ) )  =  ( z  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 z ) ) `
 m ) ) )
229226, 228syl5eq 2327 . . . . . . . . 9  |-  ( j  =  m  ->  (
y  e.  B  |->  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) `  j ) )  =  ( z  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 z ) ) `
 m ) ) )
230229cbvmptv 4111 . . . . . . . 8  |-  ( j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) )  =  ( m  e.  NN0  |->  ( z  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 z ) ) `
 m ) ) )
23121rpred 10390 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e.  RR )
2328, 16, 9, 17, 18, 19psercnlem1 19801 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  ( M  e.  RR+  /\  ( abs `  a )  < 
M  /\  M  <  R ) )
233232simp1d 967 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR+ )
234233rpxrd 10391 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR* )
235207, 218, 223radcnvcl 19793 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  sup ( { r  e.  RR  |  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )  e.  ( 0 [,]  +oo ) )
23662, 235sseldi 3178 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  sup ( { r  e.  RR  |  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )  e. 
RR* )
237232simp2d 968 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
M )
238 cnvimass 5033 . . . . . . . . . . . . . . . 16  |-  ( `' abs " ( 0 [,) R ) ) 
C_  dom  abs
239 absf 11821 . . . . . . . . . . . . . . . . 17  |-  abs : CC
--> RR
240239fdmi 5394 . . . . . . . . . . . . . . . 16  |-  dom  abs  =  CC
241238, 240sseqtri 3210 . . . . . . . . . . . . . . 15  |-  ( `' abs " ( 0 [,) R ) ) 
C_  CC
24218, 241eqsstri 3208 . . . . . . . . . . . . . 14  |-  S  C_  CC
243242a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  S  C_  CC )
244243sselda 3180 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  a  e.  CC )
245244abscld 11918 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  e.  RR )
246233rpred 10390 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR )
247 avglt2 9950 . . . . . . . . . . 11  |-  ( ( ( abs `  a
)  e.  RR  /\  M  e.  RR )  ->  ( ( abs `  a
)  <  M  <->  ( (
( abs `  a
)  +  M )  /  2 )  < 
M ) )
248245, 246, 247syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  <  M  <->  ( (
( abs `  a
)  +  M )  /  2 )  < 
M ) )
249237, 248mpbid 201 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
M )
250233rpge0d 10394 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  0  <_  M )
251246, 250absidd 11905 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  M )  =  M )
252233rpcnd 10392 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  CC )
253 oveq1 5865 . . . . . . . . . . . . . . . . 17  |-  ( w  =  M  ->  (
w ^ i )  =  ( M ^
i ) )
254253oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( w  =  M  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( w ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( M ^ i
) ) )
255254mpteq2dv 4107 . . . . . . . . . . . . . . 15  |-  ( w  =  M  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( w ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( M ^ i
) ) ) )
256 oveq1 5865 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  w  ->  (
a ^ i )  =  ( w ^
i ) )
257256oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( a  =  w  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( w ^ i
) ) )
258257mpteq2dv 4107 . . . . . . . . . . . . . . . 16  |-  ( a  =  w  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( w ^ i
) ) ) )
259258cbvmptv 4111 . . . . . . . . . . . . . . 15  |-  ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) )  =  ( w  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( w ^
i ) ) ) )
260 nn0ex 9971 . . . . . . . . . . . . . . . 16  |-  NN0  e.  _V
261260mptex 5746 . . . . . . . . . . . . . . 15  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) )  e.  _V
262255, 259, 261fvmpt 5602 . . . . . . . . . . . . . 14  |-  ( M  e.  CC  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  M )  =  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) ) )
263252, 262syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  M )  =  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) ) )
264263seqeq3d 11054 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 M ) )  =  seq  0 (  +  ,  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) ) ) )
265 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  ( A `  n )  =  ( A `  i ) )
266 oveq2 5866 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
x ^ n )  =  ( x ^
i ) )
267265, 266oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 i )  x.  ( x ^ i
) ) )
268267cbvmptv 4111 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( x ^ i
) ) )
269 oveq1 5865 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
x ^ i )  =  ( y ^
i ) )
270269oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A `  i
)  x.  ( x ^ i ) )  =  ( ( A `
 i )  x.  ( y ^ i
) ) )
271270mpteq2dv 4107 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
i  e.  NN0  |->  ( ( A `  i )  x.  ( x ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( y ^ i
) ) ) )
272268, 271syl5eq 2327 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( y ^ i
) ) ) )
273272cbvmptv 4111 . . . . . . . . . . . . . 14  |-  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) ) )  =  ( y  e.  CC  |->  ( i  e.  NN0  |->  ( ( A `  i )  x.  ( y ^
i ) ) ) )
2748, 273eqtri 2303 . . . . . . . . . . . . 13  |-  G  =  ( y  e.  CC  |->  ( i  e.  NN0  |->  ( ( A `  i )  x.  (
y ^ i ) ) ) )
275 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( r  =  s  ->  ( G `  r )  =  ( G `  s ) )
276275seqeq3d 11054 . . . . . . . . . . . . . . . . 17  |-  ( r  =  s  ->  seq  0 (  +  , 
( G `  r
) )  =  seq  0 (  +  , 
( G `  s
) ) )
277276eleq1d 2349 . . . . . . . . . . . . . . . 16  |-  ( r  =  s  ->  (  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  <->  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  ) )
278277cbvrabv 2787 . . . . . . . . . . . . . . 15  |-  { r  e.  RR  |  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  }  =  { s  e.  RR  |  seq  0
(  +  ,  ( G `  s ) )  e.  dom  ~~>  }
279278supeq1i 7200 . . . . . . . . . . . . . 14  |-  sup ( { r  e.  RR  |  seq  0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  =  sup ( { s  e.  RR  |  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  } ,  RR* ,  <  )
28017, 279eqtri 2303 . . . . . . . . . . . . 13  |-  R  =  sup ( { s  e.  RR  |  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  } ,  RR* ,  <  )
281 eqid 2283 . . . . . . . . . . . . 13  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( M ^ i
) ) )
2829adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  A : NN0 --> CC )
283232simp3d 969 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  S )  ->  M  <  R )
284251, 283eqbrtrd 4043 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  M )  < 
R )
285274, 280, 281, 282, 252, 284dvradcnv 19797 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  seq  0 (  +  , 
( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  ( M ^ i ) ) ) )  e.  dom  ~~>  )
286264, 285eqeltrd 2357 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 M ) )  e.  dom  ~~>  )
287207, 218, 223, 252, 286radcnvle 19796 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  M )  <_  sup ( { r  e.  RR  |  seq  0
(  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) )
288251, 287eqbrtrrd 4045 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  M  <_  sup ( { r  e.  RR  |  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 r ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )
28922, 234, 236, 249, 288xrltletrd 10492 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  <  sup ( { r  e.  RR  |  seq  0
(  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) )
290207, 211, 218, 223, 230, 231, 289, 47pserulm 19798 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  (
j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) ) ( ~~> u `  B ) ( y  e.  B  |->  sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) `
 k ) ) )
29125sselda 3180 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  y  e.  CC )
292 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( a  =  y  ->  (
a ^ i )  =  ( y ^
i ) )
293292oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( a  =  y  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) )
294293mpteq2dv 4107 . . . . . . . . . . . . . 14  |-  ( a  =  y  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) ) )
295 eqid 2283 . . . . . . . . . . . . . 14  |-  ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) )  =  ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) )
296260mptex 5746 . . . . . . . . . . . . . 14  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) )  e.  _V
297294, 295, 296fvmpt 5602 . . . . . . . . . . . . 13  |-  ( y  e.  CC  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y )  =  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) )
298291, 297syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y )  =  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) )
299298adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  k  e.  NN0 )  ->  ( (
a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) ) )
300299fveq1d 5527 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  k  e.  NN0 )  ->  ( (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y ) `  k
)  =  ( ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) `
 k ) )
301 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
302301fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  ( A `  ( i  +  1 ) )  =  ( A `  ( k  +  1 ) ) )
303301, 302oveq12d 5876 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  =  ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) ) )
304 oveq2 5866 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
y ^ i )  =  ( y ^
k ) )
305303, 304oveq12d 5876 . . . . . . . . . . . 12  |-  ( i  =  k  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i ) )  =  ( ( ( k  +  1 )  x.  ( A `  ( k  +  1 ) ) )  x.  ( y ^ k
) ) )
306 eqid 2283 . . . . . . . . . . . 12  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) )
307 ovex 5883 . . . . . . . . . . . 12  |-  ( ( ( k  +  1 )  x.  ( A `
 ( k  +  1 ) ) )  x.  ( y ^
k ) )  e. 
_V
308305, 306, 307fvmpt 5602 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) `
 k )  =  ( ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) )  x.  (
y ^ k ) ) )
309308adantl 452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  k  e.  NN0 )  ->  ( (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) `
 k )  =  ( ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) )  x.  (
y ^ k ) ) )
310300, 309eqtrd 2315 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  k  e.  NN0 )  ->  ( (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y ) `  k
)  =  ( ( ( k  +  1 )  x.  ( A `
 ( k  +  1 ) ) )  x.  ( y ^
k ) ) )
311310sumeq2dv 12176 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  sum_ k  e.  NN0  ( ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) `
 k )  = 
sum_ k  e.  NN0  ( ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) )  x.  (
y ^ k ) ) )
312311mpteq2dva 4106 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  (
y  e.  B  |->  sum_ k  e.  NN0  (
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) `  k ) )  =  ( y  e.  B  |-> 
sum_ k  e.  NN0  ( ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) )  x.  (
y ^ k ) ) ) )
313290, 312breqtrd 4047 . . . . . 6  |-  ( (
ph  /\  a  e.  S )  ->  (
j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) ) ( ~~> u `  B ) ( y  e.  B  |->  sum_ k  e.  NN0  ( ( ( k  +  1 )  x.  ( A `  ( k  +  1 ) ) )  x.  ( y ^ k
) ) ) )
314 nnuz 10263 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
315 1e0p1 10152 . . . . . . . . 9  |-  1  =  ( 0  +  1 )
316315fveq2i 5528 . . . . . . . 8  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
317314, 316eqtri 2303 . . . . . . 7  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
318 1z 10053 . . . . . . . 8  |-  1  e.  ZZ
319318a1i 10 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  1  e.  ZZ )
3205a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  0  e.  ZZ )
321 peano2nn0 10004 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
322321nn0cnd 10020 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  NN0  ->  ( i  +  1 )  e.  CC )
323322adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( i  +  1 )  e.  CC )
3249ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  A : NN0 --> CC )
325 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A : NN0 --> CC  /\  ( i  +  1 )  e.  NN0 )  ->  ( A `  (
i  +  1 ) )  e.  CC )
326324, 321, 325syl2an 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( A `  ( i  +  1 ) )  e.  CC )
327323, 326mulcld 8855 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( (
i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  e.  CC )
328291, 157sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( y ^ i )  e.  CC )
329327, 328mulcld 8855 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) )  e.  CC )
330329, 306fmptd 5684 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) : NN0 --> CC )
331298feq1d 5379 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  (
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) : NN0 --> CC  <->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) ) : NN0 --> CC ) )
332330, 331mpbird 223 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y ) : NN0 --> CC )
333 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( ( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) : NN0 --> CC  /\  m  e.  NN0 )  ->  (
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) `  m )  e.  CC )
334332, 333sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  m  e.  NN0 )  ->  ( (
( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y ) `  m
)  e.  CC )
3351, 320, 334serf 11074 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) : NN0 --> CC )
336 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) : NN0 --> CC  /\  j  e.  NN0 )  -> 
(  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) `  j )  e.  CC )
337335, 336sylan 457 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  j  e.  NN0 )  ->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j )  e.  CC )
338337an32s 779 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  j  e.  NN0 )  /\  y  e.  B
)  ->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j )  e.  CC )
339 eqid 2283 . . . . . . . . . 10  |-  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) )  =  ( y  e.  B  |->  (  seq  0
(  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  (
a ^ i ) ) ) ) `  y ) ) `  j ) )
340338, 339fmptd 5684 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  j  e.  NN0 )  ->  (
y  e.  B  |->  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) `  j ) ) : B --> CC )
3412, 36elmap 6796 . . . . . . . . 9  |-  ( ( y  e.  B  |->  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) `  j ) )  e.  ( CC 
^m  B )  <->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) : B --> CC )
342340, 341sylibr 203 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  j  e.  NN0 )  ->  (
y  e.  B  |->  (  seq  0 (  +  ,  ( ( a  e.  CC  |->  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( a ^
i ) ) ) ) `  y ) ) `  j ) )  e.  ( CC 
^m  B ) )
343 eqid 2283 . . . . . . . 8  |-  ( j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) )  =  ( j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) )
344342, 343fmptd 5684 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  (
j  e.  NN0  |->  ( y  e.  B  |->  (  seq  0 (  +  , 
( ( a  e.  CC  |->  ( i  e. 
NN0  |->  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i
) ) ) ) `
 y ) ) `
 j ) ) ) : NN0 --> ( CC 
^m  B ) )
345 elfznn 10819 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... m )  ->  i  e.  NN )
346345nnne0d 9790 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... m )  ->  i  =/=  0 )
347346neneqd 2462 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... m )  ->  -.  i  =  0 )
348 iffalse 3572 . . . . . . . . . . . . . . 15  |-  ( -.  i  =  0  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  =  ( i  x.  ( y ^
( i  -  1 ) ) ) )
349347, 348syl 15 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... m )  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  =  ( i  x.  ( y ^
( i  -  1 ) ) ) )
350349oveq2d 5874 . . . . . . . . . . . . 13  |-  ( i  e.  ( 1 ... m )  ->  (
( A `  i
)  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^
( i  -  1 ) ) ) ) )  =  ( ( A `  i )  x.  ( i  x.  ( y ^ (
i  -  1 ) ) ) ) )
351350sumeq2i 12172 . . . . . . . . . . . 12  |-  sum_ i  e.  ( 1 ... m
) ( ( A `
 i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  (
y ^ ( i  -  1 ) ) ) ) )  = 
sum_ i  e.  ( 1 ... m ) ( ( A `  i )  x.  (
i  x.  ( y ^ ( i  - 
1 ) ) ) )
352318a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  1  e.  ZZ )
353 nnz 10045 . . . . . . . . . . . . . 14  |-  ( m  e.  NN  ->  m  e.  ZZ )
354353ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  m  e.  ZZ )
355282ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  A : NN0
--> CC )
356345nnnn0d 10018 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... m )  ->  i  e.  NN0 )
357355, 356, 151syl2an 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  ( A `  i )  e.  CC )
358345adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  i  e.  NN )
359358nncnd 9762 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  i  e.  CC )
360291adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y