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 |
|
ffvelrn |
|- ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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 |
|
ffvelrn |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( ( 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 |
|
ffvelrn |
|- ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
syl5eq |
|- ( 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
|
syl5eq |
|- ( 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 |
|
ffvelrn |
|- ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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
|
syl5eq |
|- ( ( ( ( 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
|
ffvelrnd |
|- ( ( ( ( ( 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
|
syl5eq |
|- ( ( ( ( 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 ) ) ) ) |