Step |
Hyp |
Ref |
Expression |
1 |
|
abelth.1 |
|- ( ph -> A : NN0 --> CC ) |
2 |
|
abelth.2 |
|- ( ph -> seq 0 ( + , A ) e. dom ~~> ) |
3 |
|
abelth.3 |
|- ( ph -> M e. RR ) |
4 |
|
abelth.4 |
|- ( ph -> 0 <_ M ) |
5 |
|
abelth.5 |
|- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) } |
6 |
|
abelth.6 |
|- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |
7 |
|
abelth.7 |
|- ( ph -> seq 0 ( + , A ) ~~> 0 ) |
8 |
|
abelthlem6.1 |
|- ( ph -> X e. ( S \ { 1 } ) ) |
9 |
8
|
eldifad |
|- ( ph -> X e. S ) |
10 |
|
oveq1 |
|- ( x = X -> ( x ^ n ) = ( X ^ n ) ) |
11 |
10
|
oveq2d |
|- ( x = X -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` n ) x. ( X ^ n ) ) ) |
12 |
11
|
sumeq2sdv |
|- ( x = X -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ n e. NN0 ( ( A ` n ) x. ( X ^ n ) ) ) |
13 |
|
sumex |
|- sum_ n e. NN0 ( ( A ` n ) x. ( X ^ n ) ) e. _V |
14 |
12 6 13
|
fvmpt |
|- ( X e. S -> ( F ` X ) = sum_ n e. NN0 ( ( A ` n ) x. ( X ^ n ) ) ) |
15 |
9 14
|
syl |
|- ( ph -> ( F ` X ) = sum_ n e. NN0 ( ( A ` n ) x. ( X ^ n ) ) ) |
16 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
17 |
|
0zd |
|- ( ph -> 0 e. ZZ ) |
18 |
|
fveq2 |
|- ( k = n -> ( A ` k ) = ( A ` n ) ) |
19 |
|
oveq2 |
|- ( k = n -> ( X ^ k ) = ( X ^ n ) ) |
20 |
18 19
|
oveq12d |
|- ( k = n -> ( ( A ` k ) x. ( X ^ k ) ) = ( ( A ` n ) x. ( X ^ n ) ) ) |
21 |
|
eqid |
|- ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) = ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) |
22 |
|
ovex |
|- ( ( A ` n ) x. ( X ^ n ) ) e. _V |
23 |
20 21 22
|
fvmpt |
|- ( n e. NN0 -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( A ` n ) x. ( X ^ n ) ) ) |
24 |
23
|
adantl |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( A ` n ) x. ( X ^ n ) ) ) |
25 |
1
|
ffvelrnda |
|- ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. CC ) |
26 |
5
|
ssrab3 |
|- S C_ CC |
27 |
26 9
|
sselid |
|- ( ph -> X e. CC ) |
28 |
|
expcl |
|- ( ( X e. CC /\ n e. NN0 ) -> ( X ^ n ) e. CC ) |
29 |
27 28
|
sylan |
|- ( ( ph /\ n e. NN0 ) -> ( X ^ n ) e. CC ) |
30 |
25 29
|
mulcld |
|- ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. ( X ^ n ) ) e. CC ) |
31 |
|
fveq2 |
|- ( k = n -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` n ) ) |
32 |
31 19
|
oveq12d |
|- ( k = n -> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) |
33 |
|
eqid |
|- ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) |
34 |
|
ovex |
|- ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. _V |
35 |
32 33 34
|
fvmpt |
|- ( n e. NN0 -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) |
36 |
35
|
adantl |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) |
37 |
16 17 25
|
serf |
|- ( ph -> seq 0 ( + , A ) : NN0 --> CC ) |
38 |
37
|
ffvelrnda |
|- ( ( ph /\ n e. NN0 ) -> ( seq 0 ( + , A ) ` n ) e. CC ) |
39 |
38 29
|
mulcld |
|- ( ( ph /\ n e. NN0 ) -> ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC ) |
40 |
1 2 3 4 5
|
abelthlem2 |
|- ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) ) |
41 |
40
|
simprd |
|- ( ph -> ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) |
42 |
41 8
|
sseldd |
|- ( ph -> X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) |
43 |
1 2 3 4 5 6 7
|
abelthlem5 |
|- ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> ) |
44 |
42 43
|
mpdan |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> ) |
45 |
16 17 36 39 44
|
isumclim2 |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ~~> sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) |
46 |
|
seqex |
|- seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ) e. _V |
47 |
46
|
a1i |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ) e. _V ) |
48 |
|
0nn0 |
|- 0 e. NN0 |
49 |
48
|
a1i |
|- ( ph -> 0 e. NN0 ) |
50 |
|
oveq1 |
|- ( k = i -> ( k - 1 ) = ( i - 1 ) ) |
51 |
50
|
oveq2d |
|- ( k = i -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( i - 1 ) ) ) |
52 |
51
|
sumeq1d |
|- ( k = i -> sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) = sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) ) |
53 |
|
oveq2 |
|- ( k = i -> ( X ^ k ) = ( X ^ i ) ) |
54 |
52 53
|
oveq12d |
|- ( k = i -> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) = ( sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) x. ( X ^ i ) ) ) |
55 |
|
eqid |
|- ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) = ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) |
56 |
|
ovex |
|- ( sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) x. ( X ^ i ) ) e. _V |
57 |
54 55 56
|
fvmpt |
|- ( i e. NN0 -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` i ) = ( sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) x. ( X ^ i ) ) ) |
58 |
57
|
adantl |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` i ) = ( sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) x. ( X ^ i ) ) ) |
59 |
|
fzfid |
|- ( ( ph /\ i e. NN0 ) -> ( 0 ... ( i - 1 ) ) e. Fin ) |
60 |
1
|
adantr |
|- ( ( ph /\ i e. NN0 ) -> A : NN0 --> CC ) |
61 |
|
elfznn0 |
|- ( m e. ( 0 ... ( i - 1 ) ) -> m e. NN0 ) |
62 |
|
ffvelrn |
|- ( ( A : NN0 --> CC /\ m e. NN0 ) -> ( A ` m ) e. CC ) |
63 |
60 61 62
|
syl2an |
|- ( ( ( ph /\ i e. NN0 ) /\ m e. ( 0 ... ( i - 1 ) ) ) -> ( A ` m ) e. CC ) |
64 |
59 63
|
fsumcl |
|- ( ( ph /\ i e. NN0 ) -> sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) e. CC ) |
65 |
|
expcl |
|- ( ( X e. CC /\ i e. NN0 ) -> ( X ^ i ) e. CC ) |
66 |
27 65
|
sylan |
|- ( ( ph /\ i e. NN0 ) -> ( X ^ i ) e. CC ) |
67 |
64 66
|
mulcld |
|- ( ( ph /\ i e. NN0 ) -> ( sum_ m e. ( 0 ... ( i - 1 ) ) ( A ` m ) x. ( X ^ i ) ) e. CC ) |
68 |
58 67
|
eqeltrd |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` i ) e. CC ) |
69 |
17
|
peano2zd |
|- ( ph -> ( 0 + 1 ) e. ZZ ) |
70 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
71 |
|
1e0p1 |
|- 1 = ( 0 + 1 ) |
72 |
71
|
fveq2i |
|- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) ) |
73 |
70 72
|
eqtri |
|- NN = ( ZZ>= ` ( 0 + 1 ) ) |
74 |
73
|
eleq2i |
|- ( n e. NN <-> n e. ( ZZ>= ` ( 0 + 1 ) ) ) |
75 |
|
nnm1nn0 |
|- ( n e. NN -> ( n - 1 ) e. NN0 ) |
76 |
75
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( n - 1 ) e. NN0 ) |
77 |
|
fveq2 |
|- ( k = ( n - 1 ) -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` ( n - 1 ) ) ) |
78 |
|
oveq2 |
|- ( k = ( n - 1 ) -> ( X ^ k ) = ( X ^ ( n - 1 ) ) ) |
79 |
77 78
|
oveq12d |
|- ( k = ( n - 1 ) -> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) = ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) |
80 |
79
|
oveq2d |
|- ( k = ( n - 1 ) -> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) ) |
81 |
|
eqid |
|- ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) = ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) |
82 |
|
ovex |
|- ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) e. _V |
83 |
80 81 82
|
fvmpt |
|- ( ( n - 1 ) e. NN0 -> ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` ( n - 1 ) ) = ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) ) |
84 |
76 83
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` ( n - 1 ) ) = ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) ) |
85 |
|
ax-1cn |
|- 1 e. CC |
86 |
|
nncn |
|- ( n e. NN -> n e. CC ) |
87 |
86
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. CC ) |
88 |
|
nn0ex |
|- NN0 e. _V |
89 |
88
|
mptex |
|- ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. _V |
90 |
89
|
shftval |
|- ( ( 1 e. CC /\ n e. CC ) -> ( ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ` n ) = ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` ( n - 1 ) ) ) |
91 |
85 87 90
|
sylancr |
|- ( ( ph /\ n e. NN ) -> ( ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ` n ) = ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` ( n - 1 ) ) ) |
92 |
|
eqidd |
|- ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( A ` m ) = ( A ` m ) ) |
93 |
76 16
|
eleqtrdi |
|- ( ( ph /\ n e. NN ) -> ( n - 1 ) e. ( ZZ>= ` 0 ) ) |
94 |
1
|
adantr |
|- ( ( ph /\ n e. NN ) -> A : NN0 --> CC ) |
95 |
|
elfznn0 |
|- ( m e. ( 0 ... ( n - 1 ) ) -> m e. NN0 ) |
96 |
94 95 62
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( A ` m ) e. CC ) |
97 |
92 93 96
|
fsumser |
|- ( ( ph /\ n e. NN ) -> sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) = ( seq 0 ( + , A ) ` ( n - 1 ) ) ) |
98 |
|
expm1t |
|- ( ( X e. CC /\ n e. NN ) -> ( X ^ n ) = ( ( X ^ ( n - 1 ) ) x. X ) ) |
99 |
27 98
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( X ^ n ) = ( ( X ^ ( n - 1 ) ) x. X ) ) |
100 |
27
|
adantr |
|- ( ( ph /\ n e. NN ) -> X e. CC ) |
101 |
|
expcl |
|- ( ( X e. CC /\ ( n - 1 ) e. NN0 ) -> ( X ^ ( n - 1 ) ) e. CC ) |
102 |
27 75 101
|
syl2an |
|- ( ( ph /\ n e. NN ) -> ( X ^ ( n - 1 ) ) e. CC ) |
103 |
100 102
|
mulcomd |
|- ( ( ph /\ n e. NN ) -> ( X x. ( X ^ ( n - 1 ) ) ) = ( ( X ^ ( n - 1 ) ) x. X ) ) |
104 |
99 103
|
eqtr4d |
|- ( ( ph /\ n e. NN ) -> ( X ^ n ) = ( X x. ( X ^ ( n - 1 ) ) ) ) |
105 |
97 104
|
oveq12d |
|- ( ( ph /\ n e. NN ) -> ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) = ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X x. ( X ^ ( n - 1 ) ) ) ) ) |
106 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
107 |
106
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. NN0 ) |
108 |
|
oveq1 |
|- ( k = n -> ( k - 1 ) = ( n - 1 ) ) |
109 |
108
|
oveq2d |
|- ( k = n -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( n - 1 ) ) ) |
110 |
109
|
sumeq1d |
|- ( k = n -> sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) = sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) |
111 |
110 19
|
oveq12d |
|- ( k = n -> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) |
112 |
|
ovex |
|- ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) e. _V |
113 |
111 55 112
|
fvmpt |
|- ( n e. NN0 -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) |
114 |
107 113
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) |
115 |
|
ffvelrn |
|- ( ( seq 0 ( + , A ) : NN0 --> CC /\ ( n - 1 ) e. NN0 ) -> ( seq 0 ( + , A ) ` ( n - 1 ) ) e. CC ) |
116 |
37 75 115
|
syl2an |
|- ( ( ph /\ n e. NN ) -> ( seq 0 ( + , A ) ` ( n - 1 ) ) e. CC ) |
117 |
100 116 102
|
mul12d |
|- ( ( ph /\ n e. NN ) -> ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) = ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X x. ( X ^ ( n - 1 ) ) ) ) ) |
118 |
105 114 117
|
3eqtr4d |
|- ( ( ph /\ n e. NN ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) = ( X x. ( ( seq 0 ( + , A ) ` ( n - 1 ) ) x. ( X ^ ( n - 1 ) ) ) ) ) |
119 |
84 91 118
|
3eqtr4d |
|- ( ( ph /\ n e. NN ) -> ( ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ` n ) = ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) ) |
120 |
74 119
|
sylan2br |
|- ( ( ph /\ n e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ` n ) = ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) ) |
121 |
69 120
|
seqfeq |
|- ( ph -> seq ( 0 + 1 ) ( + , ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ) = seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ) |
122 |
|
fveq2 |
|- ( k = i -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` i ) ) |
123 |
122 53
|
oveq12d |
|- ( k = i -> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) |
124 |
|
ovex |
|- ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) e. _V |
125 |
123 33 124
|
fvmpt |
|- ( i e. NN0 -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) |
126 |
125
|
adantl |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) |
127 |
37
|
ffvelrnda |
|- ( ( ph /\ i e. NN0 ) -> ( seq 0 ( + , A ) ` i ) e. CC ) |
128 |
127 66
|
mulcld |
|- ( ( ph /\ i e. NN0 ) -> ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) e. CC ) |
129 |
126 128
|
eqeltrd |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) e. CC ) |
130 |
123
|
oveq2d |
|- ( k = i -> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( X x. ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) ) |
131 |
|
ovex |
|- ( X x. ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) e. _V |
132 |
130 81 131
|
fvmpt |
|- ( i e. NN0 -> ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` i ) = ( X x. ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) ) |
133 |
132
|
adantl |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` i ) = ( X x. ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) ) |
134 |
126
|
oveq2d |
|- ( ( ph /\ i e. NN0 ) -> ( X x. ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) ) = ( X x. ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) ) |
135 |
133 134
|
eqtr4d |
|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` i ) = ( X x. ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) ) ) |
136 |
16 17 27 45 129 135
|
isermulc2 |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
137 |
|
0z |
|- 0 e. ZZ |
138 |
|
1z |
|- 1 e. ZZ |
139 |
89
|
isershft |
|- ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( seq 0 ( + , ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <-> seq ( 0 + 1 ) ( + , ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) |
140 |
137 138 139
|
mp2an |
|- ( seq 0 ( + , ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <-> seq ( 0 + 1 ) ( + , ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
141 |
136 140
|
sylib |
|- ( ph -> seq ( 0 + 1 ) ( + , ( ( k e. NN0 |-> ( X x. ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) shift 1 ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
142 |
121 141
|
eqbrtrrd |
|- ( ph -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
143 |
16 49 68 142
|
clim2ser2 |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ~~> ( ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) ) ) |
144 |
|
seq1 |
|- ( 0 e. ZZ -> ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` 0 ) ) |
145 |
137 144
|
ax-mp |
|- ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` 0 ) |
146 |
|
oveq1 |
|- ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) ) |
147 |
146
|
oveq2d |
|- ( k = 0 -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( 0 - 1 ) ) ) |
148 |
|
risefall0lem |
|- ( 0 ... ( 0 - 1 ) ) = (/) |
149 |
147 148
|
eqtrdi |
|- ( k = 0 -> ( 0 ... ( k - 1 ) ) = (/) ) |
150 |
149
|
sumeq1d |
|- ( k = 0 -> sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) = sum_ m e. (/) ( A ` m ) ) |
151 |
|
sum0 |
|- sum_ m e. (/) ( A ` m ) = 0 |
152 |
150 151
|
eqtrdi |
|- ( k = 0 -> sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) = 0 ) |
153 |
|
oveq2 |
|- ( k = 0 -> ( X ^ k ) = ( X ^ 0 ) ) |
154 |
152 153
|
oveq12d |
|- ( k = 0 -> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) = ( 0 x. ( X ^ 0 ) ) ) |
155 |
|
ovex |
|- ( 0 x. ( X ^ 0 ) ) e. _V |
156 |
154 55 155
|
fvmpt |
|- ( 0 e. NN0 -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` 0 ) = ( 0 x. ( X ^ 0 ) ) ) |
157 |
48 156
|
ax-mp |
|- ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` 0 ) = ( 0 x. ( X ^ 0 ) ) |
158 |
145 157
|
eqtri |
|- ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) = ( 0 x. ( X ^ 0 ) ) |
159 |
|
expcl |
|- ( ( X e. CC /\ 0 e. NN0 ) -> ( X ^ 0 ) e. CC ) |
160 |
27 48 159
|
sylancl |
|- ( ph -> ( X ^ 0 ) e. CC ) |
161 |
160
|
mul02d |
|- ( ph -> ( 0 x. ( X ^ 0 ) ) = 0 ) |
162 |
158 161
|
syl5eq |
|- ( ph -> ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) = 0 ) |
163 |
162
|
oveq2d |
|- ( ph -> ( ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) ) = ( ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + 0 ) ) |
164 |
16 17 36 39 44
|
isumcl |
|- ( ph -> sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC ) |
165 |
27 164
|
mulcld |
|- ( ph -> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. CC ) |
166 |
165
|
addid1d |
|- ( ph -> ( ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + 0 ) = ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
167 |
163 166
|
eqtrd |
|- ( ph -> ( ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` 0 ) ) = ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
168 |
143 167
|
breqtrd |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ~~> ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
169 |
16 17 129
|
serf |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) : NN0 --> CC ) |
170 |
169
|
ffvelrnda |
|- ( ( ph /\ i e. NN0 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` i ) e. CC ) |
171 |
16 17 68
|
serf |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) : NN0 --> CC ) |
172 |
171
|
ffvelrnda |
|- ( ( ph /\ i e. NN0 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` i ) e. CC ) |
173 |
|
simpr |
|- ( ( ph /\ i e. NN0 ) -> i e. NN0 ) |
174 |
173 16
|
eleqtrdi |
|- ( ( ph /\ i e. NN0 ) -> i e. ( ZZ>= ` 0 ) ) |
175 |
|
simpl |
|- ( ( ph /\ i e. NN0 ) -> ph ) |
176 |
|
elfznn0 |
|- ( n e. ( 0 ... i ) -> n e. NN0 ) |
177 |
36 39
|
eqeltrd |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) e. CC ) |
178 |
175 176 177
|
syl2an |
|- ( ( ( ph /\ i e. NN0 ) /\ n e. ( 0 ... i ) ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) e. CC ) |
179 |
113
|
adantl |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) |
180 |
|
fzfid |
|- ( ( ph /\ n e. NN0 ) -> ( 0 ... ( n - 1 ) ) e. Fin ) |
181 |
1
|
adantr |
|- ( ( ph /\ n e. NN0 ) -> A : NN0 --> CC ) |
182 |
181 95 62
|
syl2an |
|- ( ( ( ph /\ n e. NN0 ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( A ` m ) e. CC ) |
183 |
180 182
|
fsumcl |
|- ( ( ph /\ n e. NN0 ) -> sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) e. CC ) |
184 |
183 29
|
mulcld |
|- ( ( ph /\ n e. NN0 ) -> ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) e. CC ) |
185 |
179 184
|
eqeltrd |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) e. CC ) |
186 |
175 176 185
|
syl2an |
|- ( ( ( ph /\ i e. NN0 ) /\ n e. ( 0 ... i ) ) -> ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) e. CC ) |
187 |
|
eqidd |
|- ( ( ( ph /\ n e. NN0 ) /\ m e. ( 0 ... n ) ) -> ( A ` m ) = ( A ` m ) ) |
188 |
|
simpr |
|- ( ( ph /\ n e. NN0 ) -> n e. NN0 ) |
189 |
188 16
|
eleqtrdi |
|- ( ( ph /\ n e. NN0 ) -> n e. ( ZZ>= ` 0 ) ) |
190 |
|
elfznn0 |
|- ( m e. ( 0 ... n ) -> m e. NN0 ) |
191 |
181 190 62
|
syl2an |
|- ( ( ( ph /\ n e. NN0 ) /\ m e. ( 0 ... n ) ) -> ( A ` m ) e. CC ) |
192 |
187 189 191
|
fsumser |
|- ( ( ph /\ n e. NN0 ) -> sum_ m e. ( 0 ... n ) ( A ` m ) = ( seq 0 ( + , A ) ` n ) ) |
193 |
|
fveq2 |
|- ( m = n -> ( A ` m ) = ( A ` n ) ) |
194 |
189 191 193
|
fsumm1 |
|- ( ( ph /\ n e. NN0 ) -> sum_ m e. ( 0 ... n ) ( A ` m ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) + ( A ` n ) ) ) |
195 |
192 194
|
eqtr3d |
|- ( ( ph /\ n e. NN0 ) -> ( seq 0 ( + , A ) ` n ) = ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) + ( A ` n ) ) ) |
196 |
195
|
oveq1d |
|- ( ( ph /\ n e. NN0 ) -> ( ( seq 0 ( + , A ) ` n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) = ( ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) + ( A ` n ) ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) ) |
197 |
183 25
|
pncan2d |
|- ( ( ph /\ n e. NN0 ) -> ( ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) + ( A ` n ) ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) = ( A ` n ) ) |
198 |
196 197
|
eqtr2d |
|- ( ( ph /\ n e. NN0 ) -> ( A ` n ) = ( ( seq 0 ( + , A ) ` n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) ) |
199 |
198
|
oveq1d |
|- ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. ( X ^ n ) ) = ( ( ( seq 0 ( + , A ) ` n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) x. ( X ^ n ) ) ) |
200 |
38 183 29
|
subdird |
|- ( ( ph /\ n e. NN0 ) -> ( ( ( seq 0 ( + , A ) ` n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) ) x. ( X ^ n ) ) = ( ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) ) |
201 |
199 200
|
eqtrd |
|- ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. ( X ^ n ) ) = ( ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) ) |
202 |
36 179
|
oveq12d |
|- ( ( ph /\ n e. NN0 ) -> ( ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) - ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) ) = ( ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( sum_ m e. ( 0 ... ( n - 1 ) ) ( A ` m ) x. ( X ^ n ) ) ) ) |
203 |
201 24 202
|
3eqtr4d |
|- ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) - ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) ) ) |
204 |
175 176 203
|
syl2an |
|- ( ( ( ph /\ i e. NN0 ) /\ n e. ( 0 ... i ) ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) - ( ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ` n ) ) ) |
205 |
174 178 186 204
|
sersub |
|- ( ( ph /\ i e. NN0 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ) ` i ) = ( ( seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` i ) - ( seq 0 ( + , ( k e. NN0 |-> ( sum_ m e. ( 0 ... ( k - 1 ) ) ( A ` m ) x. ( X ^ k ) ) ) ) ` i ) ) ) |
206 |
16 17 45 47 168 170 172 205
|
climsub |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ) ~~> ( sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) |
207 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
208 |
207 27 164
|
subdird |
|- ( ph -> ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( ( 1 x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) - ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) |
209 |
164
|
mulid2d |
|- ( ph -> ( 1 x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) |
210 |
209
|
oveq1d |
|- ( ph -> ( ( 1 x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) - ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) |
211 |
208 210
|
eqtrd |
|- ( ph -> ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) - ( X x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) |
212 |
206 211
|
breqtrrd |
|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( X ^ k ) ) ) ) ~~> ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
213 |
16 17 24 30 212
|
isumclim |
|- ( ph -> sum_ n e. NN0 ( ( A ` n ) x. ( X ^ n ) ) = ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |
214 |
15 213
|
eqtrd |
|- ( ph -> ( F ` X ) = ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) |