let a be Real; :: thesis: ( 0 < a implies for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume AS: 0 < a ; :: thesis: for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
let k be Nat; :: thesis: for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
let d be nonnegative-yielding XFinSequence of REAL ; :: thesis: ( len d = k implies ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume A1: len d = k ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
A2: for i being Nat st i in dom d holds
0 <= d . i

proof

let i be Nat; :: thesis: ( i in dom d implies 0 <= d . i )
assume i in dom d ; :: thesis: 0 <= d . i
then d . i in rng d by FUNCT_1:3;
hence 0 <= d . i by PARTFUN3:def 4; :: thesis: verum

end;

per cases ( k = 0 or k <> 0 ) ;

suppose P0: k = 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

set N = 0 ;
take 0 ; :: thesis: for x being Nat st 0 <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
let x be Nat; :: thesis: ( 0 <= x implies for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume 0 <= x ; :: thesis: for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
thus for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) by P0, A1; :: thesis: verum

end;

suppose K1P: k <> 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

then 0 <= k - 1 by XREAL_1:48, NAT_1:14;
then reconsider k1 = k - 1 as Nat by INT_1:3, ORDINAL1:def 12;
consider M being Real such that
Q1: ( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) ) by TLNEG42, A2;
set N = [/((M * k) / a)\] + 2;
MM1: (M * k) / a <= [/((M * k) / a)\] by INT_1:def 7;
Q20P: 0 <= (M * k) / a by AS, Q1;
then Q20: 1 + 0 < 2 + [/((M * k) / a)\] by XREAL_1:8, MM1;
[/((M * k) / a)\] + 2 in NAT by INT_1:3, MM1, Q20P;
then reconsider N = [/((M * k) / a)\] + 2 as Nat ;
([/((M * k) / a)\] + 1) + 0 < ([/((M * k) / a)\] + 1) + 1 by XREAL_1:8;
then (M * k) / a < N by XXREAL_0:2, INT_1:32;
then ((M * k) / a) * a <= N * a by AS, XREAL_1:64;
then Q2: ( M * k <= a * N & 1 < N ) by XCMPLX_1:87, AS, Q20;
take N ; :: thesis: for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
thus for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) :: thesis: verum

proof

let x be Nat; :: thesis: ( N <= x implies for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume Q3: N <= x ; :: thesis: for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
let i be Nat; :: thesis: ( i in dom d implies ((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume Q4: i in dom d ; :: thesis: ((d . i) * (x to_power i)) * k <= a * (x to_power k)
then (d . i) * k <= M * k by XREAL_1:64, Q1;
then Q5: ((d . i) * k) * (x to_power i) <= (M * k) * (x to_power i) by XREAL_1:64;
i in Segm k by Q4, A1;
then i < k1 + 1 by NAT_1:44;
then Y1: i <= k1 by NAT_1:13;
Y2: 1 < x by Q3, XXREAL_0:2, Q20;
X1: x to_power i <= x to_power k1

proof

per cases ( i = k1 or i <> k1 ) ;

suppose i = k1 ; :: thesis: x to_power i <= x to_power k1

hence x to_power i <= x to_power k1 ; :: thesis: verum

end;

suppose i <> k1 ; :: thesis: x to_power i <= x to_power k1

then i < k1 by Y1, XXREAL_0:1;
hence x to_power i <= x to_power k1 by Y2, POWER:39; :: thesis: verum

end;

end;

end;

N1: x * (x to_power k1) = x to_power k

proof

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: x * (x to_power k1) = x to_power k

hence x * (x to_power k1) = x to_power k by K1P, POWER:def 2; :: thesis: verum

end;

suppose XX1: x <> 0 ; :: thesis: x * (x to_power k1) = x to_power k

x = x to_power 1 by POWER:25;
hence x * (x to_power k1) = x to_power (1 + k1) by XX1, POWER:27
.= x to_power k ;
:: thesis: verum

end;

end;

end;

(M * k) * (x to_power i) <= (M * k) * (x to_power k1) by X1, XREAL_1:64, Q1;
then Q7: ((d . i) * k) * (x to_power i) <= (M * k) * (x to_power k1) by XXREAL_0:2, Q5;
(M * k) * (x to_power k1) <= (a * N) * (x to_power k1) by Q2, XREAL_1:64;
then Q8: ((d . i) * k) * (x to_power i) <= (a * N) * (x to_power k1) by XXREAL_0:2, Q7;
a * N <= a * x by XREAL_1:64, AS, Q3;
then (a * N) * (x to_power k1) <= (a * x) * (x to_power k1) by XREAL_1:64;
hence ((d . i) * (x to_power i)) * k <= a * (x to_power k) by XXREAL_0:2, Q8, N1; :: thesis: verum

end;

end;

end;