let f be eventually-nonnegative Real_Sequence; :: thesis: for t being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds
t in Big_Theta f
let t be eventually-nonnegative eventually-nondecreasing Real_Sequence; :: thesis: for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds
t in Big_Theta f
let b be Element of NAT ; :: thesis: ( f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) implies t in Big_Theta f )
assume that
A1: ( f is smooth & b >= 2 ) and
A2: t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) ; :: thesis: t in Big_Theta f
set X = { (b |^ n) where n is Element of NAT : verum } ;
A3: t in (Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } )) /\ (Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } )) by A2, Th36;
then t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) by XBOOLE_0:def 4;
then A4: t in Big_Omega f by A1, Th39;
t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) by A3, XBOOLE_0:def 4;
then t in Big_Oh f by A1, Th38;
hence t in Big_Theta f by A4, XBOOLE_0:def 4; :: thesis: verum