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)

proof

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;

TLCPP2: ex N, b being Nat st
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)

proof

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;

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

end;

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

suppose 1 < k ; :: thesis: contradiction

hence contradiction by TLCPP2, N2POWINPOLY; :: thesis: verum

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)

proof

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;

hence contradiction by N2POWINPOLY; :: thesis: verum

end;

end;