let a be Real; for k being Nat ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds a * (x to_power k) <= (polynom c) . x
let k be Nat; ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds a * (x to_power k) <= (polynom c) . x
reconsider c = (Segm (k + 1)) --> (|.a.| + 1) as XFinSequence of REAL by AFINSQ_1:63, XREAL_0:def 1;
reconsider c = c as non empty positive-yielding XFinSequence of REAL ;
take
c
; for x being Nat holds a * (x to_power k) <= (polynom c) . x
for x being Nat holds a * (x to_power k) <= (polynom c) . x
proof
let x be
Nat;
a * (x to_power k) <= (polynom c) . x
set c2 =
c (#) (seq_a^ (x,1,0));
T0:
(polynom c) . x = Sum (c (#) (seq_a^ (x,1,0)))
by ASYMPT_2:def 2;
LN2:
k + 0 < k + 1
by XREAL_1:8;
T1:
dom (c (#) (seq_a^ (x,1,0))) =
(dom c) /\ (dom (seq_a^ (x,1,0)))
by VALUED_1:def 4
.=
(dom c) /\ NAT
by SEQ_1:1
.=
(Segm (k + 1)) /\ NAT
;
T3:
(c (#) (seq_a^ (x,1,0))) . k =
(c . k) * ((seq_a^ (x,1,0)) . k)
by VALUED_1:5
.=
(c . k) * (x to_power ((1 * k) + 0))
by ASYMPT_1:def 1
.=
(|.a.| + 1) * (x to_power k)
by FUNCOP_1:7, NAT_1:44, LN2
;
a < |.a.| + 1
by TCL001;
then T4:
a * (x to_power k) <= (|.a.| + 1) * (x to_power k)
by XREAL_1:64;
len (c (#) (seq_a^ (x,1,0))) = k + 1
by T1, XBOOLE_1:28;
then
Sum (c (#) (seq_a^ (x,1,0))) >= (|.a.| + 1) * (x to_power k)
by T3, AFINSQ_2:61, NAT_1:44, LN2;
hence
a * (x to_power k) <= (polynom c) . x
by T4, XXREAL_0:2, T0;
verum
end;
hence
for x being Nat holds a * (x to_power k) <= (polynom c) . x
; verum