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 ) ) ) )