Metamath Proof Explorer

Theorem abelthlem9

Description: Lemma for abelth . By adjusting the constant term, we can assume that the entire series converges to 0 . (Contributed by Mario Carneiro, 1-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 ) ) )
Assertion abelthlem9 
|- ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )

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 0nn0 
 |-  0 e. NN0
8 7 a1i 
 |-  ( k e. NN0 -> 0 e. NN0 )
9 ffvelrn 
 |-  ( ( A : NN0 --> CC /\ 0 e. NN0 ) -> ( A ` 0 ) e. CC )
10 1 8 9 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` 0 ) e. CC )
11 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
12 0zd 
 |-  ( ph -> 0 e. ZZ )
13 eqidd 
 |-  ( ( ph /\ m e. NN0 ) -> ( A ` m ) = ( A ` m ) )
14 1 ffvelrnda 
 |-  ( ( ph /\ m e. NN0 ) -> ( A ` m ) e. CC )
15 11 12 13 14 2 isumcl 
 |-  ( ph -> sum_ m e. NN0 ( A ` m ) e. CC )
16 15 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ m e. NN0 ( A ` m ) e. CC )
17 10 16 subcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) e. CC )
18 1 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
19 17 18 ifcld 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) e. CC )
20 19 fmpttd 
 |-  ( ph -> ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) : NN0 --> CC )
21 7 a1i 
 |-  ( ph -> 0 e. NN0 )
22 20 ffvelrnda 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) e. CC )
23 1e0p1 
 |-  1 = ( 0 + 1 )
24 1z 
 |-  1 e. ZZ
25 23 24 eqeltrri 
 |-  ( 0 + 1 ) e. ZZ
26 25 a1i 
 |-  ( ph -> ( 0 + 1 ) e. ZZ )
27 nnuz 
 |-  NN = ( ZZ>= ` 1 )
28 23 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
29 27 28 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
30 29 eleq2i 
 |-  ( i e. NN <-> i e. ( ZZ>= ` ( 0 + 1 ) ) )
31 nnnn0 
 |-  ( i e. NN -> i e. NN0 )
32 31 adantl 
 |-  ( ( ph /\ i e. NN ) -> i e. NN0 )
33 eqeq1 
 |-  ( k = i -> ( k = 0 <-> i = 0 ) )
34 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
35 33 34 ifbieq2d 
 |-  ( k = i -> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
36 eqid 
 |-  ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) )
37 ovex 
 |-  ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) e. _V
38 fvex 
 |-  ( A ` i ) e. _V
39 37 38 ifex 
 |-  if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) e. _V
40 35 36 39 fvmpt 
 |-  ( i e. NN0 -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
41 32 40 syl 
 |-  ( ( ph /\ i e. NN ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
42 nnne0 
 |-  ( i e. NN -> i =/= 0 )
43 42 adantl 
 |-  ( ( ph /\ i e. NN ) -> i =/= 0 )
44 43 neneqd 
 |-  ( ( ph /\ i e. NN ) -> -. i = 0 )
45 44 iffalsed 
 |-  ( ( ph /\ i e. NN ) -> if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) = ( A ` i ) )
46 41 45 eqtrd 
 |-  ( ( ph /\ i e. NN ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = ( A ` i ) )
47 30 46 sylan2br 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = ( A ` i ) )
48 26 47 seqfeq 
 |-  ( ph -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) = seq ( 0 + 1 ) ( + , A ) )
49 11 12 13 14 2 isumclim2 
 |-  ( ph -> seq 0 ( + , A ) ~~> sum_ m e. NN0 ( A ` m ) )
50 11 21 18 49 clim2ser 
 |-  ( ph -> seq ( 0 + 1 ) ( + , A ) ~~> ( sum_ m e. NN0 ( A ` m ) - ( seq 0 ( + , A ) ` 0 ) ) )
51 0z 
 |-  0 e. ZZ
52 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( + , A ) ` 0 ) = ( A ` 0 ) )
53 51 52 ax-mp 
 |-  ( seq 0 ( + , A ) ` 0 ) = ( A ` 0 )
54 53 oveq2i 
 |-  ( sum_ m e. NN0 ( A ` m ) - ( seq 0 ( + , A ) ` 0 ) ) = ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) )
55 50 54 breqtrdi 
 |-  ( ph -> seq ( 0 + 1 ) ( + , A ) ~~> ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) )
56 48 55 eqbrtrd 
 |-  ( ph -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) )
57 11 21 22 56 clim2ser2 
 |-  ( ph -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) ) )
58 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` 0 ) )
59 51 58 ax-mp 
 |-  ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` 0 )
60 iftrue 
 |-  ( k = 0 -> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
61 60 36 37 fvmpt 
 |-  ( 0 e. NN0 -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` 0 ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
62 7 61 ax-mp 
 |-  ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` 0 ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) )
63 59 62 eqtri 
 |-  ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) )
64 63 oveq2i 
 |-  ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) ) = ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
65 1 7 9 sylancl 
 |-  ( ph -> ( A ` 0 ) e. CC )
66 npncan2 
 |-  ( ( sum_ m e. NN0 ( A ` m ) e. CC /\ ( A ` 0 ) e. CC ) -> ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) ) = 0 )
67 15 65 66 syl2anc 
 |-  ( ph -> ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) ) = 0 )
68 64 67 syl5eq 
 |-  ( ph -> ( ( sum_ m e. NN0 ( A ` m ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ` 0 ) ) = 0 )
69 57 68 breqtrd 
 |-  ( ph -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> 0 )
70 seqex 
 |-  seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) e. _V
71 c0ex 
 |-  0 e. _V
72 70 71 breldm 
 |-  ( seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> 0 -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) e. dom ~~> )
73 69 72 syl 
 |-  ( ph -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) e. dom ~~> )
74 eqid 
 |-  ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) = ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) )
75 20 73 3 4 5 74 69 abelthlem8 
 |-  ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R ) )
76 1 2 3 4 5 abelthlem2 
 |-  ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
77 76 simpld 
 |-  ( ph -> 1 e. S )
78 77 adantr 
 |-  ( ( ph /\ y e. S ) -> 1 e. S )
79 40 adantl 
 |-  ( ( x = 1 /\ i e. NN0 ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
80 oveq1 
 |-  ( x = 1 -> ( x ^ i ) = ( 1 ^ i ) )
81 nn0z 
 |-  ( i e. NN0 -> i e. ZZ )
82 1exp 
 |-  ( i e. ZZ -> ( 1 ^ i ) = 1 )
83 81 82 syl 
 |-  ( i e. NN0 -> ( 1 ^ i ) = 1 )
84 80 83 sylan9eq 
 |-  ( ( x = 1 /\ i e. NN0 ) -> ( x ^ i ) = 1 )
85 79 84 oveq12d 
 |-  ( ( x = 1 /\ i e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) )
86 85 sumeq2dv 
 |-  ( x = 1 -> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) )
87 sumex 
 |-  sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) e. _V
88 86 74 87 fvmpt 
 |-  ( 1 e. S -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) )
89 78 88 syl 
 |-  ( ( ph /\ y e. S ) -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) )
90 0zd 
 |-  ( ( ph /\ y e. S ) -> 0 e. ZZ )
91 40 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
92 65 15 subcld 
 |-  ( ph -> ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) e. CC )
93 92 ad2antrr 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) e. CC )
94 1 ffvelrnda 
 |-  ( ( ph /\ i e. NN0 ) -> ( A ` i ) e. CC )
95 94 adantlr 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( A ` i ) e. CC )
96 93 95 ifcld 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) e. CC )
97 96 mulid1d 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) = if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) )
98 91 97 eqtr4d 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) )
99 97 96 eqeltrd 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) e. CC )
100 oveq1 
 |-  ( x = 1 -> ( x ^ n ) = ( 1 ^ n ) )
101 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
102 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
103 101 102 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
104 100 103 sylan9eq 
 |-  ( ( x = 1 /\ n e. NN0 ) -> ( x ^ n ) = 1 )
105 104 oveq2d 
 |-  ( ( x = 1 /\ n e. NN0 ) -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` n ) x. 1 ) )
106 105 sumeq2dv 
 |-  ( x = 1 -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ n e. NN0 ( ( A ` n ) x. 1 ) )
107 fveq2 
 |-  ( n = m -> ( A ` n ) = ( A ` m ) )
108 107 oveq1d 
 |-  ( n = m -> ( ( A ` n ) x. 1 ) = ( ( A ` m ) x. 1 ) )
109 108 cbvsumv 
 |-  sum_ n e. NN0 ( ( A ` n ) x. 1 ) = sum_ m e. NN0 ( ( A ` m ) x. 1 )
110 106 109 eqtrdi 
 |-  ( x = 1 -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ m e. NN0 ( ( A ` m ) x. 1 ) )
111 sumex 
 |-  sum_ m e. NN0 ( ( A ` m ) x. 1 ) e. _V
112 110 6 111 fvmpt 
 |-  ( 1 e. S -> ( F ` 1 ) = sum_ m e. NN0 ( ( A ` m ) x. 1 ) )
113 77 112 syl 
 |-  ( ph -> ( F ` 1 ) = sum_ m e. NN0 ( ( A ` m ) x. 1 ) )
114 14 mulid1d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( A ` m ) x. 1 ) = ( A ` m ) )
115 114 sumeq2dv 
 |-  ( ph -> sum_ m e. NN0 ( ( A ` m ) x. 1 ) = sum_ m e. NN0 ( A ` m ) )
116 113 115 eqtrd 
 |-  ( ph -> ( F ` 1 ) = sum_ m e. NN0 ( A ` m ) )
117 116 oveq1d 
 |-  ( ph -> ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) = ( sum_ m e. NN0 ( A ` m ) - sum_ m e. NN0 ( A ` m ) ) )
118 15 subidd 
 |-  ( ph -> ( sum_ m e. NN0 ( A ` m ) - sum_ m e. NN0 ( A ` m ) ) = 0 )
119 117 118 eqtrd 
 |-  ( ph -> ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) = 0 )
120 69 119 breqtrrd 
 |-  ( ph -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) )
121 120 adantr 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ) ~~> ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) )
122 11 90 98 99 121 isumclim 
 |-  ( ( ph /\ y e. S ) -> sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. 1 ) = ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) )
123 89 122 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) = ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) )
124 oveq1 
 |-  ( x = y -> ( x ^ i ) = ( y ^ i ) )
125 40 124 oveqan12rd 
 |-  ( ( x = y /\ i e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
126 125 sumeq2dv 
 |-  ( x = y -> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
127 sumex 
 |-  sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) e. _V
128 126 74 127 fvmpt 
 |-  ( y e. S -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
129 128 adantl 
 |-  ( ( ph /\ y e. S ) -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) = sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
130 oveq2 
 |-  ( k = i -> ( y ^ k ) = ( y ^ i ) )
131 35 130 oveq12d 
 |-  ( k = i -> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
132 eqid 
 |-  ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) = ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) )
133 ovex 
 |-  ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) e. _V
134 131 132 133 fvmpt 
 |-  ( i e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
135 134 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
136 5 ssrab3 
 |-  S C_ CC
137 136 a1i 
 |-  ( ph -> S C_ CC )
138 137 sselda 
 |-  ( ( ph /\ y e. S ) -> y e. CC )
139 expcl 
 |-  ( ( y e. CC /\ i e. NN0 ) -> ( y ^ i ) e. CC )
140 138 139 sylan 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( y ^ i ) e. CC )
141 96 140 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) e. CC )
142 7 a1i 
 |-  ( ( ph /\ y e. S ) -> 0 e. NN0 )
143 19 adantlr 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN0 ) -> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) e. CC )
144 expcl 
 |-  ( ( y e. CC /\ k e. NN0 ) -> ( y ^ k ) e. CC )
145 138 144 sylan 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN0 ) -> ( y ^ k ) e. CC )
146 143 145 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN0 ) -> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) e. CC )
147 146 fmpttd 
 |-  ( ( ph /\ y e. S ) -> ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) : NN0 --> CC )
148 147 ffvelrnda 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) e. CC )
149 45 oveq1d 
 |-  ( ( ph /\ i e. NN ) -> ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) = ( ( A ` i ) x. ( y ^ i ) ) )
150 32 134 syl 
 |-  ( ( ph /\ i e. NN ) -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) = ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) )
151 34 130 oveq12d 
 |-  ( k = i -> ( ( A ` k ) x. ( y ^ k ) ) = ( ( A ` i ) x. ( y ^ i ) ) )
152 eqid 
 |-  ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) = ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) )
153 ovex 
 |-  ( ( A ` i ) x. ( y ^ i ) ) e. _V
154 151 152 153 fvmpt 
 |-  ( i e. NN0 -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
155 32 154 syl 
 |-  ( ( ph /\ i e. NN ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
156 149 150 155 3eqtr4d 
 |-  ( ( ph /\ i e. NN ) -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) = ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) )
157 30 156 sylan2br 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` i ) = ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) )
158 26 157 seqfeq 
 |-  ( ph -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) = seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) )
159 158 adantr 
 |-  ( ( ph /\ y e. S ) -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) = seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) )
160 18 adantlr 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
161 160 145 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( y ^ k ) ) e. CC )
162 161 fmpttd 
 |-  ( ( ph /\ y e. S ) -> ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) : NN0 --> CC )
163 162 ffvelrnda 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) e. CC )
164 154 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
165 95 140 mulcld 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( ( A ` i ) x. ( y ^ i ) ) e. CC )
166 1 2 3 4 5 abelthlem3 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) e. dom ~~> )
167 11 90 164 165 166 isumclim2 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ~~> sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) )
168 fveq2 
 |-  ( n = i -> ( A ` n ) = ( A ` i ) )
169 oveq2 
 |-  ( n = i -> ( x ^ n ) = ( x ^ i ) )
170 168 169 oveq12d 
 |-  ( n = i -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` i ) x. ( x ^ i ) ) )
171 170 cbvsumv 
 |-  sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ i e. NN0 ( ( A ` i ) x. ( x ^ i ) )
172 124 oveq2d 
 |-  ( x = y -> ( ( A ` i ) x. ( x ^ i ) ) = ( ( A ` i ) x. ( y ^ i ) ) )
173 172 sumeq2sdv 
 |-  ( x = y -> sum_ i e. NN0 ( ( A ` i ) x. ( x ^ i ) ) = sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) )
174 171 173 syl5eq 
 |-  ( x = y -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) )
175 sumex 
 |-  sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) e. _V
176 174 6 175 fvmpt 
 |-  ( y e. S -> ( F ` y ) = sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) )
177 176 adantl 
 |-  ( ( ph /\ y e. S ) -> ( F ` y ) = sum_ i e. NN0 ( ( A ` i ) x. ( y ^ i ) ) )
178 167 177 breqtrrd 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ~~> ( F ` y ) )
179 11 142 163 178 clim2ser 
 |-  ( ( ph /\ y e. S ) -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ~~> ( ( F ` y ) - ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) ) )
180 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` 0 ) )
181 51 180 ax-mp 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` 0 )
182 fveq2 
 |-  ( k = 0 -> ( A ` k ) = ( A ` 0 ) )
183 oveq2 
 |-  ( k = 0 -> ( y ^ k ) = ( y ^ 0 ) )
184 182 183 oveq12d 
 |-  ( k = 0 -> ( ( A ` k ) x. ( y ^ k ) ) = ( ( A ` 0 ) x. ( y ^ 0 ) ) )
185 ovex 
 |-  ( ( A ` 0 ) x. ( y ^ 0 ) ) e. _V
186 184 152 185 fvmpt 
 |-  ( 0 e. NN0 -> ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` 0 ) = ( ( A ` 0 ) x. ( y ^ 0 ) ) )
187 7 186 ax-mp 
 |-  ( ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ` 0 ) = ( ( A ` 0 ) x. ( y ^ 0 ) )
188 181 187 eqtri 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( A ` 0 ) x. ( y ^ 0 ) )
189 138 exp0d 
 |-  ( ( ph /\ y e. S ) -> ( y ^ 0 ) = 1 )
190 189 oveq2d 
 |-  ( ( ph /\ y e. S ) -> ( ( A ` 0 ) x. ( y ^ 0 ) ) = ( ( A ` 0 ) x. 1 ) )
191 65 adantr 
 |-  ( ( ph /\ y e. S ) -> ( A ` 0 ) e. CC )
192 191 mulid1d 
 |-  ( ( ph /\ y e. S ) -> ( ( A ` 0 ) x. 1 ) = ( A ` 0 ) )
193 190 192 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( A ` 0 ) x. ( y ^ 0 ) ) = ( A ` 0 ) )
194 188 193 syl5eq 
 |-  ( ( ph /\ y e. S ) -> ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) = ( A ` 0 ) )
195 194 oveq2d 
 |-  ( ( ph /\ y e. S ) -> ( ( F ` y ) - ( seq 0 ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ` 0 ) ) = ( ( F ` y ) - ( A ` 0 ) ) )
196 179 195 breqtrd 
 |-  ( ( ph /\ y e. S ) -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( ( A ` k ) x. ( y ^ k ) ) ) ) ~~> ( ( F ` y ) - ( A ` 0 ) ) )
197 159 196 eqbrtrd 
 |-  ( ( ph /\ y e. S ) -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ~~> ( ( F ` y ) - ( A ` 0 ) ) )
198 11 142 148 197 clim2ser2 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ~~> ( ( ( F ` y ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) ) )
199 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` 0 ) )
200 51 199 ax-mp 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` 0 )
201 60 183 oveq12d 
 |-  ( k = 0 -> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) = ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) ) )
202 ovex 
 |-  ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) ) e. _V
203 201 132 202 fvmpt 
 |-  ( 0 e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` 0 ) = ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) ) )
204 7 203 ax-mp 
 |-  ( ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ` 0 ) = ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) )
205 200 204 eqtri 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) )
206 189 oveq2d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) ) = ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. 1 ) )
207 15 adantr 
 |-  ( ( ph /\ y e. S ) -> sum_ m e. NN0 ( A ` m ) e. CC )
208 191 207 subcld 
 |-  ( ( ph /\ y e. S ) -> ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) e. CC )
209 208 mulid1d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. 1 ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
210 206 209 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) x. ( y ^ 0 ) ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
211 205 210 syl5eq 
 |-  ( ( ph /\ y e. S ) -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) = ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) )
212 211 oveq2d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( F ` y ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) ) = ( ( ( F ` y ) - ( A ` 0 ) ) + ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) ) )
213 1 2 3 4 5 6 abelthlem4 
 |-  ( ph -> F : S --> CC )
214 213 ffvelrnda 
 |-  ( ( ph /\ y e. S ) -> ( F ` y ) e. CC )
215 214 191 207 npncand 
 |-  ( ( ph /\ y e. S ) -> ( ( ( F ` y ) - ( A ` 0 ) ) + ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) ) = ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) )
216 212 215 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( ( F ` y ) - ( A ` 0 ) ) + ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ` 0 ) ) = ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) )
217 198 216 breqtrd 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) x. ( y ^ k ) ) ) ) ~~> ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) )
218 11 90 135 141 217 isumclim 
 |-  ( ( ph /\ y e. S ) -> sum_ i e. NN0 ( if ( i = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` i ) ) x. ( y ^ i ) ) = ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) )
219 129 218 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) = ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) )
220 123 219 oveq12d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) = ( ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) - ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) ) )
221 213 adantr 
 |-  ( ( ph /\ y e. S ) -> F : S --> CC )
222 221 78 ffvelrnd 
 |-  ( ( ph /\ y e. S ) -> ( F ` 1 ) e. CC )
223 222 214 207 nnncan2d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( F ` 1 ) - sum_ m e. NN0 ( A ` m ) ) - ( ( F ` y ) - sum_ m e. NN0 ( A ` m ) ) ) = ( ( F ` 1 ) - ( F ` y ) ) )
224 220 223 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) = ( ( F ` 1 ) - ( F ` y ) ) )
225 224 fveq2d 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) = ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) )
226 225 breq1d 
 |-  ( ( ph /\ y e. S ) -> ( ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R <-> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
227 226 imbi2d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R ) <-> ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) ) )
228 227 ralbidva 
 |-  ( ph -> ( A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R ) <-> A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) ) )
229 228 rexbidv 
 |-  ( ph -> ( E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R ) <-> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) ) )
230 229 adantr 
 |-  ( ( ph /\ R e. RR+ ) -> ( E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` 1 ) - ( ( x e. S |-> sum_ i e. NN0 ( ( ( k e. NN0 |-> if ( k = 0 , ( ( A ` 0 ) - sum_ m e. NN0 ( A ` m ) ) , ( A ` k ) ) ) ` i ) x. ( x ^ i ) ) ) ` y ) ) ) < R ) <-> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) ) )
231 75 230 mpbid 
 |-  ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )