let k be Nat; :: thesis: for d being XFinSequence of REAL st len d = k + 1 & 0 < d . k holds
seq_p d is eventually-nonnegative
let d be XFinSequence of REAL ; :: thesis: ( len d = k + 1 & 0 < d . k implies seq_p d is eventually-nonnegative )
assume AS: ( len d = k + 1 & 0 < d . k ) ; :: thesis: seq_p d is eventually-nonnegative
then consider a being Real, d1 being XFinSequence of REAL , y being Real_Sequence such that
P1: ( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) ) by LMXFIN4;
consider N being Nat such that
P20: for i being Nat st N <= i holds
|.((seq_p d1) . i).| <= y . i by P1, TLNEG35, AS;
for i being Nat st N <= i holds
0 <= (seq_p d) . i
proof
let i be Nat; :: thesis: ( N <= i implies 0 <= (seq_p d) . i )
assume N <= i ; :: thesis: 0 <= (seq_p d) . i
then P32: 0 <= (y . i) - |.((seq_p d1) . i).| by XREAL_1:48, P20;
- ((seq_p d1) . i) <= - (- |.((seq_p d1) . i).|) by XREAL_1:24, ABSVALUE:4;
then (y . i) - |.((seq_p d1) . i).| <= (y . i) - (- ((seq_p d1) . i)) by XREAL_1:13;
then (y . i) - |.((seq_p d1) . i).| <= ((seq_p d1) . i) + (y . i) ;
hence 0 <= (seq_p d) . i by P1, SEQ_1:7, P32; :: thesis: verum
end;
hence seq_p d is eventually-nonnegative ; :: thesis: verum