let f be Real_Sequence; :: thesis: for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds
f in Big_Theta (seq_n^ (k + 1))
let k be Element of NAT ; :: thesis: ( ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) implies f in Big_Theta (seq_n^ (k + 1)) )
assume A1: for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ; :: thesis: f in Big_Theta (seq_n^ (k + 1))
set g = seq_n^ (k + 1);
A2: f is Element of Funcs (NAT,REAL) by FUNCT_2:8;

A3: now :: thesis: for n being Element of NAT st n >= 1 holds
( ((2 to_power (k + 1)) ") * ((seq_n^ (k + 1)) . n) <= f . n & f . n >= 0 )

set p = seq_n^ k;
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( ((2 to_power (k + 1)) ") * ((seq_n^ (k + 1)) . n) <= f . n & f . n >= 0 ) )
set n1 = [/(n / 2)\];
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = (n / 2) to_power k ) )

proof

defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = (n / 2) to_power k ) );
A4: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[x,y]

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

suppose x = zz ; :: thesis: ex y being Element of REAL st S₁[x,y]

hence ex y being Element of REAL st S₁[x,y] ; :: thesis: verum

end;

suppose A5: x > 0 ; :: thesis: ex y being Element of REAL st S₁[x,y]

reconsider y = (n / 2) to_power k as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A5; :: thesis: verum

end;

end;

end;

consider h being sequence of REAL such that
A6: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A4);
take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = (n / 2) to_power k ) )
thus h . 0 = 0 by A6; :: thesis: for m being Element of NAT st m > 0 holds
h . m = (n / 2) to_power k
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = (n / 2) to_power k )
thus ( n > 0 implies h . n = (n / 2) to_power k ) by A6; :: thesis: verum

end;

then consider q being Real_Sequence such that
A7: q . 0 = 0 and
A8: for m being Element of NAT st m > 0 holds
q . m = (n / 2) to_power k ;
A9: [/(n / 2)\] >= n / 2 by INT_1:def 7;
then reconsider n1 = [/(n / 2)\] as Element of NAT by INT_1:3;
set n2 = n1 - 1;
assume A10: n >= 1 ; :: thesis: ( ((2 to_power (k + 1)) ") * ((seq_n^ (k + 1)) . n) <= f . n & f . n >= 0 )
then A11: n * (2 ") > 0 * (2 ") by XREAL_1:68;
then A12: (n / 2) to_power k > 0 by POWER:34;

now :: thesis: not n1 - 1 < 0

assume n1 - 1 < 0 ; :: thesis: contradiction
then (n1 - 1) + 1 <= (- 1) + 1 ;
hence contradiction by A11, INT_1:def 7; :: thesis: verum

end;

then reconsider n2 = n1 - 1 as Element of NAT by INT_1:3;

A13: now :: thesis: not n - n2 < n / 2

[/(n / 2)\] < (n / 2) + 1 by INT_1:def 7;
then n2 < n / 2 by XREAL_1:19;
then A14: (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:6;
assume n - n2 < n / 2 ; :: thesis: contradiction
hence contradiction by A14, XREAL_1:19; :: thesis: verum

end;

Sum (q,n,n2) = (n - n2) * ((n / 2) to_power k) by A7, A8, Lm18;
then Sum (q,n,n2) >= (n / 2) * ((n / 2) to_power k) by A13, A12, XREAL_1:64;
then Sum (q,n,n2) >= ((n / 2) to_power 1) * ((n / 2) to_power k) by POWER:25;
then Sum (q,n,n2) >= (n / 2) to_power (k + 1) by A11, POWER:27;
then A15: Sum (q,n,n2) >= (n to_power (k + 1)) / (2 to_power (k + 1)) by A10, POWER:31;
A16: f . n = Sum ((seq_n^ k),n) by A1;

A17: now :: thesis: for m being Element of NAT st m <= n holds
(seq_n^ k) . m >= 0

let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b₁ >= 0 )
assume m <= n ; :: thesis: (seq_n^ k) . b₁ >= 0

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: (seq_n^ k) . b₁ >= 0

hence (seq_n^ k) . m >= 0 by Def3; :: thesis: verum

end;

suppose m > 0 ; :: thesis: (seq_n^ k) . b₁ >= 0

then (seq_n^ k) . m = m to_power k by Def3;
hence (seq_n^ k) . m >= 0 ; :: thesis: verum

end;

end;

end;

now :: thesis: for m being Element of NAT st m <= n2 holds
(seq_n^ k) . m >= 0

let m be Element of NAT ; :: thesis: ( m <= n2 implies (seq_n^ k) . m >= 0 )
n1 <= n1 + 1 by NAT_1:11;
then A18: n2 <= n1 by XREAL_1:20;
A19: n1 <= n by Lm17;
assume m <= n2 ; :: thesis: (seq_n^ k) . m >= 0
then m <= n1 by A18, XXREAL_0:2;
then m <= n by A19, XXREAL_0:2;
hence (seq_n^ k) . m >= 0 by A17; :: thesis: verum

end;

then Sum ((seq_n^ k),n2) >= 0 by Lm12;
then A20: (Sum ((seq_n^ k),n)) + (Sum ((seq_n^ k),n2)) >= (Sum ((seq_n^ k),n)) + 0 by XREAL_1:7;
A21: for N0 being Element of NAT st n1 <= N0 & N0 <= n holds
q . N0 <= (seq_n^ k) . N0

proof

let N0 be Element of NAT ; :: thesis: ( n1 <= N0 & N0 <= n implies q . N0 <= (seq_n^ k) . N0 )
assume that
A22: n1 <= N0 and
N0 <= n ; :: thesis: q . N0 <= (seq_n^ k) . N0
A23: N0 >= n / 2 by A9, A22, XXREAL_0:2;
A24: (seq_n^ k) . N0 = N0 to_power k by A11, A9, A22, Def3;
q . N0 = (n / 2) to_power k by A8, A11, A9, A22;
hence q . N0 <= (seq_n^ k) . N0 by A11, A24, A23, Lm6; :: thesis: verum

end;

n >= n2 + 1 by Lm17;
then Sum ((seq_n^ k),n,n2) >= Sum (q,n,n2) by A21, Lm16;
then A25: Sum ((seq_n^ k),n,n2) >= (n to_power (k + 1)) * ((2 to_power (k + 1)) ") by A15, XXREAL_0:2;
Sum ((seq_n^ k),n,n2) = (Sum ((seq_n^ k),n)) - (Sum ((seq_n^ k),n2)) by SERIES_1:def 6;
then A26: Sum ((seq_n^ k),n) >= Sum ((seq_n^ k),n,n2) by A20, XREAL_1:20;
(seq_n^ (k + 1)) . n = n to_power (k + 1) by A10, Def3;
hence ((2 to_power (k + 1)) ") * ((seq_n^ (k + 1)) . n) <= f . n by A16, A26, A25, XXREAL_0:2; :: thesis: f . n >= 0
Sum ((seq_n^ k),n) >= 0 by A17, Lm12;
hence f . n >= 0 by A1; :: thesis: verum

end;

now :: thesis: for n being Element of NAT st n >= 1 holds
( f . n <= 1 * ((seq_n^ (k + 1)) . n) & f . n >= 0 )

set p = seq_n^ k;
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( f . n <= 1 * ((seq_n^ (k + 1)) . n) & f . n >= 0 ) )
assume A27: n >= 1 ; :: thesis: ( f . n <= 1 * ((seq_n^ (k + 1)) . n) & f . n >= 0 )
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = n to_power k ) )

proof

defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = n to_power k ) );
A28: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[x,y]

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

suppose x = zz ; :: thesis: ex y being Element of REAL st S₁[x,y]

hence ex y being Element of REAL st S₁[x,y] ; :: thesis: verum

end;

suppose A29: x > 0 ; :: thesis: ex y being Element of REAL st S₁[x,y]

reconsider y = n to_power k as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A29; :: thesis: verum

end;

end;

end;

consider h being sequence of REAL such that
A30: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A28);
take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = n to_power k ) )
thus h . 0 = 0 by A30; :: thesis: for m being Element of NAT st m > 0 holds
h . m = n to_power k
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = n to_power k )
thus ( n > 0 implies h . n = n to_power k ) by A30; :: thesis: verum

end;

then consider q being Real_Sequence such that
A31: q . 0 = 0 and
A32: for m being Element of NAT st m > 0 holds
q . m = n to_power k ;

now :: thesis: for m being Element of NAT st m <= n holds
(seq_n^ k) . m <= q . m

let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b₁ <= q . b₁ )
assume A33: m <= n ; :: thesis: (seq_n^ k) . b₁ <= q . b₁

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: (seq_n^ k) . b₁ <= q . b₁

hence (seq_n^ k) . m <= q . m by A31, Def3; :: thesis: verum

end;

suppose A34: m > 0 ; :: thesis: (seq_n^ k) . b₁ <= q . b₁

then A35: q . m = n to_power k by A32;
(seq_n^ k) . m = m to_power k by A34, Def3;
hence (seq_n^ k) . m <= q . m by A33, A34, A35, Lm6; :: thesis: verum

end;

end;

end;

then A36: Sum ((seq_n^ k),n) <= Sum (q,n) by Lm13;
Sum (q,n) = (n to_power k) * n by A31, A32, Lm14
.= (n to_power k) * (n to_power 1) by POWER:25
.= n to_power (k + 1) by A27, POWER:27
.= (seq_n^ (k + 1)) . n by A27, Def3 ;
hence f . n <= 1 * ((seq_n^ (k + 1)) . n) by A1, A36; :: thesis: f . n >= 0

A37: now :: thesis: for m being Element of NAT st m <= n holds
(seq_n^ k) . m >= 0

let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b₁ >= 0 )
assume m <= n ; :: thesis: (seq_n^ k) . b₁ >= 0

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: (seq_n^ k) . b₁ >= 0

hence (seq_n^ k) . m >= 0 by Def3; :: thesis: verum

end;

suppose m > 0 ; :: thesis: (seq_n^ k) . b₁ >= 0

then (seq_n^ k) . m = m to_power k by Def3;
hence (seq_n^ k) . m >= 0 ; :: thesis: verum

end;

end;

end;

f . n = Sum ((seq_n^ k),n) by A1;
hence f . n >= 0 by A37, Lm12; :: thesis: verum

end;

then A38: f in Big_Oh (seq_n^ (k + 1)) by A2;
2 to_power (k + 1) > 0 by POWER:34;
then f in Big_Omega (seq_n^ (k + 1)) by A2, A3;
hence f in Big_Theta (seq_n^ (k + 1)) by A38, XBOOLE_0:def 4; :: thesis: verum