Metamath Proof Explorer

Theorem abelthlem8

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 )
Assertion abelthlem8 
|- ( ( 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 abelth.7 
 |-  ( ph -> seq 0 ( + , A ) ~~> 0 )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 0zd 
 |-  ( ( ph /\ R e. RR+ ) -> 0 e. ZZ )
10 id 
 |-  ( R e. RR+ -> R e. RR+ )
11 3 4 ge0p1rpd 
 |-  ( ph -> ( M + 1 ) e. RR+ )
12 rpdivcl 
 |-  ( ( R e. RR+ /\ ( M + 1 ) e. RR+ ) -> ( R / ( M + 1 ) ) e. RR+ )
13 10 11 12 syl2anr 
 |-  ( ( ph /\ R e. RR+ ) -> ( R / ( M + 1 ) ) e. RR+ )
14 eqidd 
 |-  ( ( ( ph /\ R e. RR+ ) /\ k e. NN0 ) -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` k ) )
15 7 adantr 
 |-  ( ( ph /\ R e. RR+ ) -> seq 0 ( + , A ) ~~> 0 )
16 8 9 13 14 15 climi0 
 |-  ( ( ph /\ R e. RR+ ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) )
17 13 adantr 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> ( R / ( M + 1 ) ) e. RR+ )
18 fzfid 
 |-  ( ph -> ( 0 ... ( j - 1 ) ) e. Fin )
19 0zd 
 |-  ( ph -> 0 e. ZZ )
20 1 ffvelrnda 
 |-  ( ( ph /\ w e. NN0 ) -> ( A ` w ) e. CC )
21 8 19 20 serf 
 |-  ( ph -> seq 0 ( + , A ) : NN0 --> CC )
22 elfznn0 
 |-  ( i e. ( 0 ... ( j - 1 ) ) -> i e. NN0 )
23 ffvelrn 
 |-  ( ( seq 0 ( + , A ) : NN0 --> CC /\ i e. NN0 ) -> ( seq 0 ( + , A ) ` i ) e. CC )
24 21 22 23 syl2an 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( seq 0 ( + , A ) ` i ) e. CC )
25 24 abscld 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> ( abs ` ( seq 0 ( + , A ) ` i ) ) e. RR )
26 18 25 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) e. RR )
27 26 ad2antrr 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) e. RR )
28 24 absge0d 
 |-  ( ( ph /\ i e. ( 0 ... ( j - 1 ) ) ) -> 0 <_ ( abs ` ( seq 0 ( + , A ) ` i ) ) )
29 18 25 28 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) )
30 29 ad2antrr 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> 0 <_ sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) )
31 27 30 ge0p1rpd 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) e. RR+ )
32 17 31 rpdivcld 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) e. RR+ )
33 1 2 3 4 5 abelthlem2 
 |-  ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
34 33 simpld 
 |-  ( ph -> 1 e. S )
35 oveq1 
 |-  ( x = 1 -> ( x ^ n ) = ( 1 ^ n ) )
36 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
37 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
38 36 37 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
39 35 38 sylan9eq 
 |-  ( ( x = 1 /\ n e. NN0 ) -> ( x ^ n ) = 1 )
40 39 oveq2d 
 |-  ( ( x = 1 /\ n e. NN0 ) -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` n ) x. 1 ) )
41 40 sumeq2dv 
 |-  ( x = 1 -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) = sum_ n e. NN0 ( ( A ` n ) x. 1 ) )
42 sumex 
 |-  sum_ n e. NN0 ( ( A ` n ) x. 1 ) e. _V
43 41 6 42 fvmpt 
 |-  ( 1 e. S -> ( F ` 1 ) = sum_ n e. NN0 ( ( A ` n ) x. 1 ) )
44 34 43 syl 
 |-  ( ph -> ( F ` 1 ) = sum_ n e. NN0 ( ( A ` n ) x. 1 ) )
45 1 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. CC )
46 45 mulid1d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. 1 ) = ( A ` n ) )
47 46 eqcomd 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) = ( ( A ` n ) x. 1 ) )
48 46 45 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. 1 ) e. CC )
49 8 19 47 48 7 isumclim 
 |-  ( ph -> sum_ n e. NN0 ( ( A ` n ) x. 1 ) = 0 )
50 44 49 eqtrd 
 |-  ( ph -> ( F ` 1 ) = 0 )
51 50 adantr 
 |-  ( ( ph /\ y e. S ) -> ( F ` 1 ) = 0 )
52 51 oveq1d 
 |-  ( ( ph /\ y e. S ) -> ( ( F ` 1 ) - ( F ` y ) ) = ( 0 - ( F ` y ) ) )
53 df-neg 
 |-  -u ( F ` y ) = ( 0 - ( F ` y ) )
54 52 53 eqtr4di 
 |-  ( ( ph /\ y e. S ) -> ( ( F ` 1 ) - ( F ` y ) ) = -u ( F ` y ) )
55 54 fveq2d 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) = ( abs ` -u ( F ` y ) ) )
56 1 2 3 4 5 6 abelthlem4 
 |-  ( ph -> F : S --> CC )
57 56 ffvelrnda 
 |-  ( ( ph /\ y e. S ) -> ( F ` y ) e. CC )
58 57 absnegd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` -u ( F ` y ) ) = ( abs ` ( F ` y ) ) )
59 55 58 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) = ( abs ` ( F ` y ) ) )
60 59 adantlr 
 |-  ( ( ( ph /\ R e. RR+ ) /\ y e. S ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) = ( abs ` ( F ` y ) ) )
61 60 ad2ant2r 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) = ( abs ` ( F ` y ) ) )
62 fveq2 
 |-  ( y = 1 -> ( F ` y ) = ( F ` 1 ) )
63 62 50 sylan9eqr 
 |-  ( ( ph /\ y = 1 ) -> ( F ` y ) = 0 )
64 63 abs00bd 
 |-  ( ( ph /\ y = 1 ) -> ( abs ` ( F ` y ) ) = 0 )
65 64 ad5ant15 
 |-  ( ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) /\ y = 1 ) -> ( abs ` ( F ` y ) ) = 0 )
66 simpllr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) -> R e. RR+ )
67 66 rpgt0d 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) -> 0 < R )
68 67 adantr 
 |-  ( ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) /\ y = 1 ) -> 0 < R )
69 65 68 eqbrtrd 
 |-  ( ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) /\ y = 1 ) -> ( abs ` ( F ` y ) ) < R )
70 1 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> A : NN0 --> CC )
71 2 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> seq 0 ( + , A ) e. dom ~~> )
72 3 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> M e. RR )
73 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> 0 <_ M )
74 7 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> seq 0 ( + , A ) ~~> 0 )
75 simprll 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> y e. S )
76 simprr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> y =/= 1 )
77 eldifsn 
 |-  ( y e. ( S \ { 1 } ) <-> ( y e. S /\ y =/= 1 ) )
78 75 76 77 sylanbrc 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> y e. ( S \ { 1 } ) )
79 13 ad2antrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( R / ( M + 1 ) ) e. RR+ )
80 simplrl 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> j e. NN0 )
81 simplrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) )
82 2fveq3 
 |-  ( k = m -> ( abs ` ( seq 0 ( + , A ) ` k ) ) = ( abs ` ( seq 0 ( + , A ) ` m ) ) )
83 82 breq1d 
 |-  ( k = m -> ( ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) <-> ( abs ` ( seq 0 ( + , A ) ` m ) ) < ( R / ( M + 1 ) ) ) )
84 83 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) <-> A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < ( R / ( M + 1 ) ) )
85 81 84 sylib 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < ( R / ( M + 1 ) ) )
86 simprlr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) )
87 2fveq3 
 |-  ( i = n -> ( abs ` ( seq 0 ( + , A ) ` i ) ) = ( abs ` ( seq 0 ( + , A ) ` n ) ) )
88 87 cbvsumv 
 |-  sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) = sum_ n e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) )
89 88 oveq1i 
 |-  ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) = ( sum_ n e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 )
90 89 oveq2i 
 |-  ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) = ( ( R / ( M + 1 ) ) / ( sum_ n e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) )
91 86 90 breqtrdi 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ n e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )
92 70 71 72 73 5 6 74 78 79 80 85 91 abelthlem7 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( abs ` ( F ` y ) ) < ( ( M + 1 ) x. ( R / ( M + 1 ) ) ) )
93 rpcn 
 |-  ( R e. RR+ -> R e. CC )
94 93 adantl 
 |-  ( ( ph /\ R e. RR+ ) -> R e. CC )
95 11 adantr 
 |-  ( ( ph /\ R e. RR+ ) -> ( M + 1 ) e. RR+ )
96 95 rpcnd 
 |-  ( ( ph /\ R e. RR+ ) -> ( M + 1 ) e. CC )
97 95 rpne0d 
 |-  ( ( ph /\ R e. RR+ ) -> ( M + 1 ) =/= 0 )
98 94 96 97 divcan2d 
 |-  ( ( ph /\ R e. RR+ ) -> ( ( M + 1 ) x. ( R / ( M + 1 ) ) ) = R )
99 98 ad2antrr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( ( M + 1 ) x. ( R / ( M + 1 ) ) ) = R )
100 92 99 breqtrd 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) /\ y =/= 1 ) ) -> ( abs ` ( F ` y ) ) < R )
101 100 anassrs 
 |-  ( ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) /\ y =/= 1 ) -> ( abs ` ( F ` y ) ) < R )
102 69 101 pm2.61dane 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) -> ( abs ` ( F ` y ) ) < R )
103 61 102 eqbrtrd 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ ( y e. S /\ ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R )
104 103 expr 
 |-  ( ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) /\ y e. S ) -> ( ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
105 104 ralrimiva 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> A. y e. S ( ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
106 breq2 
 |-  ( w = ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) -> ( ( abs ` ( 1 - y ) ) < w <-> ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) ) )
107 106 rspceaimv 
 |-  ( ( ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) e. RR+ /\ A. y e. S ( ( abs ` ( 1 - y ) ) < ( ( R / ( M + 1 ) ) / ( sum_ i e. ( 0 ... ( j - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` i ) ) + 1 ) ) -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
108 32 105 107 syl2anc 
 |-  ( ( ( ph /\ R e. RR+ ) /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < ( R / ( M + 1 ) ) ) ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
109 16 108 rexlimddv 
 |-  ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )