assume A1: log 2,3 < 159 / 100 ; :: thesis: ( seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100)) )
set f = seq_n^ (log 2,3);
set g = seq_n^ (159 / 100);
set h = (seq_n^ (log 2,3)) /" (seq_n^ (159 / 100));
set c = (159 / 100) - (log 2,3);
A2: (log 2,3) - (log 2,3) < (159 / 100) - (log 2,3) by A1, XREAL_1:11;
then A3: ((159 / 100) - (log 2,3)) * (2 " ) > 0 * (2 " ) by XREAL_1:70;
A4: ((159 / 100) - (log 2,3)) / 2 <> 0 by A1;

A5: now

let p be real number ; :: thesis: ( p > 0 implies ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p )
assume A6: p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p
reconsider p1 = p as Real by XREAL_0:def 1;
set N1 = max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2;
A7: ( max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 >= [/((1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\] & max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 >= 2 ) by XXREAL_0:25;
then A8: max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 > 1 by XXREAL_0:2;
max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 is Integer by XXREAL_0:16;
then reconsider N1 = max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 as Element of NAT by A7, INT_1:16;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p )
assume A9: n >= N1 ; :: thesis: abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p
p " > 0 by A6;
then A10: 1 / p > 0 ;
[/((1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\] >= (1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) by INT_1:def 5;
then A11: N1 >= (1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) by A7, XXREAL_0:2;
A12: (1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) > 0 by A10, POWER:39;
A13: n > 1 by A8, A9, XXREAL_0:2;
A14: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n = ((seq_n^ (log 2,3)) . n) / ((seq_n^ (159 / 100)) . n) by Lm4;
(seq_n^ (log 2,3)) . n = n to_power (log 2,3) by A7, A9, Def3;
then A15: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n = (n to_power (log 2,3)) / (n to_power (159 / 100)) by A7, A9, A14, Def3
.= n to_power ((log 2,3) - (159 / 100)) by A7, A9, POWER:34
.= n to_power (- ((159 / 100) - (log 2,3))) ;
n >= (1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) by A9, A11, XXREAL_0:2;
then n to_power (((159 / 100) - (log 2,3)) / 2) >= ((1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2))) to_power (((159 / 100) - (log 2,3)) / 2) by A3, A12, Lm6;
then n to_power (((159 / 100) - (log 2,3)) / 2) >= (1 / p1) to_power ((1 / (((159 / 100) - (log 2,3)) / 2)) * (((159 / 100) - (log 2,3)) / 2)) by A10, POWER:38;
then n to_power (((159 / 100) - (log 2,3)) / 2) >= (1 / p) to_power 1 by A4, XCMPLX_1:88;
then n to_power (((159 / 100) - (log 2,3)) / 2) >= 1 / p1 by POWER:30;
then 1 / (n to_power (((159 / 100) - (log 2,3)) / 2)) <= 1 / (1 / p) by A10, XREAL_1:87;
then 1 / (n to_power (((159 / 100) - (log 2,3)) / 2)) <= 1 / (p " ) ;
then 1 / (n to_power (((159 / 100) - (log 2,3)) / 2)) <= p ;
then A16: n to_power (- (((159 / 100) - (log 2,3)) / 2)) <= p by A7, A9, POWER:33;
A17: n to_power (((159 / 100) - (log 2,3)) / 2) > 0 by A7, A9, POWER:39;
((159 / 100) - (log 2,3)) * (1 / 2) < ((159 / 100) - (log 2,3)) * 1 by A2, XREAL_1:70;
then n to_power (((159 / 100) - (log 2,3)) / 2) < n to_power ((159 / 100) - (log 2,3)) by A13, POWER:44;
then 1 / (n to_power (((159 / 100) - (log 2,3)) / 2)) > 1 / (n to_power ((159 / 100) - (log 2,3))) by A17, XREAL_1:90;
then n to_power (- (((159 / 100) - (log 2,3)) / 2)) > 1 / (n to_power ((159 / 100) - (log 2,3))) by A7, A9, POWER:33;
then ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n < n to_power (- (((159 / 100) - (log 2,3)) / 2)) by A7, A9, A15, POWER:33;
then A18: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n < p by A16, XXREAL_0:2;
((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n > 0 by A7, A9, A15, POWER:39;
hence abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p by A18, ABSVALUE:def 1; :: thesis: verum

end;

then A19: (seq_n^ (log 2,3)) /" (seq_n^ (159 / 100)) is convergent by SEQ_2:def 6;
then A20: lim ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) = 0 by A5, SEQ_2:def 7;
then A21: ( seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) & not seq_n^ (159 / 100) in Big_Oh (seq_n^ (log 2,3)) ) by A19, ASYMPT_0:16;
then A22: ( seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) ) by ASYMPT_0:19;
thus seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) by A19, A20, ASYMPT_0:16; :: thesis: ( not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100)) )
thus not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) by A21, ASYMPT_0:19; :: thesis: not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100))
thus not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100)) by A22, XBOOLE_0:def 4; :: thesis: verum