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

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

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

end;

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)

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

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)

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

end;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

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;((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 end;

N1:
x * (x to_power k1) = x to_power k
proof
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