Metamath Proof Explorer

Theorem abelthlem7

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 } ) )
abelthlem7.2 
|- ( ph -> R e. RR+ )
abelthlem7.3 
|- ( ph -> N e. NN0 )
abelthlem7.4 
|- ( ph -> A. k e. ( ZZ>= ` N ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < R )
abelthlem7.5 
|- ( ph -> ( abs ` ( 1 - X ) ) < ( R / ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )
Assertion abelthlem7 
|- ( ph -> ( abs ` ( F ` X ) ) < ( ( M + 1 ) x. 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 abelthlem6.1 
 |-  ( ph -> X e. ( S \ { 1 } ) )
9 abelthlem7.2 
 |-  ( ph -> R e. RR+ )
10 abelthlem7.3 
 |-  ( ph -> N e. NN0 )
11 abelthlem7.4 
 |-  ( ph -> A. k e. ( ZZ>= ` N ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < R )
12 abelthlem7.5 
 |-  ( ph -> ( abs ` ( 1 - X ) ) < ( R / ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )
13 1 2 3 4 5 6 abelthlem4 
 |-  ( ph -> F : S --> CC )
14 8 eldifad 
 |-  ( ph -> X e. S )
15 13 14 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. CC )
16 15 abscld 
 |-  ( ph -> ( abs ` ( F ` X ) ) e. RR )
17 ax-1cn 
 |-  1 e. CC
18 1 2 3 4 5 6 7 8 abelthlem7a 
 |-  ( ph -> ( X e. CC /\ ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )
19 18 simpld 
 |-  ( ph -> X e. CC )
20 subcl 
 |-  ( ( 1 e. CC /\ X e. CC ) -> ( 1 - X ) e. CC )
21 17 19 20 sylancr 
 |-  ( ph -> ( 1 - X ) e. CC )
22 fzfid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) e. Fin )
23 elfznn0 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. NN0 )
24 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
25 0zd 
 |-  ( ph -> 0 e. ZZ )
26 1 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. CC )
27 24 25 26 serf 
 |-  ( ph -> seq 0 ( + , A ) : NN0 --> CC )
28 27 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( seq 0 ( + , A ) ` n ) e. CC )
29 expcl 
 |-  ( ( X e. CC /\ n e. NN0 ) -> ( X ^ n ) e. CC )
30 19 29 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( X ^ n ) e. CC )
31 28 30 mulcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC )
32 23 31 sylan2 
 |-  ( ( ph /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC )
33 22 32 fsumcl 
 |-  ( ph -> sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC )
34 21 33 mulcld 
 |-  ( ph -> ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. CC )
35 34 abscld 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) e. RR )
36 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
37 10 nn0zd 
 |-  ( ph -> N e. ZZ )
38 eluznn0 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> n e. NN0 )
39 10 38 sylan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. NN0 )
40 fveq2 
 |-  ( k = n -> ( seq 0 ( + , A ) ` k ) = ( seq 0 ( + , A ) ` n ) )
41 oveq2 
 |-  ( k = n -> ( X ^ k ) = ( X ^ n ) )
42 40 41 oveq12d 
 |-  ( k = n -> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) )
43 eqid 
 |-  ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) )
44 ovex 
 |-  ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. _V
45 42 43 44 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) )
46 39 45 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) )
47 39 31 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC )
48 1 2 3 4 5 abelthlem2 
 |-  ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
49 48 simprd 
 |-  ( ph -> ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) )
50 49 8 sseldd 
 |-  ( ph -> X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
51 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 ~~> )
52 50 51 mpdan 
 |-  ( ph -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )
53 45 adantl 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) = ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) )
54 53 31 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) e. CC )
55 24 10 54 iserex 
 |-  ( ph -> ( seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> <-> seq N ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> ) )
56 52 55 mpbid 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )
57 36 37 46 47 56 isumcl 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC )
58 21 57 mulcld 
 |-  ( ph -> ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. CC )
59 58 abscld 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) e. RR )
60 35 59 readdcld 
 |-  ( ph -> ( ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) + ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) e. RR )
61 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
62 3 61 syl 
 |-  ( ph -> ( M + 1 ) e. RR )
63 9 rpred 
 |-  ( ph -> R e. RR )
64 62 63 remulcld 
 |-  ( ph -> ( ( M + 1 ) x. R ) e. RR )
65 1 2 3 4 5 6 7 8 abelthlem6 
 |-  ( ph -> ( F ` X ) = ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
66 24 36 10 53 31 52 isumsplit 
 |-  ( ph -> sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) = ( sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) + sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
67 66 oveq2d 
 |-  ( ph -> ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( ( 1 - X ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) + sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
68 21 33 57 adddid 
 |-  ( ph -> ( ( 1 - X ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) + sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
69 65 67 68 3eqtrd 
 |-  ( ph -> ( F ` X ) = ( ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
70 69 fveq2d 
 |-  ( ph -> ( abs ` ( F ` X ) ) = ( abs ` ( ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) )
71 34 58 abstrid 
 |-  ( ph -> ( abs ` ( ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) + ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) <_ ( ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) + ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) )
72 70 71 eqbrtrd 
 |-  ( ph -> ( abs ` ( F ` X ) ) <_ ( ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) + ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) )
73 3 63 remulcld 
 |-  ( ph -> ( M x. R ) e. RR )
74 21 abscld 
 |-  ( ph -> ( abs ` ( 1 - X ) ) e. RR )
75 28 abscld 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) e. RR )
76 23 75 sylan2 
 |-  ( ( ph /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) e. RR )
77 22 76 fsumrecl 
 |-  ( ph -> sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) e. RR )
78 peano2re 
 |-  ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) e. RR -> ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) e. RR )
79 77 78 syl 
 |-  ( ph -> ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) e. RR )
80 74 79 remulcld 
 |-  ( ph -> ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) e. RR )
81 21 33 absmuld 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( ( abs ` ( 1 - X ) ) x. ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
82 33 abscld 
 |-  ( ph -> ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
83 21 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( 1 - X ) ) )
84 31 abscld 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
85 23 84 sylan2 
 |-  ( ( ph /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
86 22 85 fsumrecl 
 |-  ( ph -> sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
87 22 32 fsumabs 
 |-  ( ph -> ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
88 19 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
89 reexpcl 
 |-  ( ( ( abs ` X ) e. RR /\ n e. NN0 ) -> ( ( abs ` X ) ^ n ) e. RR )
90 88 89 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` X ) ^ n ) e. RR )
91 1red 
 |-  ( ( ph /\ n e. NN0 ) -> 1 e. RR )
92 28 absge0d 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( abs ` ( seq 0 ( + , A ) ` n ) ) )
93 88 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` X ) e. RR )
94 19 absge0d 
 |-  ( ph -> 0 <_ ( abs ` X ) )
95 94 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> 0 <_ ( abs ` X ) )
96 0cn 
 |-  0 e. CC
97 eqid 
 |-  ( abs o. - ) = ( abs o. - )
98 97 cnmetdval 
 |-  ( ( X e. CC /\ 0 e. CC ) -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
99 19 96 98 sylancl 
 |-  ( ph -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
100 19 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
101 100 fveq2d 
 |-  ( ph -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
102 99 101 eqtrd 
 |-  ( ph -> ( X ( abs o. - ) 0 ) = ( abs ` X ) )
103 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
104 1xr 
 |-  1 e. RR*
105 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 ) )
106 103 104 105 mpanl12 
 |-  ( ( 0 e. CC /\ X e. CC ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
107 96 19 106 sylancr 
 |-  ( ph -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
108 50 107 mpbid 
 |-  ( ph -> ( X ( abs o. - ) 0 ) < 1 )
109 102 108 eqbrtrrd 
 |-  ( ph -> ( abs ` X ) < 1 )
110 1re 
 |-  1 e. RR
111 ltle 
 |-  ( ( ( abs ` X ) e. RR /\ 1 e. RR ) -> ( ( abs ` X ) < 1 -> ( abs ` X ) <_ 1 ) )
112 88 110 111 sylancl 
 |-  ( ph -> ( ( abs ` X ) < 1 -> ( abs ` X ) <_ 1 ) )
113 109 112 mpd 
 |-  ( ph -> ( abs ` X ) <_ 1 )
114 113 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` X ) <_ 1 )
115 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
116 exple1 
 |-  ( ( ( ( abs ` X ) e. RR /\ 0 <_ ( abs ` X ) /\ ( abs ` X ) <_ 1 ) /\ n e. NN0 ) -> ( ( abs ` X ) ^ n ) <_ 1 )
117 93 95 114 115 116 syl31anc 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` X ) ^ n ) <_ 1 )
118 90 91 75 92 117 lemul2ad 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) <_ ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. 1 ) )
119 28 30 absmuld 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( abs ` ( X ^ n ) ) ) )
120 absexp 
 |-  ( ( X e. CC /\ n e. NN0 ) -> ( abs ` ( X ^ n ) ) = ( ( abs ` X ) ^ n ) )
121 19 120 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( X ^ n ) ) = ( ( abs ` X ) ^ n ) )
122 121 oveq2d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( abs ` ( X ^ n ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) )
123 119 122 eqtr2d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
124 75 recnd 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) e. CC )
125 124 mulid1d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. 1 ) = ( abs ` ( seq 0 ( + , A ) ` n ) ) )
126 118 123 125 3brtr3d 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( abs ` ( seq 0 ( + , A ) ` n ) ) )
127 23 126 sylan2 
 |-  ( ( ph /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( abs ` ( seq 0 ( + , A ) ` n ) ) )
128 22 85 76 127 fsumle 
 |-  ( ph -> sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) )
129 82 86 77 87 128 letrd 
 |-  ( ph -> ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) )
130 77 ltp1d 
 |-  ( ph -> sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) < ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) )
131 82 77 79 129 130 lelttrd 
 |-  ( ph -> ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) < ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) )
132 82 79 131 ltled 
 |-  ( ph -> ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) )
133 82 79 74 83 132 lemul2ad 
 |-  ( ph -> ( ( abs ` ( 1 - X ) ) x. ( abs ` sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) <_ ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )
134 81 133 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) <_ ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )
135 0red 
 |-  ( ph -> 0 e. RR )
136 23 92 sylan2 
 |-  ( ( ph /\ n e. ( 0 ... ( N - 1 ) ) ) -> 0 <_ ( abs ` ( seq 0 ( + , A ) ` n ) ) )
137 22 76 136 fsumge0 
 |-  ( ph -> 0 <_ sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) )
138 135 77 79 137 130 lelttrd 
 |-  ( ph -> 0 < ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) )
139 ltmuldiv 
 |-  ( ( ( abs ` ( 1 - X ) ) e. RR /\ R e. RR /\ ( ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) e. RR /\ 0 < ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) ) -> ( ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) < R <-> ( abs ` ( 1 - X ) ) < ( R / ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) ) )
140 74 63 79 138 139 syl112anc 
 |-  ( ph -> ( ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) < R <-> ( abs ` ( 1 - X ) ) < ( R / ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) ) )
141 12 140 mpbird 
 |-  ( ph -> ( ( abs ` ( 1 - X ) ) x. ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) < R )
142 35 80 63 134 141 lelttrd 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) < R )
143 21 57 absmuld 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( ( abs ` ( 1 - X ) ) x. ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
144 57 abscld 
 |-  ( ph -> ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
145 42 fveq2d 
 |-  ( k = n -> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
146 eqid 
 |-  ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) = ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) )
147 fvex 
 |-  ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. _V
148 145 146 147 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
149 39 148 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
150 47 abscld 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
151 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
152 37 151 syl 
 |-  ( ph -> N e. ( ZZ>= ` N ) )
153 oveq2 
 |-  ( k = n -> ( ( abs ` X ) ^ k ) = ( ( abs ` X ) ^ n ) )
154 eqid 
 |-  ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) = ( k e. NN0 |-> ( ( abs ` X ) ^ k ) )
155 ovex 
 |-  ( ( abs ` X ) ^ n ) e. _V
156 153 154 155 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) = ( ( abs ` X ) ^ n ) )
157 39 156 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) = ( ( abs ` X ) ^ n ) )
158 39 90 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( abs ` X ) ^ n ) e. RR )
159 157 158 eqeltrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) e. RR )
160 150 recnd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. CC )
161 149 160 eqeltrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) e. CC )
162 88 recnd 
 |-  ( ph -> ( abs ` X ) e. CC )
163 absidm 
 |-  ( X e. CC -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
164 19 163 syl 
 |-  ( ph -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
165 164 109 eqbrtrd 
 |-  ( ph -> ( abs ` ( abs ` X ) ) < 1 )
166 162 165 10 157 geolim2 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ) ~~> ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) )
167 seqex 
 |-  seq N ( + , ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ) e. _V
168 ovex 
 |-  ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) e. _V
169 167 168 breldm 
 |-  ( seq N ( + , ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ) ~~> ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) -> seq N ( + , ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ) e. dom ~~> )
170 166 169 syl 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ) e. dom ~~> )
171 119 122 eqtrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) )
172 39 171 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) = ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) )
173 39 75 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) e. RR )
174 63 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> R e. RR )
175 88 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` X ) e. RR )
176 94 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> 0 <_ ( abs ` X ) )
177 175 39 176 expge0d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> 0 <_ ( ( abs ` X ) ^ n ) )
178 40 fveq2d 
 |-  ( k = n -> ( abs ` ( seq 0 ( + , A ) ` k ) ) = ( abs ` ( seq 0 ( + , A ) ` n ) ) )
179 178 breq1d 
 |-  ( k = n -> ( ( abs ` ( seq 0 ( + , A ) ` k ) ) < R <-> ( abs ` ( seq 0 ( + , A ) ` n ) ) < R ) )
180 179 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` N ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < R /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) < R )
181 11 180 sylan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) < R )
182 173 174 181 ltled 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( seq 0 ( + , A ) ` n ) ) <_ R )
183 173 174 158 177 182 lemul1ad 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( abs ` ( seq 0 ( + , A ) ` n ) ) x. ( ( abs ` X ) ^ n ) ) <_ ( R x. ( ( abs ` X ) ^ n ) ) )
184 172 183 eqbrtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( R x. ( ( abs ` X ) ^ n ) ) )
185 149 fveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) ) = ( abs ` ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) )
186 absidm 
 |-  ( ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) e. CC -> ( abs ` ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
187 47 186 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
188 185 187 eqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
189 157 oveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( R x. ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) ) = ( R x. ( ( abs ` X ) ^ n ) ) )
190 184 188 189 3brtr4d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) ) <_ ( R x. ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) ) )
191 36 152 159 161 170 63 190 cvgcmpce 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ) e. dom ~~> )
192 36 37 149 150 191 isumrecl 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) e. RR )
193 eldifsni 
 |-  ( X e. ( S \ { 1 } ) -> X =/= 1 )
194 8 193 syl 
 |-  ( ph -> X =/= 1 )
195 194 necomd 
 |-  ( ph -> 1 =/= X )
196 subeq0 
 |-  ( ( 1 e. CC /\ X e. CC ) -> ( ( 1 - X ) = 0 <-> 1 = X ) )
197 196 necon3bid 
 |-  ( ( 1 e. CC /\ X e. CC ) -> ( ( 1 - X ) =/= 0 <-> 1 =/= X ) )
198 17 19 197 sylancr 
 |-  ( ph -> ( ( 1 - X ) =/= 0 <-> 1 =/= X ) )
199 195 198 mpbird 
 |-  ( ph -> ( 1 - X ) =/= 0 )
200 21 199 absrpcld 
 |-  ( ph -> ( abs ` ( 1 - X ) ) e. RR+ )
201 73 200 rerpdivcld 
 |-  ( ph -> ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) e. RR )
202 36 37 46 47 56 isumclim2 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ~~> sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) )
203 36 37 149 160 191 isumclim2 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ) ~~> sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
204 39 54 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) e. CC )
205 46 fveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) ) = ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
206 149 205 eqtr4d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( abs ` ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) ` n ) = ( abs ` ( ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ` n ) ) )
207 36 202 203 37 204 206 iserabs 
 |-  ( ph -> ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
208 88 10 reexpcld 
 |-  ( ph -> ( ( abs ` X ) ^ N ) e. RR )
209 difrp 
 |-  ( ( ( abs ` X ) e. RR /\ 1 e. RR ) -> ( ( abs ` X ) < 1 <-> ( 1 - ( abs ` X ) ) e. RR+ ) )
210 88 110 209 sylancl 
 |-  ( ph -> ( ( abs ` X ) < 1 <-> ( 1 - ( abs ` X ) ) e. RR+ ) )
211 109 210 mpbid 
 |-  ( ph -> ( 1 - ( abs ` X ) ) e. RR+ )
212 208 211 rerpdivcld 
 |-  ( ph -> ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) e. RR )
213 63 212 remulcld 
 |-  ( ph -> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) e. RR )
214 153 oveq2d 
 |-  ( k = n -> ( R x. ( ( abs ` X ) ^ k ) ) = ( R x. ( ( abs ` X ) ^ n ) ) )
215 eqid 
 |-  ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) = ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) )
216 ovex 
 |-  ( R x. ( ( abs ` X ) ^ n ) ) e. _V
217 214 215 216 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ` n ) = ( R x. ( ( abs ` X ) ^ n ) ) )
218 39 217 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ` n ) = ( R x. ( ( abs ` X ) ^ n ) ) )
219 174 158 remulcld 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( R x. ( ( abs ` X ) ^ n ) ) e. RR )
220 9 rpcnd 
 |-  ( ph -> R e. CC )
221 159 recnd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) e. CC )
222 218 189 eqtr4d 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ` n ) = ( R x. ( ( k e. NN0 |-> ( ( abs ` X ) ^ k ) ) ` n ) ) )
223 36 37 220 166 221 222 isermulc2 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ) ~~> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) )
224 seqex 
 |-  seq N ( + , ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ) e. _V
225 ovex 
 |-  ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) e. _V
226 224 225 breldm 
 |-  ( seq N ( + , ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ) ~~> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) -> seq N ( + , ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ) e. dom ~~> )
227 223 226 syl 
 |-  ( ph -> seq N ( + , ( k e. NN0 |-> ( R x. ( ( abs ` X ) ^ k ) ) ) ) e. dom ~~> )
228 36 37 149 150 218 219 184 191 227 isumle 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ sum_ n e. ( ZZ>= ` N ) ( R x. ( ( abs ` X ) ^ n ) ) )
229 219 recnd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( R x. ( ( abs ` X ) ^ n ) ) e. CC )
230 36 37 218 229 223 isumclim 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( R x. ( ( abs ` X ) ^ n ) ) = ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) )
231 228 230 breqtrd 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) )
232 9 211 rpdivcld 
 |-  ( ph -> ( R / ( 1 - ( abs ` X ) ) ) e. RR+ )
233 232 rpred 
 |-  ( ph -> ( R / ( 1 - ( abs ` X ) ) ) e. RR )
234 208 recnd 
 |-  ( ph -> ( ( abs ` X ) ^ N ) e. CC )
235 211 rpcnd 
 |-  ( ph -> ( 1 - ( abs ` X ) ) e. CC )
236 211 rpne0d 
 |-  ( ph -> ( 1 - ( abs ` X ) ) =/= 0 )
237 220 234 235 236 div12d 
 |-  ( ph -> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) = ( ( ( abs ` X ) ^ N ) x. ( R / ( 1 - ( abs ` X ) ) ) ) )
238 1red 
 |-  ( ph -> 1 e. RR )
239 232 rpge0d 
 |-  ( ph -> 0 <_ ( R / ( 1 - ( abs ` X ) ) ) )
240 exple1 
 |-  ( ( ( ( abs ` X ) e. RR /\ 0 <_ ( abs ` X ) /\ ( abs ` X ) <_ 1 ) /\ N e. NN0 ) -> ( ( abs ` X ) ^ N ) <_ 1 )
241 88 94 113 10 240 syl31anc 
 |-  ( ph -> ( ( abs ` X ) ^ N ) <_ 1 )
242 208 238 233 239 241 lemul1ad 
 |-  ( ph -> ( ( ( abs ` X ) ^ N ) x. ( R / ( 1 - ( abs ` X ) ) ) ) <_ ( 1 x. ( R / ( 1 - ( abs ` X ) ) ) ) )
243 232 rpcnd 
 |-  ( ph -> ( R / ( 1 - ( abs ` X ) ) ) e. CC )
244 243 mulid2d 
 |-  ( ph -> ( 1 x. ( R / ( 1 - ( abs ` X ) ) ) ) = ( R / ( 1 - ( abs ` X ) ) ) )
245 242 244 breqtrd 
 |-  ( ph -> ( ( ( abs ` X ) ^ N ) x. ( R / ( 1 - ( abs ` X ) ) ) ) <_ ( R / ( 1 - ( abs ` X ) ) ) )
246 237 245 eqbrtrd 
 |-  ( ph -> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) <_ ( R / ( 1 - ( abs ` X ) ) ) )
247 18 simprd 
 |-  ( ph -> ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) )
248 resubcl 
 |-  ( ( 1 e. RR /\ ( abs ` X ) e. RR ) -> ( 1 - ( abs ` X ) ) e. RR )
249 110 88 248 sylancr 
 |-  ( ph -> ( 1 - ( abs ` X ) ) e. RR )
250 3 249 remulcld 
 |-  ( ph -> ( M x. ( 1 - ( abs ` X ) ) ) e. RR )
251 74 250 9 lemul2d 
 |-  ( ph -> ( ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) <-> ( R x. ( abs ` ( 1 - X ) ) ) <_ ( R x. ( M x. ( 1 - ( abs ` X ) ) ) ) ) )
252 247 251 mpbid 
 |-  ( ph -> ( R x. ( abs ` ( 1 - X ) ) ) <_ ( R x. ( M x. ( 1 - ( abs ` X ) ) ) ) )
253 3 recnd 
 |-  ( ph -> M e. CC )
254 220 253 235 mul12d 
 |-  ( ph -> ( R x. ( M x. ( 1 - ( abs ` X ) ) ) ) = ( M x. ( R x. ( 1 - ( abs ` X ) ) ) ) )
255 220 235 mulcomd 
 |-  ( ph -> ( R x. ( 1 - ( abs ` X ) ) ) = ( ( 1 - ( abs ` X ) ) x. R ) )
256 255 oveq2d 
 |-  ( ph -> ( M x. ( R x. ( 1 - ( abs ` X ) ) ) ) = ( M x. ( ( 1 - ( abs ` X ) ) x. R ) ) )
257 253 235 220 mul12d 
 |-  ( ph -> ( M x. ( ( 1 - ( abs ` X ) ) x. R ) ) = ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) )
258 254 256 257 3eqtrd 
 |-  ( ph -> ( R x. ( M x. ( 1 - ( abs ` X ) ) ) ) = ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) )
259 252 258 breqtrd 
 |-  ( ph -> ( R x. ( abs ` ( 1 - X ) ) ) <_ ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) )
260 249 73 remulcld 
 |-  ( ph -> ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) e. RR )
261 63 260 200 lemuldivd 
 |-  ( ph -> ( ( R x. ( abs ` ( 1 - X ) ) ) <_ ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) <-> R <_ ( ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) / ( abs ` ( 1 - X ) ) ) ) )
262 259 261 mpbid 
 |-  ( ph -> R <_ ( ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) / ( abs ` ( 1 - X ) ) ) )
263 73 recnd 
 |-  ( ph -> ( M x. R ) e. CC )
264 74 recnd 
 |-  ( ph -> ( abs ` ( 1 - X ) ) e. CC )
265 200 rpne0d 
 |-  ( ph -> ( abs ` ( 1 - X ) ) =/= 0 )
266 235 263 264 265 divassd 
 |-  ( ph -> ( ( ( 1 - ( abs ` X ) ) x. ( M x. R ) ) / ( abs ` ( 1 - X ) ) ) = ( ( 1 - ( abs ` X ) ) x. ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) ) )
267 262 266 breqtrd 
 |-  ( ph -> R <_ ( ( 1 - ( abs ` X ) ) x. ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) ) )
268 posdif 
 |-  ( ( ( abs ` X ) e. RR /\ 1 e. RR ) -> ( ( abs ` X ) < 1 <-> 0 < ( 1 - ( abs ` X ) ) ) )
269 88 110 268 sylancl 
 |-  ( ph -> ( ( abs ` X ) < 1 <-> 0 < ( 1 - ( abs ` X ) ) ) )
270 109 269 mpbid 
 |-  ( ph -> 0 < ( 1 - ( abs ` X ) ) )
271 ledivmul 
 |-  ( ( R e. RR /\ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) e. RR /\ ( ( 1 - ( abs ` X ) ) e. RR /\ 0 < ( 1 - ( abs ` X ) ) ) ) -> ( ( R / ( 1 - ( abs ` X ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) <-> R <_ ( ( 1 - ( abs ` X ) ) x. ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) ) ) )
272 63 201 249 270 271 syl112anc 
 |-  ( ph -> ( ( R / ( 1 - ( abs ` X ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) <-> R <_ ( ( 1 - ( abs ` X ) ) x. ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) ) ) )
273 267 272 mpbird 
 |-  ( ph -> ( R / ( 1 - ( abs ` X ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) )
274 213 233 201 246 273 letrd 
 |-  ( ph -> ( R x. ( ( ( abs ` X ) ^ N ) / ( 1 - ( abs ` X ) ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) )
275 192 213 201 231 274 letrd 
 |-  ( ph -> sum_ n e. ( ZZ>= ` N ) ( abs ` ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) )
276 144 192 201 207 275 letrd 
 |-  ( ph -> ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) )
277 144 73 200 lemuldiv2d 
 |-  ( ph -> ( ( ( abs ` ( 1 - X ) ) x. ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) <_ ( M x. R ) <-> ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) <_ ( ( M x. R ) / ( abs ` ( 1 - X ) ) ) ) )
278 276 277 mpbird 
 |-  ( ph -> ( ( abs ` ( 1 - X ) ) x. ( abs ` sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) <_ ( M x. R ) )
279 143 278 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) <_ ( M x. R ) )
280 35 59 63 73 142 279 ltleaddd 
 |-  ( ph -> ( ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) + ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) < ( R + ( M x. R ) ) )
281 1cnd 
 |-  ( ph -> 1 e. CC )
282 253 281 220 adddird 
 |-  ( ph -> ( ( M + 1 ) x. R ) = ( ( M x. R ) + ( 1 x. R ) ) )
283 220 mulid2d 
 |-  ( ph -> ( 1 x. R ) = R )
284 283 oveq2d 
 |-  ( ph -> ( ( M x. R ) + ( 1 x. R ) ) = ( ( M x. R ) + R ) )
285 263 220 addcomd 
 |-  ( ph -> ( ( M x. R ) + R ) = ( R + ( M x. R ) ) )
286 282 284 285 3eqtrd 
 |-  ( ph -> ( ( M + 1 ) x. R ) = ( R + ( M x. R ) ) )
287 280 286 breqtrrd 
 |-  ( ph -> ( ( abs ` ( ( 1 - X ) x. sum_ n e. ( 0 ... ( N - 1 ) ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) + ( abs ` ( ( 1 - X ) x. sum_ n e. ( ZZ>= ` N ) ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) ) ) < ( ( M + 1 ) x. R ) )
288 16 60 64 72 287 lelttrd 
 |-  ( ph -> ( abs ` ( F ` X ) ) < ( ( M + 1 ) x. R ) )