Metamath Proof Explorer

Theorem ftalem1

Description: Lemma for fta : "growth lemma". There exists some r such that F is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses ftalem.1 
|- A = ( coeff ` F )
ftalem.2 
|- N = ( deg ` F )
ftalem.3 
|- ( ph -> F e. ( Poly ` S ) )
ftalem.4 
|- ( ph -> N e. NN )
ftalem1.5 
|- ( ph -> E e. RR+ )
ftalem1.6 
|- T = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E )
Assertion ftalem1 
|- ( ph -> E. r e. RR A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 
 |-  A = ( coeff ` F )
2 ftalem.2 
 |-  N = ( deg ` F )
3 ftalem.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 ftalem.4 
 |-  ( ph -> N e. NN )
5 ftalem1.5 
 |-  ( ph -> E e. RR+ )
6 ftalem1.6 
 |-  T = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E )
7 fzfid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) e. Fin )
8 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
9 3 8 syl 
 |-  ( ph -> A : NN0 --> CC )
10 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
11 ffvelrn 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
12 9 10 11 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A ` k ) e. CC )
13 12 abscld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( A ` k ) ) e. RR )
14 7 13 fsumrecl 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) e. RR )
15 14 5 rerpdivcld 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E ) e. RR )
16 6 15 eqeltrid 
 |-  ( ph -> T e. RR )
17 1re 
 |-  1 e. RR
18 ifcl 
 |-  ( ( T e. RR /\ 1 e. RR ) -> if ( 1 <_ T , T , 1 ) e. RR )
19 16 17 18 sylancl 
 |-  ( ph -> if ( 1 <_ T , T , 1 ) e. RR )
20 fzfid 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( 0 ... ( N - 1 ) ) e. Fin )
21 9 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> A : NN0 --> CC )
22 21 11 sylan 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
23 simprl 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> x e. CC )
24 expcl 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( x ^ k ) e. CC )
25 23 24 sylan 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. NN0 ) -> ( x ^ k ) e. CC )
26 22 25 mulcld 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( x ^ k ) ) e. CC )
27 10 26 sylan2 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( A ` k ) x. ( x ^ k ) ) e. CC )
28 20 27 fsumcl 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) e. CC )
29 4 nnnn0d 
 |-  ( ph -> N e. NN0 )
30 29 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> N e. NN0 )
31 21 30 ffvelrnd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( A ` N ) e. CC )
32 23 30 expcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( x ^ N ) e. CC )
33 31 32 mulcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( A ` N ) x. ( x ^ N ) ) e. CC )
34 3 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> F e. ( Poly ` S ) )
35 1 2 coeid2 
 |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( F ` x ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) )
36 34 23 35 syl2anc 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( F ` x ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) )
37 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
38 30 37 eleqtrdi 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> N e. ( ZZ>= ` 0 ) )
39 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
40 39 26 sylan2 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( x ^ k ) ) e. CC )
41 fveq2 
 |-  ( k = N -> ( A ` k ) = ( A ` N ) )
42 oveq2 
 |-  ( k = N -> ( x ^ k ) = ( x ^ N ) )
43 41 42 oveq12d 
 |-  ( k = N -> ( ( A ` k ) x. ( x ^ k ) ) = ( ( A ` N ) x. ( x ^ N ) ) )
44 38 40 43 fsumm1 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) + ( ( A ` N ) x. ( x ^ N ) ) ) )
45 36 44 eqtrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( F ` x ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) + ( ( A ` N ) x. ( x ^ N ) ) ) )
46 28 33 45 mvrraddd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) )
47 46 fveq2d 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) = ( abs ` sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) ) )
48 28 abscld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) ) e. RR )
49 27 abscld 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) e. RR )
50 20 49 fsumrecl 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) e. RR )
51 5 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> E e. RR+ )
52 51 rpred 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> E e. RR )
53 23 abscld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` x ) e. RR )
54 53 30 reexpcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ N ) e. RR )
55 52 54 remulcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( E x. ( ( abs ` x ) ^ N ) ) e. RR )
56 20 27 fsumabs 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) ) <_ sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) )
57 14 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) e. RR )
58 4 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> N e. NN )
59 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
60 58 59 syl 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( N - 1 ) e. NN0 )
61 53 60 reexpcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ ( N - 1 ) ) e. RR )
62 57 61 remulcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) e. RR )
63 13 adantlr 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( A ` k ) ) e. RR )
64 61 adantr 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( abs ` x ) ^ ( N - 1 ) ) e. RR )
65 63 64 remulcld 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) e. RR )
66 22 25 absmuld 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. NN0 ) -> ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) = ( ( abs ` ( A ` k ) ) x. ( abs ` ( x ^ k ) ) ) )
67 10 66 sylan2 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) = ( ( abs ` ( A ` k ) ) x. ( abs ` ( x ^ k ) ) ) )
68 10 25 sylan2 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( x ^ k ) e. CC )
69 68 abscld 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( x ^ k ) ) e. RR )
70 10 22 sylan2 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A ` k ) e. CC )
71 70 absge0d 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> 0 <_ ( abs ` ( A ` k ) ) )
72 absexp 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( abs ` ( x ^ k ) ) = ( ( abs ` x ) ^ k ) )
73 23 10 72 syl2an 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( x ^ k ) ) = ( ( abs ` x ) ^ k ) )
74 53 adantr 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` x ) e. RR )
75 17 a1i 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 1 e. RR )
76 19 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> if ( 1 <_ T , T , 1 ) e. RR )
77 max1 
 |-  ( ( 1 e. RR /\ T e. RR ) -> 1 <_ if ( 1 <_ T , T , 1 ) )
78 17 16 77 sylancr 
 |-  ( ph -> 1 <_ if ( 1 <_ T , T , 1 ) )
79 78 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 1 <_ if ( 1 <_ T , T , 1 ) )
80 simprr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> if ( 1 <_ T , T , 1 ) < ( abs ` x ) )
81 75 76 53 79 80 lelttrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 1 < ( abs ` x ) )
82 75 53 81 ltled 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 1 <_ ( abs ` x ) )
83 82 adantr 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> 1 <_ ( abs ` x ) )
84 elfzuz3 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` k ) )
85 84 adantl 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` k ) )
86 74 83 85 leexp2ad 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( abs ` x ) ^ k ) <_ ( ( abs ` x ) ^ ( N - 1 ) ) )
87 73 86 eqbrtrd 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( x ^ k ) ) <_ ( ( abs ` x ) ^ ( N - 1 ) ) )
88 69 64 63 71 87 lemul2ad 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( abs ` ( A ` k ) ) x. ( abs ` ( x ^ k ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
89 67 88 eqbrtrd 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
90 20 49 65 89 fsumle 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) <_ sum_ k e. ( 0 ... ( N - 1 ) ) ( ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
91 61 recnd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ ( N - 1 ) ) e. CC )
92 63 recnd 
 |-  ( ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( abs ` ( A ` k ) ) e. CC )
93 20 91 92 fsummulc1 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
94 90 93 breqtrrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) <_ ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
95 16 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> T e. RR )
96 max2 
 |-  ( ( 1 e. RR /\ T e. RR ) -> T <_ if ( 1 <_ T , T , 1 ) )
97 17 16 96 sylancr 
 |-  ( ph -> T <_ if ( 1 <_ T , T , 1 ) )
98 97 adantr 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> T <_ if ( 1 <_ T , T , 1 ) )
99 95 76 53 98 80 lelttrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> T < ( abs ` x ) )
100 6 99 eqbrtrrid 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E ) < ( abs ` x ) )
101 57 53 51 ltdivmuld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E ) < ( abs ` x ) <-> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) < ( E x. ( abs ` x ) ) ) )
102 100 101 mpbid 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) < ( E x. ( abs ` x ) ) )
103 52 53 remulcld 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( E x. ( abs ` x ) ) e. RR )
104 60 nn0zd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( N - 1 ) e. ZZ )
105 0red 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 0 e. RR )
106 0lt1 
 |-  0 < 1
107 106 a1i 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 0 < 1 )
108 105 75 53 107 81 lttrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 0 < ( abs ` x ) )
109 expgt0 
 |-  ( ( ( abs ` x ) e. RR /\ ( N - 1 ) e. ZZ /\ 0 < ( abs ` x ) ) -> 0 < ( ( abs ` x ) ^ ( N - 1 ) ) )
110 53 104 108 109 syl3anc 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> 0 < ( ( abs ` x ) ^ ( N - 1 ) ) )
111 ltmul1 
 |-  ( ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) e. RR /\ ( E x. ( abs ` x ) ) e. RR /\ ( ( ( abs ` x ) ^ ( N - 1 ) ) e. RR /\ 0 < ( ( abs ` x ) ^ ( N - 1 ) ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) < ( E x. ( abs ` x ) ) <-> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) < ( ( E x. ( abs ` x ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) ) )
112 57 103 61 110 111 syl112anc 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) < ( E x. ( abs ` x ) ) <-> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) < ( ( E x. ( abs ` x ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) ) )
113 102 112 mpbid 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) < ( ( E x. ( abs ` x ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
114 53 recnd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` x ) e. CC )
115 expm1t 
 |-  ( ( ( abs ` x ) e. CC /\ N e. NN ) -> ( ( abs ` x ) ^ N ) = ( ( ( abs ` x ) ^ ( N - 1 ) ) x. ( abs ` x ) ) )
116 114 58 115 syl2anc 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ N ) = ( ( ( abs ` x ) ^ ( N - 1 ) ) x. ( abs ` x ) ) )
117 91 114 mulcomd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( ( abs ` x ) ^ ( N - 1 ) ) x. ( abs ` x ) ) = ( ( abs ` x ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
118 116 117 eqtrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ N ) = ( ( abs ` x ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
119 118 oveq2d 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( E x. ( ( abs ` x ) ^ N ) ) = ( E x. ( ( abs ` x ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) ) )
120 52 recnd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> E e. CC )
121 120 114 91 mulassd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( ( E x. ( abs ` x ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) = ( E x. ( ( abs ` x ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) ) )
122 119 121 eqtr4d 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( E x. ( ( abs ` x ) ^ N ) ) = ( ( E x. ( abs ` x ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) )
123 113 122 breqtrrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) x. ( ( abs ` x ) ^ ( N - 1 ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) )
124 50 62 55 94 123 lelttrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( ( A ` k ) x. ( x ^ k ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) )
125 48 50 55 56 124 lelttrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` sum_ k e. ( 0 ... ( N - 1 ) ) ( ( A ` k ) x. ( x ^ k ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) )
126 47 125 eqbrtrd 
 |-  ( ( ph /\ ( x e. CC /\ if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) )
127 126 expr 
 |-  ( ( ph /\ x e. CC ) -> ( if ( 1 <_ T , T , 1 ) < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )
128 127 ralrimiva 
 |-  ( ph -> A. x e. CC ( if ( 1 <_ T , T , 1 ) < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )
129 breq1 
 |-  ( r = if ( 1 <_ T , T , 1 ) -> ( r < ( abs ` x ) <-> if ( 1 <_ T , T , 1 ) < ( abs ` x ) ) )
130 129 rspceaimv 
 |-  ( ( if ( 1 <_ T , T , 1 ) e. RR /\ A. x e. CC ( if ( 1 <_ T , T , 1 ) < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) ) -> E. r e. RR A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )
131 19 128 130 syl2anc 
 |-  ( ph -> E. r e. RR A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )