let a be Nat; ( 1 < a implies not seq_a^ (a,1,0) is polynomially-bounded )
assume AS1:
1 < a
; not seq_a^ (a,1,0) is polynomially-bounded
assume
seq_a^ (a,1,0) is polynomially-bounded
; 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)
TLCPP2:
ex N, b being Nat st
for n being Nat st N <= n holds
2 to_power n <= b * (n to_power k)