let a be Nat; :: thesis: ( 1 < a implies not seq_a^ (a,1,0) is polynomially-bounded )

assume AS1: 1 < a ; :: thesis: not seq_a^ (a,1,0) is polynomially-bounded

assume seq_a^ (a,1,0) is polynomially-bounded ; :: thesis: contradiction

then consider k being Nat such that

CL1: seq_a^ (a,1,0) in Big_Oh (seq_n^ k) ;

reconsider f = seq_n^ k as eventually-positive Real_Sequence ;

reconsider t = seq_a^ (a,1,0) as eventually-nonnegative Real_Sequence by AS1;

( t in Big_Oh f & ( for n being Element of NAT st 1 <= n holds

0 < f . n ) ) by LC4, CL1;

then consider c being Real such that

LL1: ( c > 0 & ( for n being Element of NAT st n >= 1 holds

(seq_a^ (a,1,0)) . n <= c * ((seq_n^ k) . n) ) ) by ASYMPT_0:8;

TLCPP: for n being Nat st n >= 1 holds

2 to_power n <= c * (n to_power k)

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

assume AS1: 1 < a ; :: thesis: not seq_a^ (a,1,0) is polynomially-bounded

assume seq_a^ (a,1,0) is polynomially-bounded ; :: thesis: contradiction

then consider k being Nat such that

CL1: seq_a^ (a,1,0) in Big_Oh (seq_n^ k) ;

reconsider f = seq_n^ k as eventually-positive Real_Sequence ;

reconsider t = seq_a^ (a,1,0) as eventually-nonnegative Real_Sequence by AS1;

( t in Big_Oh f & ( for n being Element of NAT st 1 <= n holds

0 < f . n ) ) by LC4, CL1;

then consider c being Real such that

LL1: ( c > 0 & ( for n being Element of NAT st n >= 1 holds

(seq_a^ (a,1,0)) . n <= c * ((seq_n^ k) . n) ) ) by ASYMPT_0:8;

TLCPP: for n being Nat st n >= 1 holds

2 to_power n <= c * (n to_power k)

proof

TLCPP2:
ex N, b being Nat st
let n be Nat; :: thesis: ( n >= 1 implies 2 to_power n <= c * (n to_power k) )

ZZ: n in NAT by ORDINAL1:def 12;

assume AT1: n >= 1 ; :: thesis: 2 to_power n <= c * (n to_power k)

then (seq_a^ (a,1,0)) . n <= c * ((seq_n^ k) . n) by ZZ, LL1;

then a to_power ((1 * n) + 0) <= c * ((seq_n^ k) . n) by ASYMPT_1:def 1;

then TZ1: a to_power n <= c * (n to_power k) by ASYMPT_1:def 3, AT1;

1 + 1 <= a by AS1, INT_1:7;

then 2 to_power n <= a to_power n by LEMC01;

hence 2 to_power n <= c * (n to_power k) by XXREAL_0:2, TZ1; :: thesis: verum

end;ZZ: n in NAT by ORDINAL1:def 12;

assume AT1: n >= 1 ; :: thesis: 2 to_power n <= c * (n to_power k)

then (seq_a^ (a,1,0)) . n <= c * ((seq_n^ k) . n) by ZZ, LL1;

then a to_power ((1 * n) + 0) <= c * ((seq_n^ k) . n) by ASYMPT_1:def 1;

then TZ1: a to_power n <= c * (n to_power k) by ASYMPT_1:def 3, AT1;

1 + 1 <= a by AS1, INT_1:7;

then 2 to_power n <= a to_power n by LEMC01;

hence 2 to_power n <= c * (n to_power k) by XXREAL_0:2, TZ1; :: thesis: verum

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

proof

consider N being Nat such that

TLCPP3: for n being Nat st N <= n holds

2 to_power n <= c * (n to_power k) by TLCPP;

set b = [/c\];

TLCPP4: c <= [/c\] by INT_1:def 7;

then reconsider b = [/c\] as Element of NAT by INT_1:3, LL1;

take N ; :: thesis: ex b being Nat st

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

take b ; :: thesis: for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

2 to_power n <= b * (n to_power k) ; :: thesis: verum

end;TLCPP3: for n being Nat st N <= n holds

2 to_power n <= c * (n to_power k) by TLCPP;

set b = [/c\];

TLCPP4: c <= [/c\] by INT_1:def 7;

then reconsider b = [/c\] as Element of NAT by INT_1:3, LL1;

take N ; :: thesis: ex b being Nat st

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

take b ; :: thesis: for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k)

proof

hence
for n being Nat st N <= n holds
let n be Nat; :: thesis: ( N <= n implies 2 to_power n <= b * (n to_power k) )

assume N <= n ; :: thesis: 2 to_power n <= b * (n to_power k)

then TLCPP5: 2 to_power n <= c * (n to_power k) by TLCPP3;

c * (n to_power k) <= b * (n to_power k) by XREAL_1:64, TLCPP4;

hence 2 to_power n <= b * (n to_power k) by TLCPP5, XXREAL_0:2; :: thesis: verum

end;assume N <= n ; :: thesis: 2 to_power n <= b * (n to_power k)

then TLCPP5: 2 to_power n <= c * (n to_power k) by TLCPP3;

c * (n to_power k) <= b * (n to_power k) by XREAL_1:64, TLCPP4;

hence 2 to_power n <= b * (n to_power k) by TLCPP5, XXREAL_0:2; :: thesis: verum

2 to_power n <= b * (n to_power k) ; :: thesis: verum

per cases
( 1 < k or k <= 1 )
;

end;

suppose
k <= 1
; :: thesis: contradiction

then TLCPPAA:
k < 2
by XXREAL_0:2;

ex N, b being Nat st

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power 2)

end;ex N, b being Nat st

for n being Nat st N <= n holds

2 to_power n <= b * (n to_power 2)

proof

hence
contradiction
by N2POWINPOLY; :: thesis: verum
consider N, b being Nat such that

TLCPPA3: for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k) by TLCPP2;

reconsider M = N + 2 as Element of NAT ;

TLCPPAA1: N <= M by NAT_1:11;

take M ; :: thesis: ex b being Nat st

for n being Nat st M <= n holds

2 to_power n <= b * (n to_power 2)

take b ; :: thesis: for n being Nat st M <= n holds

2 to_power n <= b * (n to_power 2)

let n be Nat; :: thesis: ( M <= n implies 2 to_power n <= b * (n to_power 2) )

assume TLCPPAS: M <= n ; :: thesis: 2 to_power n <= b * (n to_power 2)

then N <= n by XXREAL_0:2, TLCPPAA1;

then TLCPPA4: 2 to_power n <= b * (n to_power k) by TLCPPA3;

2 <= N + 2 by NAT_1:11;

then 1 + 1 <= n by TLCPPAS, XXREAL_0:2;

then 1 < n by NAT_1:13;

then n to_power k <= n to_power 2 by POWER:39, TLCPPAA;

then b * (n to_power k) <= b * (n to_power 2) by XREAL_1:64;

hence 2 to_power n <= b * (n to_power 2) by TLCPPA4, XXREAL_0:2; :: thesis: verum

end;TLCPPA3: for n being Nat st N <= n holds

2 to_power n <= b * (n to_power k) by TLCPP2;

reconsider M = N + 2 as Element of NAT ;

TLCPPAA1: N <= M by NAT_1:11;

take M ; :: thesis: ex b being Nat st

for n being Nat st M <= n holds

2 to_power n <= b * (n to_power 2)

take b ; :: thesis: for n being Nat st M <= n holds

2 to_power n <= b * (n to_power 2)

let n be Nat; :: thesis: ( M <= n implies 2 to_power n <= b * (n to_power 2) )

assume TLCPPAS: M <= n ; :: thesis: 2 to_power n <= b * (n to_power 2)

then N <= n by XXREAL_0:2, TLCPPAA1;

then TLCPPA4: 2 to_power n <= b * (n to_power k) by TLCPPA3;

2 <= N + 2 by NAT_1:11;

then 1 + 1 <= n by TLCPPAS, XXREAL_0:2;

then 1 < n by NAT_1:13;

then n to_power k <= n to_power 2 by POWER:39, TLCPPAA;

then b * (n to_power k) <= b * (n to_power 2) by XREAL_1:64;

hence 2 to_power n <= b * (n to_power 2) by TLCPPA4, XXREAL_0:2; :: thesis: verum