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 and
A2: b >= 2 and
A3: 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 } ;
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 A3, Th36;
then A4: ( t in Big_Oh f,{ (b |^ n) where n is Element of NAT : verum } & t in Big_Omega f,{ (b |^ n) where n is Element of NAT : verum } ) by XBOOLE_0:def 4;
then A5: t in Big_Oh f by A1, A2, Th38;
t in Big_Omega f by A1, A2, A4, Th39;
hence t in Big_Theta f by A5, XBOOLE_0:def 4; :: thesis: verum