Metamath Proof Explorer


Theorem ftalem5

Description: Lemma for fta : Main proof. We have already shifted the minimum found in ftalem3 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let K be the lowest term in the polynomial that is nonzero, and let T be a K -th root of -u F ( 0 ) / A ( K ) . Then an evaluation of F ( T X ) where X is a sufficiently small positive number yields F ( 0 ) for the first term and -u F ( 0 ) x. X ^ K for the K -th term, and all higher terms are bounded because X is small. Thus, abs ( F ( T X ) ) <_ abs ( F ( 0 ) ) ( 1 - X ^ K ) < abs ( F ( 0 ) ) , in contradiction to our choice of F ( 0 ) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014) (Revised by AV, 28-Sep-2020)

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 )
ftalem4.5
|- ( ph -> ( F ` 0 ) =/= 0 )
ftalem4.6
|- K = inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < )
ftalem4.7
|- T = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) )
ftalem4.8
|- U = ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )
ftalem4.9
|- X = if ( 1 <_ U , 1 , U )
Assertion ftalem5
|- ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )

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 ftalem4.5
 |-  ( ph -> ( F ` 0 ) =/= 0 )
6 ftalem4.6
 |-  K = inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < )
7 ftalem4.7
 |-  T = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) )
8 ftalem4.8
 |-  U = ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )
9 ftalem4.9
 |-  X = if ( 1 <_ U , 1 , U )
10 1 2 3 4 5 6 7 8 9 ftalem4
 |-  ( ph -> ( ( K e. NN /\ ( A ` K ) =/= 0 ) /\ ( T e. CC /\ U e. RR+ /\ X e. RR+ ) ) )
11 10 simprd
 |-  ( ph -> ( T e. CC /\ U e. RR+ /\ X e. RR+ ) )
12 11 simp1d
 |-  ( ph -> T e. CC )
13 11 simp3d
 |-  ( ph -> X e. RR+ )
14 13 rpred
 |-  ( ph -> X e. RR )
15 14 recnd
 |-  ( ph -> X e. CC )
16 12 15 mulcld
 |-  ( ph -> ( T x. X ) e. CC )
17 plyf
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
18 3 17 syl
 |-  ( ph -> F : CC --> CC )
19 18 16 ffvelrnd
 |-  ( ph -> ( F ` ( T x. X ) ) e. CC )
20 19 abscld
 |-  ( ph -> ( abs ` ( F ` ( T x. X ) ) ) e. RR )
21 0cn
 |-  0 e. CC
22 ffvelrn
 |-  ( ( F : CC --> CC /\ 0 e. CC ) -> ( F ` 0 ) e. CC )
23 18 21 22 sylancl
 |-  ( ph -> ( F ` 0 ) e. CC )
24 23 abscld
 |-  ( ph -> ( abs ` ( F ` 0 ) ) e. RR )
25 10 simpld
 |-  ( ph -> ( K e. NN /\ ( A ` K ) =/= 0 ) )
26 25 simpld
 |-  ( ph -> K e. NN )
27 26 nnnn0d
 |-  ( ph -> K e. NN0 )
28 14 27 reexpcld
 |-  ( ph -> ( X ^ K ) e. RR )
29 24 28 remulcld
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) e. RR )
30 24 29 resubcld
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) e. RR )
31 fzfid
 |-  ( ph -> ( ( K + 1 ) ... N ) e. Fin )
32 1 coef3
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
33 3 32 syl
 |-  ( ph -> A : NN0 --> CC )
34 peano2nn0
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
35 27 34 syl
 |-  ( ph -> ( K + 1 ) e. NN0 )
36 elfzuz
 |-  ( k e. ( ( K + 1 ) ... N ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
37 eluznn0
 |-  ( ( ( K + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN0 )
38 35 36 37 syl2an
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> k e. NN0 )
39 ffvelrn
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
40 33 38 39 syl2an2r
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( A ` k ) e. CC )
41 16 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( T x. X ) e. CC )
42 41 38 expcld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( T x. X ) ^ k ) e. CC )
43 40 42 mulcld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
44 31 43 fsumcl
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
45 44 abscld
 |-  ( ph -> ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) e. RR )
46 30 45 readdcld
 |-  ( ph -> ( ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) e. RR )
47 fzfid
 |-  ( ph -> ( 0 ... K ) e. Fin )
48 elfznn0
 |-  ( k e. ( 0 ... K ) -> k e. NN0 )
49 33 48 39 syl2an
 |-  ( ( ph /\ k e. ( 0 ... K ) ) -> ( A ` k ) e. CC )
50 expcl
 |-  ( ( ( T x. X ) e. CC /\ k e. NN0 ) -> ( ( T x. X ) ^ k ) e. CC )
51 16 48 50 syl2an
 |-  ( ( ph /\ k e. ( 0 ... K ) ) -> ( ( T x. X ) ^ k ) e. CC )
52 49 51 mulcld
 |-  ( ( ph /\ k e. ( 0 ... K ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
53 47 52 fsumcl
 |-  ( ph -> sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
54 53 44 abstrid
 |-  ( ph -> ( abs ` ( sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) <_ ( ( abs ` sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) )
55 1 2 coeid2
 |-  ( ( F e. ( Poly ` S ) /\ ( T x. X ) e. CC ) -> ( F ` ( T x. X ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) )
56 3 16 55 syl2anc
 |-  ( ph -> ( F ` ( T x. X ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) )
57 26 nnred
 |-  ( ph -> K e. RR )
58 57 ltp1d
 |-  ( ph -> K < ( K + 1 ) )
59 fzdisj
 |-  ( K < ( K + 1 ) -> ( ( 0 ... K ) i^i ( ( K + 1 ) ... N ) ) = (/) )
60 58 59 syl
 |-  ( ph -> ( ( 0 ... K ) i^i ( ( K + 1 ) ... N ) ) = (/) )
61 ssrab2
 |-  { n e. NN | ( A ` n ) =/= 0 } C_ NN
62 nnuz
 |-  NN = ( ZZ>= ` 1 )
63 61 62 sseqtri
 |-  { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 )
64 fveq2
 |-  ( n = N -> ( A ` n ) = ( A ` N ) )
65 64 neeq1d
 |-  ( n = N -> ( ( A ` n ) =/= 0 <-> ( A ` N ) =/= 0 ) )
66 4 nnne0d
 |-  ( ph -> N =/= 0 )
67 2 1 dgreq0
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
68 3 67 syl
 |-  ( ph -> ( F = 0p <-> ( A ` N ) = 0 ) )
69 fveq2
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
70 dgr0
 |-  ( deg ` 0p ) = 0
71 69 70 eqtrdi
 |-  ( F = 0p -> ( deg ` F ) = 0 )
72 2 71 syl5eq
 |-  ( F = 0p -> N = 0 )
73 68 72 syl6bir
 |-  ( ph -> ( ( A ` N ) = 0 -> N = 0 ) )
74 73 necon3d
 |-  ( ph -> ( N =/= 0 -> ( A ` N ) =/= 0 ) )
75 66 74 mpd
 |-  ( ph -> ( A ` N ) =/= 0 )
76 65 4 75 elrabd
 |-  ( ph -> N e. { n e. NN | ( A ` n ) =/= 0 } )
77 infssuzle
 |-  ( ( { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 ) /\ N e. { n e. NN | ( A ` n ) =/= 0 } ) -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) <_ N )
78 63 76 77 sylancr
 |-  ( ph -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) <_ N )
79 6 78 eqbrtrid
 |-  ( ph -> K <_ N )
80 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
81 27 80 eleqtrdi
 |-  ( ph -> K e. ( ZZ>= ` 0 ) )
82 4 nnzd
 |-  ( ph -> N e. ZZ )
83 elfz5
 |-  ( ( K e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
84 81 82 83 syl2anc
 |-  ( ph -> ( K e. ( 0 ... N ) <-> K <_ N ) )
85 79 84 mpbird
 |-  ( ph -> K e. ( 0 ... N ) )
86 fzsplit
 |-  ( K e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... K ) u. ( ( K + 1 ) ... N ) ) )
87 85 86 syl
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... K ) u. ( ( K + 1 ) ... N ) ) )
88 fzfid
 |-  ( ph -> ( 0 ... N ) e. Fin )
89 elfznn0
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
90 33 89 39 syl2an
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
91 16 89 50 syl2an
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( T x. X ) ^ k ) e. CC )
92 90 91 mulcld
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
93 60 87 88 92 fsumsplit
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) )
94 56 93 eqtrd
 |-  ( ph -> ( F ` ( T x. X ) ) = ( sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) )
95 94 fveq2d
 |-  ( ph -> ( abs ` ( F ` ( T x. X ) ) ) = ( abs ` ( sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) )
96 1 coefv0
 |-  ( F e. ( Poly ` S ) -> ( F ` 0 ) = ( A ` 0 ) )
97 3 96 syl
 |-  ( ph -> ( F ` 0 ) = ( A ` 0 ) )
98 97 eqcomd
 |-  ( ph -> ( A ` 0 ) = ( F ` 0 ) )
99 16 exp0d
 |-  ( ph -> ( ( T x. X ) ^ 0 ) = 1 )
100 98 99 oveq12d
 |-  ( ph -> ( ( A ` 0 ) x. ( ( T x. X ) ^ 0 ) ) = ( ( F ` 0 ) x. 1 ) )
101 23 mulid1d
 |-  ( ph -> ( ( F ` 0 ) x. 1 ) = ( F ` 0 ) )
102 100 101 eqtrd
 |-  ( ph -> ( ( A ` 0 ) x. ( ( T x. X ) ^ 0 ) ) = ( F ` 0 ) )
103 1e0p1
 |-  1 = ( 0 + 1 )
104 103 oveq1i
 |-  ( 1 ... K ) = ( ( 0 + 1 ) ... K )
105 104 sumeq1i
 |-  sum_ k e. ( 1 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = sum_ k e. ( ( 0 + 1 ) ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) )
106 26 62 eleqtrdi
 |-  ( ph -> K e. ( ZZ>= ` 1 ) )
107 elfznn
 |-  ( k e. ( 1 ... K ) -> k e. NN )
108 107 nnnn0d
 |-  ( k e. ( 1 ... K ) -> k e. NN0 )
109 33 108 39 syl2an
 |-  ( ( ph /\ k e. ( 1 ... K ) ) -> ( A ` k ) e. CC )
110 16 108 50 syl2an
 |-  ( ( ph /\ k e. ( 1 ... K ) ) -> ( ( T x. X ) ^ k ) e. CC )
111 109 110 mulcld
 |-  ( ( ph /\ k e. ( 1 ... K ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) e. CC )
112 fveq2
 |-  ( k = K -> ( A ` k ) = ( A ` K ) )
113 oveq2
 |-  ( k = K -> ( ( T x. X ) ^ k ) = ( ( T x. X ) ^ K ) )
114 112 113 oveq12d
 |-  ( k = K -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) )
115 106 111 114 fsumm1
 |-  ( ph -> sum_ k e. ( 1 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( sum_ k e. ( 1 ... ( K - 1 ) ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) ) )
116 105 115 eqtr3id
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( sum_ k e. ( 1 ... ( K - 1 ) ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) ) )
117 elfznn
 |-  ( k e. ( 1 ... ( K - 1 ) ) -> k e. NN )
118 117 adantl
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> k e. NN )
119 118 nnred
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> k e. RR )
120 57 adantr
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> K e. RR )
121 peano2rem
 |-  ( K e. RR -> ( K - 1 ) e. RR )
122 120 121 syl
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
123 elfzle2
 |-  ( k e. ( 1 ... ( K - 1 ) ) -> k <_ ( K - 1 ) )
124 123 adantl
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> k <_ ( K - 1 ) )
125 120 ltm1d
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) < K )
126 119 122 120 124 125 lelttrd
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> k < K )
127 119 120 ltnled
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( k < K <-> -. K <_ k ) )
128 126 127 mpbid
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> -. K <_ k )
129 infssuzle
 |-  ( ( { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 ) /\ k e. { n e. NN | ( A ` n ) =/= 0 } ) -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) <_ k )
130 6 129 eqbrtrid
 |-  ( ( { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 ) /\ k e. { n e. NN | ( A ` n ) =/= 0 } ) -> K <_ k )
131 63 130 mpan
 |-  ( k e. { n e. NN | ( A ` n ) =/= 0 } -> K <_ k )
132 128 131 nsyl
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> -. k e. { n e. NN | ( A ` n ) =/= 0 } )
133 fveq2
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
134 133 neeq1d
 |-  ( n = k -> ( ( A ` n ) =/= 0 <-> ( A ` k ) =/= 0 ) )
135 134 elrab3
 |-  ( k e. NN -> ( k e. { n e. NN | ( A ` n ) =/= 0 } <-> ( A ` k ) =/= 0 ) )
136 118 135 syl
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( k e. { n e. NN | ( A ` n ) =/= 0 } <-> ( A ` k ) =/= 0 ) )
137 136 necon2bbid
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( ( A ` k ) = 0 <-> -. k e. { n e. NN | ( A ` n ) =/= 0 } ) )
138 132 137 mpbird
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( A ` k ) = 0 )
139 138 oveq1d
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( 0 x. ( ( T x. X ) ^ k ) ) )
140 117 nnnn0d
 |-  ( k e. ( 1 ... ( K - 1 ) ) -> k e. NN0 )
141 16 140 50 syl2an
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( ( T x. X ) ^ k ) e. CC )
142 141 mul02d
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( 0 x. ( ( T x. X ) ^ k ) ) = 0 )
143 139 142 eqtrd
 |-  ( ( ph /\ k e. ( 1 ... ( K - 1 ) ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = 0 )
144 143 sumeq2dv
 |-  ( ph -> sum_ k e. ( 1 ... ( K - 1 ) ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = sum_ k e. ( 1 ... ( K - 1 ) ) 0 )
145 fzfi
 |-  ( 1 ... ( K - 1 ) ) e. Fin
146 145 olci
 |-  ( ( 1 ... ( K - 1 ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( K - 1 ) ) e. Fin )
147 sumz
 |-  ( ( ( 1 ... ( K - 1 ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( K - 1 ) ) e. Fin ) -> sum_ k e. ( 1 ... ( K - 1 ) ) 0 = 0 )
148 146 147 ax-mp
 |-  sum_ k e. ( 1 ... ( K - 1 ) ) 0 = 0
149 144 148 eqtrdi
 |-  ( ph -> sum_ k e. ( 1 ... ( K - 1 ) ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = 0 )
150 12 15 27 mulexpd
 |-  ( ph -> ( ( T x. X ) ^ K ) = ( ( T ^ K ) x. ( X ^ K ) ) )
151 150 oveq2d
 |-  ( ph -> ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) = ( ( A ` K ) x. ( ( T ^ K ) x. ( X ^ K ) ) ) )
152 33 27 ffvelrnd
 |-  ( ph -> ( A ` K ) e. CC )
153 12 27 expcld
 |-  ( ph -> ( T ^ K ) e. CC )
154 28 recnd
 |-  ( ph -> ( X ^ K ) e. CC )
155 152 153 154 mulassd
 |-  ( ph -> ( ( ( A ` K ) x. ( T ^ K ) ) x. ( X ^ K ) ) = ( ( A ` K ) x. ( ( T ^ K ) x. ( X ^ K ) ) ) )
156 151 155 eqtr4d
 |-  ( ph -> ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) = ( ( ( A ` K ) x. ( T ^ K ) ) x. ( X ^ K ) ) )
157 7 oveq1i
 |-  ( T ^ K ) = ( ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) ) ^ K )
158 57 recnd
 |-  ( ph -> K e. CC )
159 26 nnne0d
 |-  ( ph -> K =/= 0 )
160 158 159 recid2d
 |-  ( ph -> ( ( 1 / K ) x. K ) = 1 )
161 160 oveq2d
 |-  ( ph -> ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( ( 1 / K ) x. K ) ) = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c 1 ) )
162 25 simprd
 |-  ( ph -> ( A ` K ) =/= 0 )
163 23 152 162 divcld
 |-  ( ph -> ( ( F ` 0 ) / ( A ` K ) ) e. CC )
164 163 negcld
 |-  ( ph -> -u ( ( F ` 0 ) / ( A ` K ) ) e. CC )
165 26 nnrecred
 |-  ( ph -> ( 1 / K ) e. RR )
166 165 recnd
 |-  ( ph -> ( 1 / K ) e. CC )
167 164 166 27 cxpmul2d
 |-  ( ph -> ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( ( 1 / K ) x. K ) ) = ( ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) ) ^ K ) )
168 164 cxp1d
 |-  ( ph -> ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c 1 ) = -u ( ( F ` 0 ) / ( A ` K ) ) )
169 161 167 168 3eqtr3d
 |-  ( ph -> ( ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) ) ^ K ) = -u ( ( F ` 0 ) / ( A ` K ) ) )
170 157 169 syl5eq
 |-  ( ph -> ( T ^ K ) = -u ( ( F ` 0 ) / ( A ` K ) ) )
171 170 oveq2d
 |-  ( ph -> ( ( A ` K ) x. ( T ^ K ) ) = ( ( A ` K ) x. -u ( ( F ` 0 ) / ( A ` K ) ) ) )
172 152 163 mulneg2d
 |-  ( ph -> ( ( A ` K ) x. -u ( ( F ` 0 ) / ( A ` K ) ) ) = -u ( ( A ` K ) x. ( ( F ` 0 ) / ( A ` K ) ) ) )
173 23 152 162 divcan2d
 |-  ( ph -> ( ( A ` K ) x. ( ( F ` 0 ) / ( A ` K ) ) ) = ( F ` 0 ) )
174 173 negeqd
 |-  ( ph -> -u ( ( A ` K ) x. ( ( F ` 0 ) / ( A ` K ) ) ) = -u ( F ` 0 ) )
175 171 172 174 3eqtrd
 |-  ( ph -> ( ( A ` K ) x. ( T ^ K ) ) = -u ( F ` 0 ) )
176 175 oveq1d
 |-  ( ph -> ( ( ( A ` K ) x. ( T ^ K ) ) x. ( X ^ K ) ) = ( -u ( F ` 0 ) x. ( X ^ K ) ) )
177 23 154 mulneg1d
 |-  ( ph -> ( -u ( F ` 0 ) x. ( X ^ K ) ) = -u ( ( F ` 0 ) x. ( X ^ K ) ) )
178 156 176 177 3eqtrd
 |-  ( ph -> ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) = -u ( ( F ` 0 ) x. ( X ^ K ) ) )
179 149 178 oveq12d
 |-  ( ph -> ( sum_ k e. ( 1 ... ( K - 1 ) ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) + ( ( A ` K ) x. ( ( T x. X ) ^ K ) ) ) = ( 0 + -u ( ( F ` 0 ) x. ( X ^ K ) ) ) )
180 23 154 mulcld
 |-  ( ph -> ( ( F ` 0 ) x. ( X ^ K ) ) e. CC )
181 180 negcld
 |-  ( ph -> -u ( ( F ` 0 ) x. ( X ^ K ) ) e. CC )
182 181 addid2d
 |-  ( ph -> ( 0 + -u ( ( F ` 0 ) x. ( X ^ K ) ) ) = -u ( ( F ` 0 ) x. ( X ^ K ) ) )
183 116 179 182 3eqtrd
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = -u ( ( F ` 0 ) x. ( X ^ K ) ) )
184 102 183 oveq12d
 |-  ( ph -> ( ( ( A ` 0 ) x. ( ( T x. X ) ^ 0 ) ) + sum_ k e. ( ( 0 + 1 ) ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) = ( ( F ` 0 ) + -u ( ( F ` 0 ) x. ( X ^ K ) ) ) )
185 fveq2
 |-  ( k = 0 -> ( A ` k ) = ( A ` 0 ) )
186 oveq2
 |-  ( k = 0 -> ( ( T x. X ) ^ k ) = ( ( T x. X ) ^ 0 ) )
187 185 186 oveq12d
 |-  ( k = 0 -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( A ` 0 ) x. ( ( T x. X ) ^ 0 ) ) )
188 81 52 187 fsum1p
 |-  ( ph -> sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( ( A ` 0 ) x. ( ( T x. X ) ^ 0 ) ) + sum_ k e. ( ( 0 + 1 ) ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) )
189 101 oveq1d
 |-  ( ph -> ( ( ( F ` 0 ) x. 1 ) - ( ( F ` 0 ) x. ( X ^ K ) ) ) = ( ( F ` 0 ) - ( ( F ` 0 ) x. ( X ^ K ) ) ) )
190 1cnd
 |-  ( ph -> 1 e. CC )
191 23 190 154 subdid
 |-  ( ph -> ( ( F ` 0 ) x. ( 1 - ( X ^ K ) ) ) = ( ( ( F ` 0 ) x. 1 ) - ( ( F ` 0 ) x. ( X ^ K ) ) ) )
192 23 180 negsubd
 |-  ( ph -> ( ( F ` 0 ) + -u ( ( F ` 0 ) x. ( X ^ K ) ) ) = ( ( F ` 0 ) - ( ( F ` 0 ) x. ( X ^ K ) ) ) )
193 189 191 192 3eqtr4d
 |-  ( ph -> ( ( F ` 0 ) x. ( 1 - ( X ^ K ) ) ) = ( ( F ` 0 ) + -u ( ( F ` 0 ) x. ( X ^ K ) ) ) )
194 184 188 193 3eqtr4d
 |-  ( ph -> sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( F ` 0 ) x. ( 1 - ( X ^ K ) ) ) )
195 194 fveq2d
 |-  ( ph -> ( abs ` sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) = ( abs ` ( ( F ` 0 ) x. ( 1 - ( X ^ K ) ) ) ) )
196 1re
 |-  1 e. RR
197 resubcl
 |-  ( ( 1 e. RR /\ ( X ^ K ) e. RR ) -> ( 1 - ( X ^ K ) ) e. RR )
198 196 28 197 sylancr
 |-  ( ph -> ( 1 - ( X ^ K ) ) e. RR )
199 198 recnd
 |-  ( ph -> ( 1 - ( X ^ K ) ) e. CC )
200 23 199 absmuld
 |-  ( ph -> ( abs ` ( ( F ` 0 ) x. ( 1 - ( X ^ K ) ) ) ) = ( ( abs ` ( F ` 0 ) ) x. ( abs ` ( 1 - ( X ^ K ) ) ) ) )
201 13 rpge0d
 |-  ( ph -> 0 <_ X )
202 11 simp2d
 |-  ( ph -> U e. RR+ )
203 202 rpred
 |-  ( ph -> U e. RR )
204 min1
 |-  ( ( 1 e. RR /\ U e. RR ) -> if ( 1 <_ U , 1 , U ) <_ 1 )
205 196 203 204 sylancr
 |-  ( ph -> if ( 1 <_ U , 1 , U ) <_ 1 )
206 9 205 eqbrtrid
 |-  ( ph -> X <_ 1 )
207 exple1
 |-  ( ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) /\ K e. NN0 ) -> ( X ^ K ) <_ 1 )
208 14 201 206 27 207 syl31anc
 |-  ( ph -> ( X ^ K ) <_ 1 )
209 subge0
 |-  ( ( 1 e. RR /\ ( X ^ K ) e. RR ) -> ( 0 <_ ( 1 - ( X ^ K ) ) <-> ( X ^ K ) <_ 1 ) )
210 196 28 209 sylancr
 |-  ( ph -> ( 0 <_ ( 1 - ( X ^ K ) ) <-> ( X ^ K ) <_ 1 ) )
211 208 210 mpbird
 |-  ( ph -> 0 <_ ( 1 - ( X ^ K ) ) )
212 198 211 absidd
 |-  ( ph -> ( abs ` ( 1 - ( X ^ K ) ) ) = ( 1 - ( X ^ K ) ) )
213 212 oveq2d
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) x. ( abs ` ( 1 - ( X ^ K ) ) ) ) = ( ( abs ` ( F ` 0 ) ) x. ( 1 - ( X ^ K ) ) ) )
214 24 recnd
 |-  ( ph -> ( abs ` ( F ` 0 ) ) e. CC )
215 214 190 154 subdid
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) x. ( 1 - ( X ^ K ) ) ) = ( ( ( abs ` ( F ` 0 ) ) x. 1 ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) )
216 214 mulid1d
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) x. 1 ) = ( abs ` ( F ` 0 ) ) )
217 216 oveq1d
 |-  ( ph -> ( ( ( abs ` ( F ` 0 ) ) x. 1 ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) = ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) )
218 213 215 217 3eqtrd
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) x. ( abs ` ( 1 - ( X ^ K ) ) ) ) = ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) )
219 195 200 218 3eqtrrd
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) = ( abs ` sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) )
220 219 oveq1d
 |-  ( ph -> ( ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) = ( ( abs ` sum_ k e. ( 0 ... K ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) )
221 54 95 220 3brtr4d
 |-  ( ph -> ( abs ` ( F ` ( T x. X ) ) ) <_ ( ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) )
222 43 abscld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) e. RR )
223 31 222 fsumrecl
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) e. RR )
224 31 43 fsumabs
 |-  ( ph -> ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) <_ sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) )
225 expcl
 |-  ( ( T e. CC /\ k e. NN0 ) -> ( T ^ k ) e. CC )
226 12 38 225 syl2an2r
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( T ^ k ) e. CC )
227 40 226 mulcld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( A ` k ) x. ( T ^ k ) ) e. CC )
228 227 abscld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. RR )
229 31 228 fsumrecl
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. RR )
230 14 35 reexpcld
 |-  ( ph -> ( X ^ ( K + 1 ) ) e. RR )
231 229 230 remulcld
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) e. RR )
232 230 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( X ^ ( K + 1 ) ) e. RR )
233 228 232 remulcld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) e. RR )
234 12 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> T e. CC )
235 15 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> X e. CC )
236 234 235 38 mulexpd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( T x. X ) ^ k ) = ( ( T ^ k ) x. ( X ^ k ) ) )
237 236 oveq2d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( A ` k ) x. ( ( T ^ k ) x. ( X ^ k ) ) ) )
238 14 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> X e. RR )
239 238 38 reexpcld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( X ^ k ) e. RR )
240 239 recnd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( X ^ k ) e. CC )
241 40 226 240 mulassd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( ( A ` k ) x. ( T ^ k ) ) x. ( X ^ k ) ) = ( ( A ` k ) x. ( ( T ^ k ) x. ( X ^ k ) ) ) )
242 237 241 eqtr4d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) = ( ( ( A ` k ) x. ( T ^ k ) ) x. ( X ^ k ) ) )
243 242 fveq2d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) = ( abs ` ( ( ( A ` k ) x. ( T ^ k ) ) x. ( X ^ k ) ) ) )
244 227 240 absmuld
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( ( A ` k ) x. ( T ^ k ) ) x. ( X ^ k ) ) ) = ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( abs ` ( X ^ k ) ) ) )
245 elfzelz
 |-  ( k e. ( ( K + 1 ) ... N ) -> k e. ZZ )
246 rpexpcl
 |-  ( ( X e. RR+ /\ k e. ZZ ) -> ( X ^ k ) e. RR+ )
247 13 245 246 syl2an
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( X ^ k ) e. RR+ )
248 247 rpge0d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( X ^ k ) )
249 239 248 absidd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( X ^ k ) ) = ( X ^ k ) )
250 249 oveq2d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( abs ` ( X ^ k ) ) ) = ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ k ) ) )
251 243 244 250 3eqtrd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) = ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ k ) ) )
252 227 absge0d
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) )
253 35 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( K + 1 ) e. NN0 )
254 36 adantl
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
255 201 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> 0 <_ X )
256 206 adantr
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> X <_ 1 )
257 238 253 254 255 256 leexp2rd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( X ^ k ) <_ ( X ^ ( K + 1 ) ) )
258 239 232 228 252 257 lemul2ad
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ k ) ) <_ ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) )
259 251 258 eqbrtrd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) <_ ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) )
260 31 222 233 259 fsumle
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) <_ sum_ k e. ( ( K + 1 ) ... N ) ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) )
261 230 recnd
 |-  ( ph -> ( X ^ ( K + 1 ) ) e. CC )
262 228 recnd
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. CC )
263 31 261 262 fsummulc1
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) = sum_ k e. ( ( K + 1 ) ... N ) ( ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) )
264 260 263 breqtrrd
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) <_ ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) )
265 15 27 expp1d
 |-  ( ph -> ( X ^ ( K + 1 ) ) = ( ( X ^ K ) x. X ) )
266 154 15 mulcomd
 |-  ( ph -> ( ( X ^ K ) x. X ) = ( X x. ( X ^ K ) ) )
267 265 266 eqtrd
 |-  ( ph -> ( X ^ ( K + 1 ) ) = ( X x. ( X ^ K ) ) )
268 267 oveq2d
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) = ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X x. ( X ^ K ) ) ) )
269 229 recnd
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. CC )
270 269 15 154 mulassd
 |-  ( ph -> ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) x. ( X ^ K ) ) = ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X x. ( X ^ K ) ) ) )
271 268 270 eqtr4d
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) = ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) x. ( X ^ K ) ) )
272 229 14 remulcld
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) e. RR )
273 nnssz
 |-  NN C_ ZZ
274 61 273 sstri
 |-  { n e. NN | ( A ` n ) =/= 0 } C_ ZZ
275 76 ne0d
 |-  ( ph -> { n e. NN | ( A ` n ) =/= 0 } =/= (/) )
276 infssuzcl
 |-  ( ( { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 ) /\ { n e. NN | ( A ` n ) =/= 0 } =/= (/) ) -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) e. { n e. NN | ( A ` n ) =/= 0 } )
277 63 275 276 sylancr
 |-  ( ph -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) e. { n e. NN | ( A ` n ) =/= 0 } )
278 6 277 eqeltrid
 |-  ( ph -> K e. { n e. NN | ( A ` n ) =/= 0 } )
279 274 278 sselid
 |-  ( ph -> K e. ZZ )
280 13 279 rpexpcld
 |-  ( ph -> ( X ^ K ) e. RR+ )
281 peano2re
 |-  ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. RR -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) e. RR )
282 229 281 syl
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) e. RR )
283 282 14 remulcld
 |-  ( ph -> ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) x. X ) e. RR )
284 229 ltp1d
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) < ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )
285 229 282 13 284 ltmul1dd
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) < ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) x. X ) )
286 min2
 |-  ( ( 1 e. RR /\ U e. RR ) -> if ( 1 <_ U , 1 , U ) <_ U )
287 196 203 286 sylancr
 |-  ( ph -> if ( 1 <_ U , 1 , U ) <_ U )
288 9 287 eqbrtrid
 |-  ( ph -> X <_ U )
289 288 8 breqtrdi
 |-  ( ph -> X <_ ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) ) )
290 0red
 |-  ( ph -> 0 e. RR )
291 31 228 252 fsumge0
 |-  ( ph -> 0 <_ sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) )
292 290 229 282 291 284 lelttrd
 |-  ( ph -> 0 < ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )
293 lemuldiv2
 |-  ( ( X e. RR /\ ( abs ` ( F ` 0 ) ) e. RR /\ ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) e. RR /\ 0 < ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) ) ) -> ( ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) x. X ) <_ ( abs ` ( F ` 0 ) ) <-> X <_ ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) ) ) )
294 14 24 282 292 293 syl112anc
 |-  ( ph -> ( ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) x. X ) <_ ( abs ` ( F ` 0 ) ) <-> X <_ ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) ) ) )
295 289 294 mpbird
 |-  ( ph -> ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) x. X ) <_ ( abs ` ( F ` 0 ) ) )
296 272 283 24 285 295 ltletrd
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) < ( abs ` ( F ` 0 ) ) )
297 272 24 280 296 ltmul1dd
 |-  ( ph -> ( ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. X ) x. ( X ^ K ) ) < ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) )
298 271 297 eqbrtrd
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) x. ( X ^ ( K + 1 ) ) ) < ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) )
299 223 231 29 264 298 lelttrd
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) < ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) )
300 45 223 29 224 299 lelttrd
 |-  ( ph -> ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) < ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) )
301 45 29 24 300 ltsub2dd
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) < ( ( abs ` ( F ` 0 ) ) - ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) )
302 30 45 24 ltaddsubd
 |-  ( ph -> ( ( ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) < ( abs ` ( F ` 0 ) ) <-> ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) < ( ( abs ` ( F ` 0 ) ) - ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) ) )
303 301 302 mpbird
 |-  ( ph -> ( ( ( abs ` ( F ` 0 ) ) - ( ( abs ` ( F ` 0 ) ) x. ( X ^ K ) ) ) + ( abs ` sum_ k e. ( ( K + 1 ) ... N ) ( ( A ` k ) x. ( ( T x. X ) ^ k ) ) ) ) < ( abs ` ( F ` 0 ) ) )
304 20 46 24 221 303 lelttrd
 |-  ( ph -> ( abs ` ( F ` ( T x. X ) ) ) < ( abs ` ( F ` 0 ) ) )
305 2fveq3
 |-  ( x = ( T x. X ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( T x. X ) ) ) )
306 305 breq1d
 |-  ( x = ( T x. X ) -> ( ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) <-> ( abs ` ( F ` ( T x. X ) ) ) < ( abs ` ( F ` 0 ) ) ) )
307 306 rspcev
 |-  ( ( ( T x. X ) e. CC /\ ( abs ` ( F ` ( T x. X ) ) ) < ( abs ` ( F ` 0 ) ) ) -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )
308 16 304 307 syl2anc
 |-  ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )