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