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 () ;
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 ;
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 * (() . 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 * (() . n) by ;
then a to_power ((1 * n) + 0) <= c * (() . n) by ASYMPT_1:def 1;
then TZ1: a to_power n <= c * (n to_power k) by ;
1 + 1 <= a by ;
then 2 to_power n <= a to_power n by LEMC01;
hence 2 to_power n <= c * (n to_power k) by ; :: 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 ;
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 ;
hence 2 to_power n <= b * (n to_power k) by ; :: 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
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 ;
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 ;
then 1 < n by NAT_1:13;
then n to_power k <= n to_power 2 by ;
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 ; :: thesis: verum
end;
hence contradiction by N2POWINPOLY; :: thesis: verum
end;
end;