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

Theorem pserdvlem2 20297
Description: Lemma for pserdv 20298. (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 10476 . 2  |-  NN0  =  ( ZZ>= `  0 )
2 cnex 9027 . . . 4  |-  CC  e.  _V
32prid2 3873 . . 3  |-  CC  e.  { RR ,  CC }
43a1i 11 . 2  |-  ( (
ph  /\  a  e.  S )  ->  CC  e.  { RR ,  CC } )
5 0z 10249 . . 3  |-  0  e.  ZZ
65a1i 11 . 2  |-  ( (
ph  /\  a  e.  S )  ->  0  e.  ZZ )
7 fzfid 11267 . . . . . 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 711 . . . . . . . 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 18760 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
1312a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
14 0cn 9040 . . . . . . . . . . . . 13  |-  0  e.  CC
1514a1i 11 . . . . . . . . . . . 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 20296 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( ( abs `  a )  +  M
)  /  2 )  e.  RR+  /\  ( abs `  a )  < 
( ( ( abs `  a )  +  M
)  /  2 )  /\  ( ( ( abs `  a )  +  M )  / 
2 )  <  R
) )
2120simp1d 969 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e.  RR+ )
2221rpxrd 10605 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )
23 blssm 18401 . . . . . . . . . . . 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 1184 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  CC )
2511, 24syl5eqss 3352 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  CC )
2625adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  ->  B  C_  CC )
2726sselda 3308 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  y  e.  CC )
288, 10, 27psergf 20281 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  ( G `  y ) : NN0 --> CC )
29 elfznn0 11039 . . . . . . 7  |-  ( i  e.  ( 0 ... k )  ->  i  e.  NN0 )
30 ffvelrn 5827 . . . . . . 7  |-  ( ( ( G `  y
) : NN0 --> CC  /\  i  e.  NN0 )  -> 
( ( G `  y ) `  i
)  e.  CC )
3128, 29, 30syl2an 464 . . . . . 6  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  /\  i  e.  ( 0 ... k
) )  ->  (
( G `  y
) `  i )  e.  CC )
327, 31fsumcl 12482 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  /\  y  e.  B
)  ->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i )  e.  CC )
33 eqid 2404 . . . . 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 5852 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  k  e.  NN0 )  ->  (
y  e.  B  |->  sum_ i  e.  ( 0 ... k ) ( ( G `  y
) `  i )
) : B --> CC )
35 ovex 6065 . . . . . 6  |-  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  e.  _V
3611, 35eqeltri 2474 . . . . 5  |-  B  e. 
_V
372, 36elmap 7001 . . . 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 204 . . 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 2404 . . 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 5852 . 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 20295 . . . . 5  |-  ( ph  ->  F  e.  ( S
-cn-> CC ) )
42 cncff 18876 . . . . 5  |-  ( F  e.  ( S -cn-> CC )  ->  F : S
--> CC )
4341, 42syl 16 . . . 4  |-  ( ph  ->  F : S --> CC )
4443adantr 452 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  F : S --> CC )
458, 16, 9, 17, 18, 20psercnlem2 20293 . . . . . 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 970 . . . . 5  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  C_  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M
)  /  2 ) ) ) )
4711, 46syl5eqss 3352 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  ( `' abs " (
0 [,] ( ( ( abs `  a
)  +  M )  /  2 ) ) ) )
4845simp3d 971 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  ( `' abs " ( 0 [,] ( ( ( abs `  a )  +  M )  / 
2 ) ) ) 
C_  S )
4947, 48sstrd 3318 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  B  C_  S )
50 fssres 5569 . . 3  |-  ( ( F : S --> CC  /\  B  C_  S )  -> 
( F  |`  B ) : B --> CC )
5144, 49, 50syl2anc 643 . 2  |-  ( (
ph  /\  a  e.  S )  ->  ( F  |`  B ) : B --> CC )
525a1i 11 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  0  e.  ZZ )
53 eqidd 2405 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  j  e.  NN0 )  ->  ( ( G `  z ) `  j )  =  ( ( G `  z
) `  j )
)
549ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  A : NN0 --> CC )
5525sselda 3308 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  CC )
568, 54, 55psergf 20281 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( G `  z ) : NN0 --> CC )
5756ffvelrnda 5829 . . . . 5  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  j  e.  NN0 )  ->  ( ( G `  z ) `  j )  e.  CC )
5855abscld 12193 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  e.  RR )
5958rexrd 9090 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  e. 
RR* )
6022adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e. 
RR* )
61 iccssxr 10949 . . . . . . . . 9  |-  ( 0 [,]  +oo )  C_  RR*
628, 9, 17radcnvcl 20286 . . . . . . . . 9  |-  ( ph  ->  R  e.  ( 0 [,]  +oo ) )
6361, 62sseldi 3306 . . . . . . . 8  |-  ( ph  ->  R  e.  RR* )
6463ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  R  e.  RR* )
65 eqid 2404 . . . . . . . . . . 11  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
6665cnmetdval 18758 . . . . . . . . . 10  |-  ( ( z  e.  CC  /\  0  e.  CC )  ->  ( z ( abs 
o.  -  ) 0 )  =  ( abs `  ( z  -  0 ) ) )
6755, 14, 66sylancl 644 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  =  ( abs `  (
z  -  0 ) ) )
6855subid1d 9356 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z  -  0 )  =  z )
6968fveq2d 5691 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  ( z  - 
0 ) )  =  ( abs `  z
) )
7067, 69eqtrd 2436 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  =  ( abs `  z
) )
71 simpr 448 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  B )
7271, 11syl6eleq 2494 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a
)  +  M )  /  2 ) ) )
7312a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
7414a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  0  e.  CC )
75 elbl3 18375 . . . . . . . . . 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 ) ) )
7673, 60, 74, 55, 75syl22anc 1185 . . . . . . . . 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 ) ) )
7772, 76mpbid 202 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
z ( abs  o.  -  ) 0 )  <  ( ( ( abs `  a )  +  M )  / 
2 ) )
7870, 77eqbrtrrd 4194 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  < 
( ( ( abs `  a )  +  M
)  /  2 ) )
7920simp3d 971 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
R )
8079adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
R )
8159, 60, 64, 78, 80xrlttrd 10705 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( abs `  z )  < 
R )
828, 54, 17, 55, 81radcnvlt2 20288 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  e.  dom  ~~>  )
831, 52, 53, 57, 82isumclim2 12497 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  ~~>  sum_ j  e.  NN0  ( ( G `
 z ) `  j ) )
8449sselda 3308 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  z  e.  S )
85 fveq2 5687 . . . . . . . 8  |-  ( y  =  z  ->  ( G `  y )  =  ( G `  z ) )
8685fveq1d 5689 . . . . . . 7  |-  ( y  =  z  ->  (
( G `  y
) `  j )  =  ( ( G `
 z ) `  j ) )
8786sumeq2sdv 12453 . . . . . 6  |-  ( y  =  z  ->  sum_ j  e.  NN0  ( ( G `
 y ) `  j )  =  sum_ j  e.  NN0  ( ( G `  z ) `
 j ) )
88 sumex 12436 . . . . . 6  |-  sum_ j  e.  NN0  ( ( G `
 z ) `  j )  e.  _V
8987, 16, 88fvmpt 5765 . . . . 5  |-  ( z  e.  S  ->  ( F `  z )  =  sum_ j  e.  NN0  ( ( G `  z ) `  j
) )
9084, 89syl 16 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  ( F `  z )  =  sum_ j  e.  NN0  ( ( G `  z ) `  j
) )
9183, 90breqtrrd 4198 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  seq  0 (  +  , 
( G `  z
) )  ~~>  ( F `
 z ) )
92 oveq2 6048 . . . . . . . . . . 11  |-  ( k  =  m  ->  (
0 ... k )  =  ( 0 ... m
) )
9392sumeq1d 12450 . . . . . . . . . 10  |-  ( k  =  m  ->  sum_ i  e.  ( 0 ... k
) ( ( G `
 y ) `  i )  =  sum_ i  e.  ( 0 ... m ) ( ( G `  y
) `  i )
)
9493mpteq2dv 4256 . . . . . . . . 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 ) ) )
9536mptex 5925 . . . . . . . . 9  |-  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i ) )  e. 
_V
9694, 39, 95fvmpt 5765 . . . . . . . 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
) ) )
9796adantl 453 . . . . . . 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
) ) )
9897fveq1d 5689 . . . . . 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 )
)
9985fveq1d 5689 . . . . . . . . 9  |-  ( y  =  z  ->  (
( G `  y
) `  i )  =  ( ( G `
 z ) `  i ) )
10099sumeq2sdv 12453 . . . . . . . 8  |-  ( y  =  z  ->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i )  =  sum_ i  e.  ( 0 ... m ) ( ( G `  z
) `  i )
)
101 eqid 2404 . . . . . . . 8  |-  ( y  e.  B  |->  sum_ i  e.  ( 0 ... m
) ( ( G `
 y ) `  i ) )  =  ( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) )
102 sumex 12436 . . . . . . . 8  |-  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i )  e.  _V
103100, 101, 102fvmpt 5765 . . . . . . 7  |-  ( z  e.  B  ->  (
( y  e.  B  |-> 
sum_ i  e.  ( 0 ... m ) ( ( G `  y ) `  i
) ) `  z
)  =  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i ) )
104103ad2antlr 708 . . . . . 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
) )
105 eqidd 2405 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m
) )  ->  (
( G `  z
) `  i )  =  ( ( G `
 z ) `  i ) )
106 simpr 448 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  m  e.  NN0 )
107106, 1syl6eleq 2494 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  m  e.  ( ZZ>= `  0 )
)
10856adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  ( G `  z ) : NN0 --> CC )
109 elfznn0 11039 . . . . . . . 8  |-  ( i  e.  ( 0 ... m )  ->  i  e.  NN0 )
110 ffvelrn 5827 . . . . . . . 8  |-  ( ( ( G `  z
) : NN0 --> CC  /\  i  e.  NN0 )  -> 
( ( G `  z ) `  i
)  e.  CC )
111108, 109, 110syl2an 464 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m
) )  ->  (
( G `  z
) `  i )  e.  CC )
112105, 107, 111fsumser 12479 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  z  e.  B
)  /\  m  e.  NN0 )  ->  sum_ i  e.  ( 0 ... m
) ( ( G `
 z ) `  i )  =  (  seq  0 (  +  ,  ( G `  z ) ) `  m ) )
11398, 104, 1123eqtrd 2440 . . . . 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
) )
114113mpteq2dva 4255 . . . 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
) ) )
115 seqfn 11290 . . . . . . 7  |-  ( 0  e.  ZZ  ->  seq  0 (  +  , 
( G `  z
) )  Fn  ( ZZ>=
`  0 ) )
1165, 115ax-mp 8 . . . . . 6  |-  seq  0
(  +  ,  ( G `  z ) )  Fn  ( ZZ>= ` 
0 )
1171fneq2i 5499 . . . . . 6  |-  (  seq  0 (  +  , 
( G `  z
) )  Fn  NN0  <->  seq  0 (  +  , 
( G `  z
) )  Fn  ( ZZ>=
`  0 ) )
118116, 117mpbir 201 . . . . 5  |-  seq  0
(  +  ,  ( G `  z ) )  Fn  NN0
119 dffn5 5731 . . . . 5  |-  (  seq  0 (  +  , 
( G `  z
) )  Fn  NN0  <->  seq  0 (  +  , 
( G `  z
) )  =  ( m  e.  NN0  |->  (  seq  0 (  +  , 
( G `  z
) ) `  m
) ) )
120118, 119mpbi 200 . . . 4  |-  seq  0
(  +  ,  ( G `  z ) )  =  ( m  e.  NN0  |->  (  seq  0 (  +  , 
( G `  z
) ) `  m
) )
121114, 120syl6eqr 2454 . . 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
) ) )
122 fvres 5704 . . . 4  |-  ( z  e.  B  ->  (
( F  |`  B ) `
 z )  =  ( F `  z
) )
123122adantl 453 . . 3  |-  ( ( ( ph  /\  a  e.  S )  /\  z  e.  B )  ->  (
( F  |`  B ) `
 z )  =  ( F `  z
) )
12491, 121, 1233brtr4d 4202 . 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 ) )
12596adantl 453 . . . . . 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 )
) )
126125oveq2d 6056 . . . . 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
) ) ) )
127 eqid 2404 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
128127cnfldtop 18771 . . . . . . . 8  |-  ( TopOpen ` fld )  e.  Top
129127cnfldtopon 18770 . . . . . . . . . 10  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
130129toponunii 16952 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
131130restid 13616 . . . . . . . 8  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
132128, 131ax-mp 8 . . . . . . 7  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
133132eqcomi 2408 . . . . . 6  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
1343a1i 11 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  CC  e.  { RR ,  CC } )
135127cnfldtopn 18769 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
136135blopn 18483 . . . . . . . . 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 )
)
13713, 15, 22, 136syl3anc 1184 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  a )  +  M
)  /  2 ) )  e.  ( TopOpen ` fld )
)
13811, 137syl5eqel 2488 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  B  e.  ( TopOpen ` fld ) )
139138adantr 452 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  B  e.  ( TopOpen ` fld ) )
140 fzfid 11267 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
0 ... m )  e. 
Fin )
1419ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  A : NN0 --> CC )
1421413ad2ant1 978 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  A : NN0
--> CC )
14325adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  B  C_  CC )
144143sselda 3308 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  y  e.  B
)  ->  y  e.  CC )
1451443adant2 976 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  y  e.  CC )
1468, 142, 145psergf 20281 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  ( G `  y ) : NN0 --> CC )
1471093ad2ant2 979 . . . . . . 7  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  i  e.  NN0 )
148146, 147ffvelrnd 5830 . . . . . 6  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m )  /\  y  e.  B
)  ->  ( ( G `  y ) `  i )  e.  CC )
1493a1i 11 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  CC  e.  { RR ,  CC }
)
150 ffvelrn 5827 . . . . . . . . . . 11  |-  ( ( A : NN0 --> CC  /\  i  e.  NN0 )  -> 
( A `  i
)  e.  CC )
151141, 109, 150syl2an 464 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  ( A `  i )  e.  CC )
152151adantr 452 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  ( A `  i )  e.  CC )
153144adantlr 696 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  y  e.  CC )
154 id 20 . . . . . . . . . . 11  |-  ( y  e.  CC  ->  y  e.  CC )
155109adantl 453 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  i  e.  NN0 )
156 expcl 11354 . . . . . . . . . . 11  |-  ( ( y  e.  CC  /\  i  e.  NN0 )  -> 
( y ^ i
)  e.  CC )
157154, 155, 156syl2anr 465 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  CC )  ->  (
y ^ i )  e.  CC )
158153, 157syldan 457 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
y ^ i )  e.  CC )
159152, 158mulcld 9064 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( A `  i
)  x.  ( y ^ i ) )  e.  CC )
160 ovex 6065 . . . . . . . . 9  |-  ( ( A `  i )  x.  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ (
i  -  1 ) ) ) ) )  e.  _V
161160a1i 11 . . . . . . . 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 )
162 c0ex 9041 . . . . . . . . . . 11  |-  0  e.  _V
163 ovex 6065 . . . . . . . . . . 11  |-  ( i  x.  ( y ^
( i  -  1 ) ) )  e. 
_V
164162, 163ifex 3757 . . . . . . . . . 10  |-  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^
( i  -  1 ) ) ) )  e.  _V
165164a1i 11 . . . . . . . . 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 )
166164a1i 11 . . . . . . . . . 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 )
167 dvexp2 19793 . . . . . . . . . . 11  |-  ( i  e.  NN0  ->  ( CC 
_D  ( y  e.  CC  |->  ( y ^
i ) ) )  =  ( y  e.  CC  |->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ (
i  -  1 ) ) ) ) ) )
168155, 167syl 16 . . . . . . . . . 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 ) ) ) ) ) )
16925ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  B  C_  CC )
170138ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  ->  B  e.  ( TopOpen ` fld ) )
171149, 157, 166, 168, 169, 133, 127, 170dvmptres 19802 . . . . . . . . 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 ) ) ) ) ) )
172149, 158, 165, 171, 151dvmptcmul 19803 . . . . . . . 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 ) ) ) ) ) ) )
173149, 159, 161, 172dvmptcl 19798 . . . . . . 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 )
1741733impa 1148 . . . . . 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 )
175109ad2antlr 708 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  i  e.  NN0 )
1768pserval2 20280 . . . . . . . . . 10  |-  ( ( y  e.  CC  /\  i  e.  NN0 )  -> 
( ( G `  y ) `  i
)  =  ( ( A `  i )  x.  ( y ^
i ) ) )
177153, 175, 176syl2anc 643 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  /\  i  e.  ( 0 ... m ) )  /\  y  e.  B )  ->  (
( G `  y
) `  i )  =  ( ( A `
 i )  x.  ( y ^ i
) ) )
178177mpteq2dva 4255 . . . . . . . 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
) ) ) )
179178oveq2d 6056 . . . . . . 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 ) ) ) ) )
180179, 172eqtrd 2436 . . . . . 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 ) ) ) ) ) ) )
181133, 127, 134, 139, 140, 148, 174, 180dvmptfsum 19812 . . . . 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 ) ) ) ) ) ) )
182126, 181eqtrd 2436 . . . 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 ) ) ) ) ) ) )
183182mpteq2dva 4255 . . 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 ) ) ) ) ) ) ) )
184 nnssnn0 10180 . . . . . 6  |-  NN  C_  NN0
185 resmpt 5150 . . . . . 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 ) ) ) ) ) ) ) )
186184, 185ax-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 ) ) ) ) ) ) )
187 oveq1 6047 . . . . . . . . . . . 12  |-  ( a  =  x  ->  (
a ^ i )  =  ( x ^
i ) )
188187oveq2d 6056 . . . . . . . . . . 11  |-  ( a  =  x  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( x ^ i
) ) )
189188mpteq2dv 4256 . . . . . . . . . 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
) ) ) )
190 oveq1 6047 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  (
i  +  1 )  =  ( n  + 
1 ) )
191190fveq2d 5691 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  ( A `  ( i  +  1 ) )  =  ( A `  ( n  +  1
) ) )
192190, 191oveq12d 6058 . . . . . . . . . . . . 13  |-  ( i  =  n  ->  (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  =  ( ( n  +  1 )  x.  ( A `  (
n  +  1 ) ) ) )
193 oveq2 6048 . . . . . . . . . . . . 13  |-  ( i  =  n  ->  (
x ^ i )  =  ( x ^
n ) )
194192, 193oveq12d 6058 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( x ^ i ) )  =  ( ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  x.  ( x ^ n
) ) )
195194cbvmptv 4260 . . . . . . . . . . 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
) ) )
196 oveq1 6047 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
m  +  1 )  =  ( n  + 
1 ) )
197196fveq2d 5691 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  ( A `  ( m  +  1 ) )  =  ( A `  ( n  +  1
) ) )
198196, 197oveq12d 6058 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
( m  +  1 )  x.  ( A `
 ( m  + 
1 ) ) )  =  ( ( n  +  1 )  x.  ( A `  (
n  +  1 ) ) ) )
199 eqid 2404 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) )  =  ( m  e. 
NN0  |->  ( ( m  +  1 )  x.  ( A `  (
m  +  1 ) ) ) )
200 ovex 6065 . . . . . . . . . . . . . 14  |-  ( ( n  +  1 )  x.  ( A `  ( n  +  1
) ) )  e. 
_V
201198, 199, 200fvmpt 5765 . . . . . . . . . . . . 13  |-  ( n  e.  NN0  ->  ( ( m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) `
 n )  =  ( ( n  + 
1 )  x.  ( A `  ( n  +  1 ) ) ) )
202201oveq1d 6055 . . . . . . . . . . . 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
) ) )
203202mpteq2ia 4251 . . . . . . . . . . 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 ) ) )
204195, 203eqtr4i 2427 . . . . . . . . . 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
) ) )
205189, 204syl6eq 2452 . . . . . . . . 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
) ) ) )
206205cbvmptv 4260 . . . . . . . 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 ) ) ) )
207 fveq2 5687 . . . . . . . . . . 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 ) )
208207fveq1d 5689 . . . . . . . . . 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 ) )
209208sumeq2sdv 12453 . . . . . . . . 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 ) )
210209cbvmptv 4260 . . . . . . . 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 ) )
211 peano2nn0 10216 . . . . . . . . . . . 12  |-  ( m  e.  NN0  ->  ( m  +  1 )  e. 
NN0 )
212211adantl 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  NN0 )
213212nn0cnd 10232 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  CC )
214141, 212ffvelrnd 5830 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  ( A `  ( m  +  1 ) )  e.  CC )
215213, 214mulcld 9064 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  x.  ( A `
 ( m  + 
1 ) ) )  e.  CC )
216215, 199fmptd 5852 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
m  e.  NN0  |->  ( ( m  +  1 )  x.  ( A `  ( m  +  1
) ) ) ) : NN0 --> CC )
217 fveq2 5687 . . . . . . . . . . . 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 ) )
218217seqeq3d 11286 . . . . . . . . . . 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 ) ) )
219218eleq1d 2470 . . . . . . . . . 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 
~~>  ) )
220219cbvrabv 2915 . . . . . . . . 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  ~~>  }
221220supeq1i 7410 . . . . . . . 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* ,  <  )
222207seqeq3d 11286 . . . . . . . . . . . 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 ) ) )
223222fveq1d 5689 . . . . . . . . . . 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 ) )
224223cbvmptv 4260 . . . . . . . . . 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 ) )
225 fveq2 5687 . . . . . . . . . . 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 ) )
226225mpteq2dv 4256 . . . . . . . . . 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 ) ) )
227224, 226syl5eq 2448 . . . . . . . . 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 ) ) )
228227cbvmptv 4260 . . . . . . . 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 ) ) )
22921rpred 10604 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  e.  RR )
2308, 16, 9, 17, 18, 19psercnlem1 20294 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  ( M  e.  RR+  /\  ( abs `  a )  < 
M  /\  M  <  R ) )
231230simp1d 969 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR+ )
232231rpxrd 10605 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR* )
233206, 216, 221radcnvcl 20286 . . . . . . . . . 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 ) )
23461, 233sseldi 3306 . . . . . . . . 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* )
235230simp2d 970 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
M )
236 cnvimass 5183 . . . . . . . . . . . . . . . 16  |-  ( `' abs " ( 0 [,) R ) ) 
C_  dom  abs
237 absf 12096 . . . . . . . . . . . . . . . . 17  |-  abs : CC
--> RR
238237fdmi 5555 . . . . . . . . . . . . . . . 16  |-  dom  abs  =  CC
239236, 238sseqtri 3340 . . . . . . . . . . . . . . 15  |-  ( `' abs " ( 0 [,) R ) ) 
C_  CC
24018, 239eqsstri 3338 . . . . . . . . . . . . . 14  |-  S  C_  CC
241240a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  S  C_  CC )
242241sselda 3308 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  a  e.  CC )
243242abscld 12193 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  e.  RR )
244231rpred 10604 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR )
245 avglt2 10162 . . . . . . . . . . 11  |-  ( ( ( abs `  a
)  e.  RR  /\  M  e.  RR )  ->  ( ( abs `  a
)  <  M  <->  ( (
( abs `  a
)  +  M )  /  2 )  < 
M ) )
246243, 244, 245syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  <  M  <->  ( (
( abs `  a
)  +  M )  /  2 )  < 
M ) )
247235, 246mpbid 202 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  (
( ( abs `  a
)  +  M )  /  2 )  < 
M )
248231rpge0d 10608 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  0  <_  M )
249244, 248absidd 12180 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  M )  =  M )
250231rpcnd 10606 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  CC )
251 oveq1 6047 . . . . . . . . . . . . . . . . 17  |-  ( w  =  M  ->  (
w ^ i )  =  ( M ^
i ) )
252251oveq2d 6056 . . . . . . . . . . . . . . . 16  |-  ( w  =  M  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( w ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( M ^ i
) ) )
253252mpteq2dv 4256 . . . . . . . . . . . . . . 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
) ) ) )
254 oveq1 6047 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  w  ->  (
a ^ i )  =  ( w ^
i ) )
255254oveq2d 6056 . . . . . . . . . . . . . . . . 17  |-  ( a  =  w  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( w ^ i
) ) )
256255mpteq2dv 4256 . . . . . . . . . . . . . . . 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
) ) ) )
257256cbvmptv 4260 . . . . . . . . . . . . . . 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 ) ) ) )
258 nn0ex 10183 . . . . . . . . . . . . . . . 16  |-  NN0  e.  _V
259258mptex 5925 . . . . . . . . . . . . . . 15  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( M ^
i ) ) )  e.  _V
260253, 257, 259fvmpt 5765 . . . . . . . . . . . . . 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 ) ) ) )
261250, 260syl 16 . . . . . . . . . . . . 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 ) ) ) )
262261seqeq3d 11286 . . . . . . . . . . . 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 ) ) ) ) )
263 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  ( A `  n )  =  ( A `  i ) )
264 oveq2 6048 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
x ^ n )  =  ( x ^
i ) )
265263, 264oveq12d 6058 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 i )  x.  ( x ^ i
) ) )
266265cbvmptv 4260 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( x ^ i
) ) )
267 oveq1 6047 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
x ^ i )  =  ( y ^
i ) )
268267oveq2d 6056 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A `  i
)  x.  ( x ^ i ) )  =  ( ( A `
 i )  x.  ( y ^ i
) ) )
269268mpteq2dv 4256 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
i  e.  NN0  |->  ( ( A `  i )  x.  ( x ^
i ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( y ^ i
) ) ) )
270266, 269syl5eq 2448 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  =  ( i  e. 
NN0  |->  ( ( A `
 i )  x.  ( y ^ i
) ) ) )
271270cbvmptv 4260 . . . . . . . . . . . . . 14  |-  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) ) )  =  ( y  e.  CC  |->  ( i  e.  NN0  |->  ( ( A `  i )  x.  ( y ^
i ) ) ) )
2728, 271eqtri 2424 . . . . . . . . . . . . 13  |-  G  =  ( y  e.  CC  |->  ( i  e.  NN0  |->  ( ( A `  i )  x.  (
y ^ i ) ) ) )
273 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( r  =  s  ->  ( G `  r )  =  ( G `  s ) )
274273seqeq3d 11286 . . . . . . . . . . . . . . . . 17  |-  ( r  =  s  ->  seq  0 (  +  , 
( G `  r
) )  =  seq  0 (  +  , 
( G `  s
) ) )
275274eleq1d 2470 . . . . . . . . . . . . . . . 16  |-  ( r  =  s  ->  (  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  <->  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  ) )
276275cbvrabv 2915 . . . . . . . . . . . . . . 15  |-  { r  e.  RR  |  seq  0 (  +  , 
( G `  r
) )  e.  dom  ~~>  }  =  { s  e.  RR  |  seq  0
(  +  ,  ( G `  s ) )  e.  dom  ~~>  }
277276supeq1i 7410 . . . . . . . . . . . . . 14  |-  sup ( { r  e.  RR  |  seq  0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  =  sup ( { s  e.  RR  |  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  } ,  RR* ,  <  )
27817, 277eqtri 2424 . . . . . . . . . . . . 13  |-  R  =  sup ( { s  e.  RR  |  seq  0 (  +  , 
( G `  s
) )  e.  dom  ~~>  } ,  RR* ,  <  )
279 eqid 2404 . . . . . . . . . . . . 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
) ) )
2809adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  A : NN0 --> CC )
281230simp3d 971 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  S )  ->  M  <  R )
282249, 281eqbrtrd 4192 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  M )  < 
R )
283272, 278, 279, 280, 250, 282dvradcnv 20290 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  seq  0 (  +  , 
( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `  (
i  +  1 ) ) )  x.  ( M ^ i ) ) ) )  e.  dom  ~~>  )
284262, 283eqeltrd 2478 . . . . . . . . . . 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  ~~>  )
285206, 216, 221, 250, 284radcnvle 20289 . . . . . . . . . 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* ,  <  ) )
286249, 285eqbrtrrd 4194 . . . . . . . . 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* ,  <  ) )
28722, 232, 234, 247, 286xrltletrd 10707 . . . . . . . 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* ,  <  ) )
288206, 210, 216, 221, 228, 229, 287, 47pserulm 20291 . . . . . . 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 ) ) )
28925sselda 3308 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  y  e.  CC )
290 oveq1 6047 . . . . . . . . . . . . . . . 16  |-  ( a  =  y  ->  (
a ^ i )  =  ( y ^
i ) )
291290oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( a  =  y  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( a ^ i ) )  =  ( ( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i
) ) )
292291mpteq2dv 4256 . . . . . . . . . . . . . 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
) ) ) )
293 eqid 2404 . . . . . . . . . . . . . 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 ) ) ) )
294258mptex 5925 . . . . . . . . . . . . . 14  |-  ( i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) )  e.  _V
295292, 293, 294fvmpt 5765 . . . . . . . . . . . . 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 ) ) ) )
296289, 295syl 16 . . . . . . . . . . . 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 ) ) ) )
297296adantr 452 . . . . . . . . . . 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
) ) ) )
298297fveq1d 5689 . . . . . . . . . 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 ) )
299 oveq1 6047 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
300299fveq2d 5691 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  ( A `  ( i  +  1 ) )  =  ( A `  ( k  +  1 ) ) )
301299, 300oveq12d 6058 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  =  ( ( k  +  1 )  x.  ( A `  (
k  +  1 ) ) ) )
302 oveq2 6048 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
y ^ i )  =  ( y ^
k ) )
303301, 302oveq12d 6058 . . . . . . . . . . . 12  |-  ( i  =  k  ->  (
( ( i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  x.  ( y ^ i ) )  =  ( ( ( k  +  1 )  x.  ( A `  ( k  +  1 ) ) )  x.  ( y ^ k
) ) )
304 eqid 2404 . . . . . . . . . . . 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
) ) )
305 ovex 6065 . . . . . . . . . . . 12  |-  ( ( ( k  +  1 )  x.  ( A `
 ( k  +  1 ) ) )  x.  ( y ^
k ) )  e. 
_V
306303, 304, 305fvmpt 5765 . . . . . . . . . . 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 ) ) )
307306adantl 453 . . . . . . . . . 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 ) ) )
308298, 307eqtrd 2436 . . . . . . . . 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 ) ) )
309308sumeq2dv 12452 . . . . . . . 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 ) ) )
310309mpteq2dva 4255 . . . . . . 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 ) ) ) )
311288, 310breqtrd 4196 . . . . . 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
) ) ) )
312 nnuz 10477 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
313 1e0p1 10366 . . . . . . . . 9  |-  1  =  ( 0  +  1 )
314313fveq2i 5690 . . . . . . . 8  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
315312, 314eqtri 2424 . . . . . . 7  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
316 1z 10267 . . . . . . . 8  |-  1  e.  ZZ
317316a1i 11 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  1  e.  ZZ )
3185a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  0  e.  ZZ )
319 peano2nn0 10216 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
320319nn0cnd 10232 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  NN0  ->  ( i  +  1 )  e.  CC )
321320adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( i  +  1 )  e.  CC )
3229ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  A : NN0 --> CC )
323 ffvelrn 5827 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A : NN0 --> CC  /\  ( i  +  1 )  e.  NN0 )  ->  ( A `  (
i  +  1 ) )  e.  CC )
324322, 319, 323syl2an 464 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( A `  ( i  +  1 ) )  e.  CC )
325321, 324mulcld 9064 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( (
i  +  1 )  x.  ( A `  ( i  +  1 ) ) )  e.  CC )
326289, 156sylan 458 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( y ^ i )  e.  CC )
327325, 326mulcld 9064 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  S )  /\  y  e.  B
)  /\  i  e.  NN0 )  ->  ( (
( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) )  e.  CC )
328327, 304fmptd 5852 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  a  e.  S )  /\  y  e.  B )  ->  (
i  e.  NN0  |->  ( ( ( i  +  1 )  x.  ( A `
 ( i  +  1 ) ) )  x.  ( y ^
i ) ) ) : NN0 --> CC )
329296feq1d 5539 . . . . . . . . . . . . . . 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 ) )
330328, 329mpbird 224 . . . . . . . . . . . . . 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 )
331330ffvelrnda 5829 . . . . . . . . . . . . 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 )
3321, 318, 331serf 11306 . . . . . . . . . . . 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 )
333332ffvelrnda 5829 . . . . . . . . . . 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 )
334333an32s 780 . . . . . . . . . 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 )
335 eqid 2404 . . . . . . . . . 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 ) )
336334, 335fmptd 5852 . . . . . . . . 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 )
3372, 36elmap 7001 . . . . . . . . 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 )
338336, 337sylibr 204 . . . . . . . 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 ) )
339 eqid 2404 . . . . . . . 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 ) ) )
340338, 339fmptd 5852 . . . . . . 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 ) )
341 elfznn 11036 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... m )  ->  i  e.  NN )
342341nnne0d 10000 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... m )  ->  i  =/=  0 )
343342neneqd 2583 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... m )  ->  -.  i  =  0 )
344 iffalse 3706 . . . . . . . . . . . . . . 15  |-  ( -.  i  =  0  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  =  ( i  x.  ( y ^
( i  -  1 ) ) ) )
345343, 344syl 16 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... m )  ->  if ( i  =  0 ,  0 ,  ( i  x.  ( y ^ ( i  - 
1 ) ) ) )  =  ( i  x.  ( y ^
( i  -  1 ) ) ) )
346345oveq2d 6056 . . . . . . . . . . . . 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 ) ) ) ) )
347346sumeq2i 12448 . . . . . . . . . . . 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 ) ) ) )
348316a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  1  e.  ZZ )
349 nnz 10259 . . . . . . . . . . . . . 14  |-  ( m  e.  NN  ->  m  e.  ZZ )
350349ad2antlr 708 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  m  e.  ZZ )
351280ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  A : NN0
--> CC )
352341nnnn0d 10230 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... m )  ->  i  e.  NN0 )
353351, 352, 150syl2an 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  ( A `  i )  e.  CC )
354341adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  i  e.  NN )
355354nncnd 9972 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  i  e.  CC )
356289adantlr 696 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  ->  y  e.  CC )
357 nnm1nn0 10217 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  NN  ->  (
i  -  1 )  e.  NN0 )
358341, 357syl 16 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... m )  ->  (
i  -  1 )  e.  NN0 )
359 expcl 11354 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  CC  /\  ( i  -  1 )  e.  NN0 )  ->  ( y ^ (
i  -  1 ) )  e.  CC )
360356, 358, 359syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  (
y ^ ( i  -  1 ) )  e.  CC )
361355, 360mulcld 9064 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  (
i  x.  ( y ^ ( i  - 
1 ) ) )  e.  CC )
362353, 361mulcld 9064 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  a  e.  S )  /\  m  e.  NN )  /\  y  e.  B
)  /\  i  e.  ( 1 ... m
) )  ->  (
( A `  i
)  x.  ( i  x.  ( y ^
( i  -  1 ) ) ) )  e.  CC )
363 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( i  =  ( k  +  1 )  ->  ( A `  i )  =  ( A `  ( k  +  1 ) ) )
364 id 20 . . . . . . . . . . . . . . 15  |-  ( i  =  ( k  +  1 )  ->  i  =  ( k  +  1 ) )
365 oveq1 6047 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( k  +  1 )  ->  (
i  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
366365oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( i  =  ( k  +  1 )  ->  (
y ^ ( i  -  1 ) )  =  ( y ^
( ( k  +  1 )  -  1 ) ) )
367364, 366oveq12d 6058 . . . . . . . . . . . . . 14  |-  ( i  =  ( k  +  1 )  ->  (
i  x.  ( y ^ ( i  -