Metamath Proof Explorer

Theorem abelthlem6

Description: Lemma for abelth . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Hypotheses abelth.1 
|- ( ph -> A : NN0 --> CC )
abelth.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
abelth.3 
|- ( ph -> M e. RR )
abelth.4 
|- ( ph -> 0 <_ M )
abelth.5 
|- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
abelth.6 
|- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
abelth.7 
|- ( ph -> seq 0 ( + , A ) ~~> 0 )
abelthlem6.1 
|- ( ph -> X e. ( S \ { 1 } ) )
Assertion abelthlem6 
|- ( ph -> ( F ` X ) = ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )

Proof

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 ) ) ) )