Metamath Proof Explorer

Theorem abelthlem5

Description: Lemma for abelth . (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 ) ) )
abelth.7 
|- ( ph -> seq 0 ( + , A ) ~~> 0 )
Assertion abelthlem5 
|- ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )

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 -> 0 e. ZZ )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( ph -> 1 e. RR+ )
12 eqidd 
 |-  ( ( ph /\ m e. NN0 ) -> ( seq 0 ( + , A ) ` m ) = ( seq 0 ( + , A ) ` m ) )
13 8 9 11 12 7 climi0 
 |-  ( ph -> E. j e. NN0 A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 )
14 13 adantr 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> E. j e. NN0 A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 )
15 simprl 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> j e. NN0 )
16 oveq2 
 |-  ( n = i -> ( ( abs ` X ) ^ n ) = ( ( abs ` X ) ^ i ) )
17 eqid 
 |-  ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) = ( n e. NN0 |-> ( ( abs ` X ) ^ n ) )
18 ovex 
 |-  ( ( abs ` X ) ^ i ) e. _V
19 16 17 18 fvmpt 
 |-  ( i e. NN0 -> ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) = ( ( abs ` X ) ^ i ) )
20 19 adantl 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) = ( ( abs ` X ) ^ i ) )
21 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
22 0cn 
 |-  0 e. CC
23 1xr 
 |-  1 e. RR*
24 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
25 21 22 23 24 mp3an 
 |-  ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
26 simplr 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
27 25 26 sselid 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> X e. CC )
28 27 abscld 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` X ) e. RR )
29 reexpcl 
 |-  ( ( ( abs ` X ) e. RR /\ i e. NN0 ) -> ( ( abs ` X ) ^ i ) e. RR )
30 28 29 sylan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( abs ` X ) ^ i ) e. RR )
31 20 30 eqeltrd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) e. RR )
32 fveq2 
 |-  ( k = i -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` i ) )
33 oveq2 
 |-  ( k = i -> ( X ^ k ) = ( X ^ i ) )
34 32 33 oveq12d 
 |-  ( k = i -> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) )
35 eqid 
 |-  ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) )
36 ovex 
 |-  ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) e. _V
37 34 35 36 fvmpt 
 |-  ( i e. NN0 -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) )
38 37 adantl 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) )
39 1 ffvelrnda 
 |-  ( ( ph /\ x e. NN0 ) -> ( A ` x ) e. CC )
40 8 9 39 serf 
 |-  ( ph -> seq 0 ( + , A ) : NN0 --> CC )
41 40 ad2antrr 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> seq 0 ( + , A ) : NN0 --> CC )
42 41 ffvelrnda 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( seq 0 ( + , A ) ` i ) e. CC )
43 expcl 
 |-  ( ( X e. CC /\ i e. NN0 ) -> ( X ^ i ) e. CC )
44 27 43 sylan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( X ^ i ) e. CC )
45 42 44 mulcld 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) e. CC )
46 38 45 eqeltrd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) e. CC )
47 28 recnd 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` X ) e. CC )
48 absidm 
 |-  ( X e. CC -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
49 27 48 syl 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
50 eqid 
 |-  ( abs o. - ) = ( abs o. - )
51 50 cnmetdval 
 |-  ( ( X e. CC /\ 0 e. CC ) -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
52 27 22 51 sylancl 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
53 27 subid1d 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( X - 0 ) = X )
54 53 fveq2d 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
55 52 54 eqtrd 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( X ( abs o. - ) 0 ) = ( abs ` X ) )
56 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ X e. CC ) ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
57 21 23 56 mpanl12 
 |-  ( ( 0 e. CC /\ X e. CC ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
58 22 27 57 sylancr 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
59 26 58 mpbid 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( X ( abs o. - ) 0 ) < 1 )
60 55 59 eqbrtrrd 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` X ) < 1 )
61 49 60 eqbrtrd 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> ( abs ` ( abs ` X ) ) < 1 )
62 47 61 20 geolim 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` X ) ) ) )
63 climrel 
 |-  Rel ~~>
64 63 releldmi 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` X ) ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ) e. dom ~~> )
65 62 64 syl 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ) e. dom ~~> )
66 1red 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> 1 e. RR )
67 41 adantr 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> seq 0 ( + , A ) : NN0 --> CC )
68 eluznn0 
 |-  ( ( j e. NN0 /\ i e. ( ZZ>= ` j ) ) -> i e. NN0 )
69 15 68 sylan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> i e. NN0 )
70 67 69 ffvelrnd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( seq 0 ( + , A ) ` i ) e. CC )
71 69 44 syldan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( X ^ i ) e. CC )
72 70 71 absmuld 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` i ) ) x. ( abs ` ( X ^ i ) ) ) )
73 27 adantr 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> X e. CC )
74 73 69 absexpd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( X ^ i ) ) = ( ( abs ` X ) ^ i ) )
75 74 oveq2d 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( abs ` ( seq 0 ( + , A ) ` i ) ) x. ( abs ` ( X ^ i ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` i ) ) x. ( ( abs ` X ) ^ i ) ) )
76 72 75 eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` i ) ) x. ( ( abs ` X ) ^ i ) ) )
77 70 abscld 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( seq 0 ( + , A ) ` i ) ) e. RR )
78 1red 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> 1 e. RR )
79 69 30 syldan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( abs ` X ) ^ i ) e. RR )
80 71 absge0d 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> 0 <_ ( abs ` ( X ^ i ) ) )
81 80 74 breqtrd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> 0 <_ ( ( abs ` X ) ^ i ) )
82 simprr 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 )
83 2fveq3 
 |-  ( m = i -> ( abs ` ( seq 0 ( + , A ) ` m ) ) = ( abs ` ( seq 0 ( + , A ) ` i ) ) )
84 83 breq1d 
 |-  ( m = i -> ( ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 <-> ( abs ` ( seq 0 ( + , A ) ` i ) ) < 1 ) )
85 84 rspccva 
 |-  ( ( A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( seq 0 ( + , A ) ` i ) ) < 1 )
86 82 85 sylan 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( seq 0 ( + , A ) ` i ) ) < 1 )
87 1re 
 |-  1 e. RR
88 ltle 
 |-  ( ( ( abs ` ( seq 0 ( + , A ) ` i ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( seq 0 ( + , A ) ` i ) ) < 1 -> ( abs ` ( seq 0 ( + , A ) ` i ) ) <_ 1 ) )
89 77 87 88 sylancl 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( abs ` ( seq 0 ( + , A ) ` i ) ) < 1 -> ( abs ` ( seq 0 ( + , A ) ` i ) ) <_ 1 ) )
90 86 89 mpd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( seq 0 ( + , A ) ` i ) ) <_ 1 )
91 77 78 79 81 90 lemul1ad 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( abs ` ( seq 0 ( + , A ) ` i ) ) x. ( ( abs ` X ) ^ i ) ) <_ ( 1 x. ( ( abs ` X ) ^ i ) ) )
92 76 91 eqbrtrd 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) <_ ( 1 x. ( ( abs ` X ) ^ i ) ) )
93 69 37 syl 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) = ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) )
94 93 fveq2d 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) ) = ( abs ` ( ( seq 0 ( + , A ) ` i ) x. ( X ^ i ) ) ) )
95 69 19 syl 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) = ( ( abs ` X ) ^ i ) )
96 95 oveq2d 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( 1 x. ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) ) = ( 1 x. ( ( abs ` X ) ^ i ) ) )
97 92 94 96 3brtr4d 
 |-  ( ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) /\ i e. ( ZZ>= ` j ) ) -> ( abs ` ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` i ) ) <_ ( 1 x. ( ( n e. NN0 |-> ( ( abs ` X ) ^ n ) ) ` i ) ) )
98 8 15 31 46 65 66 97 cvgcmpce 
 |-  ( ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) /\ ( j e. NN0 /\ A. m e. ( ZZ>= ` j ) ( abs ` ( seq 0 ( + , A ) ` m ) ) < 1 ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )
99 14 98 rexlimddv 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )