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