Metamath Proof Explorer

Theorem pserdvlem2

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses 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 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 pserf.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 pserf.f 
 |-  F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3 pserf.a 
 |-  ( ph -> A : NN0 --> CC )
4 pserf.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5 psercn.s 
 |-  S = ( `' abs " ( 0 [,) R ) )
6 psercn.m 
 |-  M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
7 pserdv.b 
 |-  B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 cnelprrecn 
 |-  CC e. { RR , CC }
10 9 a1i 
 |-  ( ( ph /\ a e. S ) -> CC e. { RR , CC } )
11 0zd 
 |-  ( ( ph /\ a e. S ) -> 0 e. ZZ )
12 fzfid 
 |-  ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> ( 0 ... k ) e. Fin )
13 3 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> A : NN0 --> CC )
14 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
15 0cnd 
 |-  ( ( ph /\ a e. S ) -> 0 e. CC )
16 1 2 3 4 5 6 pserdvlem1 
 |-  ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < R ) )
17 16 simp1d 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR+ )
18 17 rpxrd 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
19 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
20 14 15 18 19 mp3an2i 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
21 7 20 eqsstrid 
 |-  ( ( ph /\ a e. S ) -> B C_ CC )
22 21 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> B C_ CC )
23 22 sselda 
 |-  ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> y e. CC )
24 1 13 23 psergf 
 |-  ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> ( G ` y ) : NN0 --> CC )
25 elfznn0 
 |-  ( i e. ( 0 ... k ) -> i e. NN0 )
26 ffvelcdm 
 |-  ( ( ( G ` y ) : NN0 --> CC /\ i e. NN0 ) -> ( ( G ` y ) ` i ) e. CC )
27 24 25 26 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) /\ i e. ( 0 ... k ) ) -> ( ( G ` y ) ` i ) e. CC )
28 12 27 fsumcl 
 |-  ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) e. CC )
29 28 fmpttd 
 |-  ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> ( y e. B |-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) : B --> CC )
30 cnex 
 |-  CC e. _V
31 7 ovexi 
 |-  B e. _V
32 30 31 elmap 
 |-  ( ( 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 )
33 29 32 sylibr 
 |-  ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> ( y e. B |-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) e. ( CC ^m B ) )
34 33 fmpttd 
 |-  ( ( ph /\ a e. S ) -> ( k e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) : NN0 --> ( CC ^m B ) )
35 1 2 3 4 5 6 psercn 
 |-  ( ph -> F e. ( S -cn-> CC ) )
36 cncff 
 |-  ( F e. ( S -cn-> CC ) -> F : S --> CC )
37 35 36 syl 
 |-  ( ph -> F : S --> CC )
38 37 adantr 
 |-  ( ( ph /\ a e. S ) -> F : S --> CC )
39 1 2 3 4 5 16 psercnlem2 
 |-  ( ( 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 ) )
40 39 simp2d 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) )
41 7 40 eqsstrid 
 |-  ( ( ph /\ a e. S ) -> B C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) )
42 39 simp3d 
 |-  ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) C_ S )
43 41 42 sstrd 
 |-  ( ( ph /\ a e. S ) -> B C_ S )
44 38 43 fssresd 
 |-  ( ( ph /\ a e. S ) -> ( F |` B ) : B --> CC )
45 0zd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> 0 e. ZZ )
46 eqidd 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ j e. NN0 ) -> ( ( G ` z ) ` j ) = ( ( G ` z ) ` j ) )
47 3 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> A : NN0 --> CC )
48 21 sselda 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. CC )
49 1 47 48 psergf 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( G ` z ) : NN0 --> CC )
50 49 ffvelcdmda 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ j e. NN0 ) -> ( ( G ` z ) ` j ) e. CC )
51 48 abscld 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) e. RR )
52 51 rexrd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) e. RR* )
53 18 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
54 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
55 1 3 4 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
56 54 55 sselid 
 |-  ( ph -> R e. RR* )
57 56 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> R e. RR* )
58 0cn 
 |-  0 e. CC
59 eqid 
 |-  ( abs o. - ) = ( abs o. - )
60 59 cnmetdval 
 |-  ( ( z e. CC /\ 0 e. CC ) -> ( z ( abs o. - ) 0 ) = ( abs ` ( z - 0 ) ) )
61 48 58 60 sylancl 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) = ( abs ` ( z - 0 ) ) )
62 48 subid1d 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z - 0 ) = z )
63 62 fveq2d 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` ( z - 0 ) ) = ( abs ` z ) )
64 61 63 eqtrd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) = ( abs ` z ) )
65 simpr 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. B )
66 65 7 eleqtrdi 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) )
67 14 a1i 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs o. - ) e. ( *Met ` CC ) )
68 0cnd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> 0 e. CC )
69 elbl3 
 |-  ( ( ( ( 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 ) ) )
70 67 53 68 48 69 syl22anc 
 |-  ( ( ( 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 ) ) )
71 66 70 mpbid 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) < ( ( ( abs ` a ) + M ) / 2 ) )
72 64 71 eqbrtrrd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) < ( ( ( abs ` a ) + M ) / 2 ) )
73 16 simp3d 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < R )
74 73 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( ( abs ` a ) + M ) / 2 ) < R )
75 52 53 57 72 74 xrlttrd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) < R )
76 1 47 4 48 75 radcnvlt2 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) e. dom ~~> )
77 8 45 46 50 76 isumclim2 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) ~~> sum_ j e. NN0 ( ( G ` z ) ` j ) )
78 43 sselda 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. S )
79 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
80 79 fveq1d 
 |-  ( y = z -> ( ( G ` y ) ` j ) = ( ( G ` z ) ` j ) )
81 80 sumeq2sdv 
 |-  ( y = z -> sum_ j e. NN0 ( ( G ` y ) ` j ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
82 sumex 
 |-  sum_ j e. NN0 ( ( G ` z ) ` j ) e. _V
83 81 2 82 fvmpt 
 |-  ( z e. S -> ( F ` z ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
84 78 83 syl 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( F ` z ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
85 77 84 breqtrrd 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) ~~> ( F ` z ) )
86 oveq2 
 |-  ( k = m -> ( 0 ... k ) = ( 0 ... m ) )
87 86 sumeq1d 
 |-  ( k = m -> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) = sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) )
88 87 mpteq2dv 
 |-  ( k = m -> ( y e. B |-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) = ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) )
89 eqid 
 |-  ( 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 ) ) )
90 31 mptex 
 |-  ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) e. _V
91 88 89 90 fvmpt 
 |-  ( 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 ) ) )
92 91 adantl 
 |-  ( ( ( ( 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 ) ) )
93 92 fveq1d 
 |-  ( ( ( ( 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 ) )
94 79 fveq1d 
 |-  ( y = z -> ( ( G ` y ) ` i ) = ( ( G ` z ) ` i ) )
95 94 sumeq2sdv 
 |-  ( y = z -> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) = sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) )
96 eqid 
 |-  ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) = ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) )
97 sumex 
 |-  sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) e. _V
98 95 96 97 fvmpt 
 |-  ( z e. B -> ( ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ` z ) = sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) )
99 98 ad2antlr 
 |-  ( ( ( ( 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 ) )
100 eqidd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( ( G ` z ) ` i ) = ( ( G ` z ) ` i ) )
101 simpr 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> m e. NN0 )
102 101 8 eleqtrdi 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> m e. ( ZZ>= ` 0 ) )
103 49 adantr 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( G ` z ) : NN0 --> CC )
104 elfznn0 
 |-  ( i e. ( 0 ... m ) -> i e. NN0 )
105 ffvelcdm 
 |-  ( ( ( G ` z ) : NN0 --> CC /\ i e. NN0 ) -> ( ( G ` z ) ` i ) e. CC )
106 103 104 105 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( ( G ` z ) ` i ) e. CC )
107 100 102 106 fsumser 
 |-  ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) = ( seq 0 ( + , ( G ` z ) ) ` m ) )
108 93 99 107 3eqtrd 
 |-  ( ( ( ( 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 ) )
109 108 mpteq2dva 
 |-  ( ( ( 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 ) ) )
110 0z 
 |-  0 e. ZZ
111 seqfn 
 |-  ( 0 e. ZZ -> seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 ) )
112 110 111 ax-mp 
 |-  seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 )
113 8 fneq2i 
 |-  ( seq 0 ( + , ( G ` z ) ) Fn NN0 <-> seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 ) )
114 112 113 mpbir 
 |-  seq 0 ( + , ( G ` z ) ) Fn NN0
115 dffn5 
 |-  ( seq 0 ( + , ( G ` z ) ) Fn NN0 <-> seq 0 ( + , ( G ` z ) ) = ( m e. NN0 |-> ( seq 0 ( + , ( G ` z ) ) ` m ) ) )
116 114 115 mpbi 
 |-  seq 0 ( + , ( G ` z ) ) = ( m e. NN0 |-> ( seq 0 ( + , ( G ` z ) ) ` m ) )
117 109 116 eqtr4di 
 |-  ( ( ( 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 ) ) )
118 fvres 
 |-  ( z e. B -> ( ( F |` B ) ` z ) = ( F ` z ) )
119 118 adantl 
 |-  ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( F |` B ) ` z ) = ( F ` z ) )
120 85 117 119 3brtr4d 
 |-  ( ( ( 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 ) )
121 91 adantl 
 |-  ( ( ( 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 ) ) )
122 121 oveq2d 
 |-  ( ( ( 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 ) ) ) )
123 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
124 123 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
125 124 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
126 9 a1i 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> CC e. { RR , CC } )
127 123 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
128 127 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) e. ( TopOpen ` CCfld ) )
129 14 15 18 128 mp3an2i 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) e. ( TopOpen ` CCfld ) )
130 7 129 eqeltrid 
 |-  ( ( ph /\ a e. S ) -> B e. ( TopOpen ` CCfld ) )
131 130 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> B e. ( TopOpen ` CCfld ) )
132 fzfid 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( 0 ... m ) e. Fin )
133 3 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> A : NN0 --> CC )
134 133 3ad2ant1 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> A : NN0 --> CC )
135 21 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> B C_ CC )
136 135 sselda 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> y e. CC )
137 136 3adant2 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> y e. CC )
138 1 134 137 psergf 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> ( G ` y ) : NN0 --> CC )
139 104 3ad2ant2 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> i e. NN0 )
140 138 139 ffvelcdmd 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> ( ( G ` y ) ` i ) e. CC )
141 9 a1i 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> CC e. { RR , CC } )
142 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ i e. NN0 ) -> ( A ` i ) e. CC )
143 133 104 142 syl2an 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( A ` i ) e. CC )
144 143 adantr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( A ` i ) e. CC )
145 136 adantlr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> y e. CC )
146 id 
 |-  ( y e. CC -> y e. CC )
147 104 adantl 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> i e. NN0 )
148 expcl 
 |-  ( ( y e. CC /\ i e. NN0 ) -> ( y ^ i ) e. CC )
149 146 147 148 syl2anr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. CC ) -> ( y ^ i ) e. CC )
150 145 149 syldan 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( y ^ i ) e. CC )
151 144 150 mulcld 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( A ` i ) x. ( y ^ i ) ) e. CC )
152 ovexd 
 |-  ( ( ( ( ( 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 )
153 c0ex 
 |-  0 e. _V
154 ovex 
 |-  ( i x. ( y ^ ( i - 1 ) ) ) e. _V
155 153 154 ifex 
 |-  if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) e. _V
156 155 a1i 
 |-  ( ( ( ( ( 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 )
157 155 a1i 
 |-  ( ( ( ( ( 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 )
158 dvexp2 
 |-  ( i e. NN0 -> ( CC _D ( y e. CC |-> ( y ^ i ) ) ) = ( y e. CC |-> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
159 147 158 syl 
 |-  ( ( ( ( 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 ) ) ) ) ) )
160 21 ad2antrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> B C_ CC )
161 130 ad2antrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> B e. ( TopOpen ` CCfld ) )
162 141 149 157 159 160 125 123 161 dvmptres 
 |-  ( ( ( ( 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 ) ) ) ) ) )
163 141 150 156 162 143 dvmptcmul 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
164 141 151 152 163 dvmptcl 
 |-  ( ( ( ( ( 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 )
165 164 3impa 
 |-  ( ( ( ( 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 )
166 104 ad2antlr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> i e. NN0 )
167 1 pserval2 
 |-  ( ( y e. CC /\ i e. NN0 ) -> ( ( G ` y ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
168 145 166 167 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( G ` y ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
169 168 mpteq2dva 
 |-  ( ( ( ( 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 ) ) ) )
170 169 oveq2d 
 |-  ( ( ( ( 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 ) ) ) ) )
171 170 163 eqtrd 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
172 125 123 126 131 132 140 165 171 dvmptfsum 
 |-  ( ( ( 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 ) ) ) ) ) ) )
173 122 172 eqtrd 
 |-  ( ( ( 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 ) ) ) ) ) ) )
174 173 mpteq2dva 
 |-  ( ( 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 ) ) ) ) ) ) ) )
175 nnssnn0 
 |-  NN C_ NN0
176 resmpt 
 |-  ( 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 ) ) ) ) ) ) ) )
177 175 176 ax-mp 
 |-  ( ( 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 ) ) ) ) ) ) )
178 oveq1 
 |-  ( a = x -> ( a ^ i ) = ( x ^ i ) )
179 178 oveq2d 
 |-  ( a = x -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) )
180 179 mpteq2dv 
 |-  ( 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 ) ) ) )
181 oveq1 
 |-  ( i = n -> ( i + 1 ) = ( n + 1 ) )
182 fvoveq1 
 |-  ( i = n -> ( A ` ( i + 1 ) ) = ( A ` ( n + 1 ) ) )
183 181 182 oveq12d 
 |-  ( i = n -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
184 oveq2 
 |-  ( i = n -> ( x ^ i ) = ( x ^ n ) )
185 183 184 oveq12d 
 |-  ( i = n -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) = ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
186 185 cbvmptv 
 |-  ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) ) = ( n e. NN0 |-> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
187 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
188 fvoveq1 
 |-  ( m = n -> ( A ` ( m + 1 ) ) = ( A ` ( n + 1 ) ) )
189 187 188 oveq12d 
 |-  ( m = n -> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
190 eqid 
 |-  ( m e. NN0 |-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) = ( m e. NN0 |-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) )
191 ovex 
 |-  ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) e. _V
192 189 190 191 fvmpt 
 |-  ( n e. NN0 -> ( ( m e. NN0 |-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
193 192 oveq1d 
 |-  ( 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 ) ) )
194 193 mpteq2ia 
 |-  ( 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 ) ) )
195 186 194 eqtr4i 
 |-  ( 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 ) ) )
196 180 195 eqtrdi 
 |-  ( 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 ) ) ) )
197 196 cbvmptv 
 |-  ( 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 ) ) ) )
198 fveq2 
 |-  ( 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 ) )
199 198 fveq1d 
 |-  ( 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 ) )
200 199 sumeq2sdv 
 |-  ( 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 ) )
201 200 cbvmptv 
 |-  ( 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 ) )
202 peano2nn0 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN0 )
203 202 adantl 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( m + 1 ) e. NN0 )
204 203 nn0cnd 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( m + 1 ) e. CC )
205 133 203 ffvelcdmd 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( A ` ( m + 1 ) ) e. CC )
206 204 205 mulcld 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) e. CC )
207 206 fmpttd 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN0 |-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) : NN0 --> CC )
208 fveq2 
 |-  ( 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 ) )
209 208 seqeq3d 
 |-  ( 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 ) ) )
210 209 eleq1d 
 |-  ( 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 ~~> ) )
211 210 cbvrabv 
 |-  { 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 ~~> }
212 211 supeq1i 
 |-  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* , < )
213 198 seqeq3d 
 |-  ( 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 ) ) )
214 213 fveq1d 
 |-  ( 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 ) )
215 214 cbvmptv 
 |-  ( 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 ) )
216 fveq2 
 |-  ( 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 ) )
217 216 mpteq2dv 
 |-  ( 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 ) ) )
218 215 217 eqtrid 
 |-  ( 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 ) ) )
219 218 cbvmptv 
 |-  ( 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 ) ) )
220 17 rpred 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR )
221 1 2 3 4 5 6 psercnlem1 
 |-  ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
222 221 simp1d 
 |-  ( ( ph /\ a e. S ) -> M e. RR+ )
223 222 rpxrd 
 |-  ( ( ph /\ a e. S ) -> M e. RR* )
224 197 207 212 radcnvcl 
 |-  ( ( 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 ) )
225 54 224 sselid 
 |-  ( ( 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* )
226 221 simp2d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < M )
227 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
228 absf 
 |-  abs : CC --> RR
229 228 fdmi 
 |-  dom abs = CC
230 227 229 sseqtri 
 |-  ( `' abs " ( 0 [,) R ) ) C_ CC
231 5 230 eqsstri 
 |-  S C_ CC
232 231 a1i 
 |-  ( ph -> S C_ CC )
233 232 sselda 
 |-  ( ( ph /\ a e. S ) -> a e. CC )
234 233 abscld 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) e. RR )
235 222 rpred 
 |-  ( ( ph /\ a e. S ) -> M e. RR )
236 avglt2 
 |-  ( ( ( abs ` a ) e. RR /\ M e. RR ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
237 234 235 236 syl2anc 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
238 226 237 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < M )
239 222 rpge0d 
 |-  ( ( ph /\ a e. S ) -> 0 <_ M )
240 235 239 absidd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` M ) = M )
241 222 rpcnd 
 |-  ( ( ph /\ a e. S ) -> M e. CC )
242 oveq1 
 |-  ( w = M -> ( w ^ i ) = ( M ^ i ) )
243 242 oveq2d 
 |-  ( w = M -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) )
244 243 mpteq2dv 
 |-  ( 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 ) ) ) )
245 oveq1 
 |-  ( a = w -> ( a ^ i ) = ( w ^ i ) )
246 245 oveq2d 
 |-  ( a = w -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) )
247 246 mpteq2dv 
 |-  ( 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 ) ) ) )
248 247 cbvmptv 
 |-  ( 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 ) ) ) )
249 nn0ex 
 |-  NN0 e. _V
250 249 mptex 
 |-  ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) e. _V
251 244 248 250 fvmpt 
 |-  ( 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 ) ) ) )
252 241 251 syl 
 |-  ( ( 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 ) ) ) )
253 252 seqeq3d 
 |-  ( ( 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 ) ) ) ) )
254 fveq2 
 |-  ( n = i -> ( A ` n ) = ( A ` i ) )
255 oveq2 
 |-  ( n = i -> ( x ^ n ) = ( x ^ i ) )
256 254 255 oveq12d 
 |-  ( n = i -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` i ) x. ( x ^ i ) ) )
257 256 cbvmptv 
 |-  ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( i e. NN0 |-> ( ( A ` i ) x. ( x ^ i ) ) )
258 oveq1 
 |-  ( x = y -> ( x ^ i ) = ( y ^ i ) )
259 258 oveq2d 
 |-  ( x = y -> ( ( A ` i ) x. ( x ^ i ) ) = ( ( A ` i ) x. ( y ^ i ) ) )
260 259 mpteq2dv 
 |-  ( x = y -> ( i e. NN0 |-> ( ( A ` i ) x. ( x ^ i ) ) ) = ( i e. NN0 |-> ( ( A ` i ) x. ( y ^ i ) ) ) )
261 257 260 eqtrid 
 |-  ( x = y -> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( i e. NN0 |-> ( ( A ` i ) x. ( y ^ i ) ) ) )
262 261 cbvmptv 
 |-  ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) ) = ( y e. CC |-> ( i e. NN0 |-> ( ( A ` i ) x. ( y ^ i ) ) ) )
263 1 262 eqtri 
 |-  G = ( y e. CC |-> ( i e. NN0 |-> ( ( A ` i ) x. ( y ^ i ) ) ) )
264 fveq2 
 |-  ( r = s -> ( G ` r ) = ( G ` s ) )
265 264 seqeq3d 
 |-  ( r = s -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` s ) ) )
266 265 eleq1d 
 |-  ( r = s -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` s ) ) e. dom ~~> ) )
267 266 cbvrabv 
 |-  { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } = { s e. RR | seq 0 ( + , ( G ` s ) ) e. dom ~~> }
268 267 supeq1i 
 |-  sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { s e. RR | seq 0 ( + , ( G ` s ) ) e. dom ~~> } , RR* , < )
269 4 268 eqtri 
 |-  R = sup ( { s e. RR | seq 0 ( + , ( G ` s ) ) e. dom ~~> } , RR* , < )
270 eqid 
 |-  ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) = ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) )
271 3 adantr 
 |-  ( ( ph /\ a e. S ) -> A : NN0 --> CC )
272 221 simp3d 
 |-  ( ( ph /\ a e. S ) -> M < R )
273 240 272 eqbrtrd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` M ) < R )
274 263 269 270 271 241 273 dvradcnv 
 |-  ( ( ph /\ a e. S ) -> seq 0 ( + , ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) ) e. dom ~~> )
275 253 274 eqeltrd 
 |-  ( ( ph /\ a e. S ) -> seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` M ) ) e. dom ~~> )
276 197 207 212 241 275 radcnvle 
 |-  ( ( 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* , < ) )
277 240 276 eqbrtrrd 
 |-  ( ( 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* , < ) )
278 18 223 225 238 277 xrltletrd 
 |-  ( ( 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* , < ) )
279 197 201 207 212 219 220 278 41 pserulm 
 |-  ( ( 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 ) ) )
280 21 sselda 
 |-  ( ( ( ph /\ a e. S ) /\ y e. B ) -> y e. CC )
281 oveq1 
 |-  ( a = y -> ( a ^ i ) = ( y ^ i ) )
282 281 oveq2d 
 |-  ( a = y -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) )
283 282 mpteq2dv 
 |-  ( 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 ) ) ) )
284 eqid 
 |-  ( 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 ) ) ) )
285 249 mptex 
 |-  ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) e. _V
286 283 284 285 fvmpt 
 |-  ( 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 ) ) ) )
287 280 286 syl 
 |-  ( ( ( 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 ) ) ) )
288 287 adantr 
 |-  ( ( ( ( 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 ) ) ) )
289 288 fveq1d 
 |-  ( ( ( ( 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 ) )
290 oveq1 
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
291 fvoveq1 
 |-  ( i = k -> ( A ` ( i + 1 ) ) = ( A ` ( k + 1 ) ) )
292 290 291 oveq12d 
 |-  ( i = k -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) = ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
293 oveq2 
 |-  ( i = k -> ( y ^ i ) = ( y ^ k ) )
294 292 293 oveq12d 
 |-  ( i = k -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
295 eqid 
 |-  ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) = ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) )
296 ovex 
 |-  ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) e. _V
297 294 295 296 fvmpt 
 |-  ( 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 ) ) )
298 297 adantl 
 |-  ( ( ( ( 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 ) ) )
299 289 298 eqtrd 
 |-  ( ( ( ( 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 ) ) )
300 299 sumeq2dv 
 |-  ( ( ( 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 ) ) )
301 300 mpteq2dva 
 |-  ( ( 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 ) ) ) )
302 279 301 breqtrd 
 |-  ( ( 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 ) ) ) )
303 nnuz 
 |-  NN = ( ZZ>= ` 1 )
304 1e0p1 
 |-  1 = ( 0 + 1 )
305 304 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
306 303 305 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
307 1zzd 
 |-  ( ( ph /\ a e. S ) -> 1 e. ZZ )
308 0zd 
 |-  ( ( ( ph /\ a e. S ) /\ y e. B ) -> 0 e. ZZ )
309 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
310 309 nn0cnd 
 |-  ( i e. NN0 -> ( i + 1 ) e. CC )
311 310 adantl 
 |-  ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( i + 1 ) e. CC )
312 3 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ y e. B ) -> A : NN0 --> CC )
313 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ ( i + 1 ) e. NN0 ) -> ( A ` ( i + 1 ) ) e. CC )
314 312 309 313 syl2an 
 |-  ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( A ` ( i + 1 ) ) e. CC )
315 311 314 mulcld 
 |-  ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) e. CC )
316 280 148 sylan 
 |-  ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( y ^ i ) e. CC )
317 315 316 mulcld 
 |-  ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) e. CC )
318 287 317 fmpt3d 
 |-  ( ( ( 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 )
319 318 ffvelcdmda 
 |-  ( ( ( ( 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 )
320 8 308 319 serf 
 |-  ( ( ( 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 )
321 320 ffvelcdmda 
 |-  ( ( ( ( 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 )
322 321 an32s 
 |-  ( ( ( ( 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 )
323 322 fmpttd 
 |-  ( ( ( 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 )
324 30 31 elmap 
 |-  ( ( 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 )
325 323 324 sylibr 
 |-  ( ( ( 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 ) )
326 325 fmpttd 
 |-  ( ( 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 ) )
327 elfznn 
 |-  ( i e. ( 1 ... m ) -> i e. NN )
328 327 nnne0d 
 |-  ( i e. ( 1 ... m ) -> i =/= 0 )
329 328 neneqd 
 |-  ( i e. ( 1 ... m ) -> -. i = 0 )
330 329 iffalsed 
 |-  ( i e. ( 1 ... m ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) = ( i x. ( y ^ ( i - 1 ) ) ) )
331 330 oveq2d 
 |-  ( i e. ( 1 ... m ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) )
332 331 sumeq2i 
 |-  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 ) ) ) )
333 1zzd 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> 1 e. ZZ )
334 nnz 
 |-  ( m e. NN -> m e. ZZ )
335 334 ad2antlr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> m e. ZZ )
336 271 ad2antrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> A : NN0 --> CC )
337 327 nnnn0d 
 |-  ( i e. ( 1 ... m ) -> i e. NN0 )
338 336 337 142 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( A ` i ) e. CC )
339 327 adantl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> i e. NN )
340 339 nncnd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> i e. CC )
341 280 adantlr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> y e. CC )
342 nnm1nn0 
 |-  ( i e. NN -> ( i - 1 ) e. NN0 )
343 327 342 syl 
 |-  ( i e. ( 1 ... m ) -> ( i - 1 ) e. NN0 )
344 expcl 
 |-  ( ( y e. CC /\ ( i - 1 ) e. NN0 ) -> ( y ^ ( i - 1 ) ) e. CC )
345 341 343 344 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( y ^ ( i - 1 ) ) e. CC )
346 340 345 mulcld 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( i x. ( y ^ ( i - 1 ) ) ) e. CC )
347 338 346 mulcld 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) e. CC )
348 fveq2 
 |-  ( i = ( k + 1 ) -> ( A ` i ) = ( A ` ( k + 1 ) ) )
349 id 
 |-  ( i = ( k + 1 ) -> i = ( k + 1 ) )
350 oveq1 
 |-  ( i = ( k + 1 ) -> ( i - 1 ) = ( ( k + 1 ) - 1 ) )
351 350 oveq2d 
 |-  ( i = ( k + 1 ) -> ( y ^ ( i - 1 ) ) = ( y ^ ( ( k + 1 ) - 1 ) ) )
352 349 351 oveq12d 
 |-  ( i = ( k + 1 ) -> ( i x. ( y ^ ( i - 1 ) ) ) = ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) )
353 348 352 oveq12d 
 |-  ( i = ( k + 1 ) -> ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
354 333 333 335 347 353 fsumshftm 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) = sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
355 332 354 eqtrid 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
356 fz1ssfz0 
 |-  ( 1 ... m ) C_ ( 0 ... m )
357 356 a1i 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( 1 ... m ) C_ ( 0 ... m ) )
358 331 adantl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) )
359 358 347 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
360 eldif 
 |-  ( i e. ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) ) <-> ( i e. ( 0 ... m ) /\ -. i e. ( ( 0 + 1 ) ... m ) ) )
361 elfzuz2 
 |-  ( i e. ( 0 ... m ) -> m e. ( ZZ>= ` 0 ) )
362 elfzp12 
 |-  ( m e. ( ZZ>= ` 0 ) -> ( i e. ( 0 ... m ) <-> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) ) )
363 361 362 syl 
 |-  ( i e. ( 0 ... m ) -> ( i e. ( 0 ... m ) <-> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) ) )
364 363 ibi 
 |-  ( i e. ( 0 ... m ) -> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) )
365 364 ord 
 |-  ( i e. ( 0 ... m ) -> ( -. i = 0 -> i e. ( ( 0 + 1 ) ... m ) ) )
366 365 con1d 
 |-  ( i e. ( 0 ... m ) -> ( -. i e. ( ( 0 + 1 ) ... m ) -> i = 0 ) )
367 366 imp 
 |-  ( ( i e. ( 0 ... m ) /\ -. i e. ( ( 0 + 1 ) ... m ) ) -> i = 0 )
368 360 367 sylbi 
 |-  ( i e. ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) ) -> i = 0 )
369 304 oveq1i 
 |-  ( 1 ... m ) = ( ( 0 + 1 ) ... m )
370 369 difeq2i 
 |-  ( ( 0 ... m ) \ ( 1 ... m ) ) = ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) )
371 368 370 eleq2s 
 |-  ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i = 0 )
372 371 adantl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> i = 0 )
373 372 iftrued 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) = 0 )
374 373 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. 0 ) )
375 eldifi 
 |-  ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i e. ( 0 ... m ) )
376 375 104 syl 
 |-  ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i e. NN0 )
377 336 376 142 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( A ` i ) e. CC )
378 377 mul01d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. 0 ) = 0 )
379 374 378 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = 0 )
380 fzfid 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( 0 ... m ) e. Fin )
381 357 359 379 380 fsumss 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
382 1m1e0 
 |-  ( 1 - 1 ) = 0
383 382 oveq1i 
 |-  ( ( 1 - 1 ) ... ( m - 1 ) ) = ( 0 ... ( m - 1 ) )
384 383 sumeq1i 
 |-  sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = sum_ k e. ( 0 ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) )
385 elfznn0 
 |-  ( k e. ( 0 ... ( m - 1 ) ) -> k e. NN0 )
386 385 adantl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> k e. NN0 )
387 386 297 syl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
388 341 adantr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> y e. CC )
389 388 286 syl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( 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 ) ) ) )
390 389 fveq1d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( 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 ) )
391 336 adantr 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> A : NN0 --> CC )
392 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
393 386 392 syl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( k + 1 ) e. NN0 )
394 391 393 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( A ` ( k + 1 ) ) e. CC )
395 393 nn0cnd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( k + 1 ) e. CC )
396 expcl 
 |-  ( ( y e. CC /\ k e. NN0 ) -> ( y ^ k ) e. CC )
397 341 385 396 syl2an 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ k ) e. CC )
398 394 395 397 mul12d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ k ) ) ) = ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( y ^ k ) ) ) )
399 386 nn0cnd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> k e. CC )
400 ax-1cn 
 |-  1 e. CC
401 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
402 399 400 401 sylancl 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) - 1 ) = k )
403 402 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ ( ( k + 1 ) - 1 ) ) = ( y ^ k ) )
404 403 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) = ( ( k + 1 ) x. ( y ^ k ) ) )
405 404 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ k ) ) ) )
406 395 394 397 mulassd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) = ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( y ^ k ) ) ) )
407 398 405 406 3eqtr4d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
408 387 390 407 3eqtr4d 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
409 nnm1nn0 
 |-  ( m e. NN -> ( m - 1 ) e. NN0 )
410 409 adantl 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( m - 1 ) e. NN0 )
411 410 adantr 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( m - 1 ) e. NN0 )
412 411 8 eleqtrdi 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( m - 1 ) e. ( ZZ>= ` 0 ) )
413 403 397 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ ( ( k + 1 ) - 1 ) ) e. CC )
414 395 413 mulcld 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) e. CC )
415 394 414 mulcld 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) e. CC )
416 408 412 415 fsumser 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ k e. ( 0 ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
417 384 416 eqtrid 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
418 355 381 417 3eqtr3d 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
419 418 mpteq2dva 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) = ( y e. B |-> ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
420 fveq2 
 |-  ( j = ( m - 1 ) -> ( 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 ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
421 420 mpteq2dv 
 |-  ( j = ( m - 1 ) -> ( 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 ) ) ` ( m - 1 ) ) ) )
422 eqid 
 |-  ( 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 ) ) )
423 31 mptex 
 |-  ( y e. B |-> ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) e. _V
424 421 422 423 fvmpt 
 |-  ( ( m - 1 ) e. NN0 -> ( ( 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 - 1 ) ) = ( y e. B |-> ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
425 410 424 syl 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( ( 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 - 1 ) ) = ( y e. B |-> ( seq 0 ( + , ( ( a e. CC |-> ( i e. NN0 |-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
426 419 425 eqtr4d 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) = ( ( 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 - 1 ) ) )
427 426 mpteq2dva 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) = ( m e. NN |-> ( ( 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 - 1 ) ) ) )
428 8 306 11 307 326 427 ulmshft 
 |-  ( ( 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 ) ) ) <-> ( m e. NN |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ) )
429 302 428 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
430 177 429 eqbrtrid 
 |-  ( ( ph /\ a e. S ) -> ( ( m e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) |` NN ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
431 1nn0 
 |-  1 e. NN0
432 431 a1i 
 |-  ( ( ph /\ a e. S ) -> 1 e. NN0 )
433 fzfid 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> ( 0 ... m ) e. Fin )
434 164 an32s 
 |-  ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) /\ i e. ( 0 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
435 433 434 fsumcl 
 |-  ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
436 435 fmpttd 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) : B --> CC )
437 30 31 elmap 
 |-  ( ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) e. ( CC ^m B ) <-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) : B --> CC )
438 436 437 sylibr 
 |-  ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) e. ( CC ^m B ) )
439 438 fmpttd 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) : NN0 --> ( CC ^m B ) )
440 8 303 432 439 ulmres 
 |-  ( ( ph /\ a e. S ) -> ( ( m e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) <-> ( ( m e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) |` NN ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ) )
441 430 440 mpbird 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
442 174 441 eqbrtrd 
 |-  ( ( ph /\ a e. S ) -> ( m e. NN0 |-> ( CC _D ( ( k e. NN0 |-> ( y e. B |-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ) ) ( ~~>u ` B ) ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
443 8 10 11 34 44 120 442 ulmdv 
 |-  ( ( ph /\ a e. S ) -> ( CC _D ( F |` B ) ) = ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )