set c = (159 / 100) - (log 2,3);
set g = seq_n^ (159 / 100);
set f = seq_n^ (log 2,3);
set h = (seq_n^ (log 2,3)) /" (seq_n^ (159 / 100));
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)) )
then A2: (log 2,3) - (log 2,3) < (159 / 100) - (log 2,3) by XREAL_1:11;
A3: ((159 / 100) - (log 2,3)) / 2 <> 0 by A1;

A4: now

A5: ((159 / 100) - (log 2,3)) * (1 / 2) < ((159 / 100) - (log 2,3)) * 1 by A2, XREAL_1:70;
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;
A7: (1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) > 0 by A6, POWER:39;
set N1 = max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2;
A8: max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 >= [/((1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\] by XXREAL_0:25;
A9: max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 is Integer by XXREAL_0:16;
A10: max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 >= 2 by XXREAL_0:25;
then A11: max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 > 1 by XXREAL_0:2;
reconsider N1 = max [/((1 / p1) to_power (1 / (((159 / 100) - (log 2,3)) / 2)))\],2 as Element of NAT by A10, A9, 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 )
A12: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n = ((seq_n^ (log 2,3)) . n) / ((seq_n^ (159 / 100)) . n) by Lm4;
assume A13: n >= N1 ; :: thesis: abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p
then (seq_n^ (log 2,3)) . n = n to_power (log 2,3) by A10, Def3;
then A14: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n = (n to_power (log 2,3)) / (n to_power (159 / 100)) by A10, A13, A12, Def3
.= n to_power ((log 2,3) - (159 / 100)) by A10, A13, POWER:34
.= n to_power (- ((159 / 100) - (log 2,3))) ;
[/((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 N1 >= (1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) by A8, XXREAL_0:2;
then n >= (1 / p) to_power (1 / (((159 / 100) - (log 2,3)) / 2)) by A13, 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 A2, A7, 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 A6, POWER:38;
then n to_power (((159 / 100) - (log 2,3)) / 2) >= (1 / p) to_power 1 by A3, 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 / (p " ) by A6, XREAL_1:87;
then A15: n to_power (- (((159 / 100) - (log 2,3)) / 2)) <= p by A10, A13, POWER:33;
n > 1 by A11, A13, XXREAL_0:2;
then A16: n to_power (((159 / 100) - (log 2,3)) / 2) < n to_power ((159 / 100) - (log 2,3)) by A5, POWER:44;
n to_power (((159 / 100) - (log 2,3)) / 2) > 0 by A10, A13, POWER:39;
then 1 / (n to_power (((159 / 100) - (log 2,3)) / 2)) > 1 / (n to_power ((159 / 100) - (log 2,3))) by A16, XREAL_1:90;
then n to_power (- (((159 / 100) - (log 2,3)) / 2)) > 1 / (n to_power ((159 / 100) - (log 2,3))) by A10, A13, POWER:33;
then ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n < n to_power (- (((159 / 100) - (log 2,3)) / 2)) by A10, A13, A14, POWER:33;
then A17: ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n < p by A15, XXREAL_0:2;
((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n > 0 by A10, A13, A14, POWER:39;
hence abs ((((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) . n) - 0 ) < p by A17, ABSVALUE:def 1; :: thesis: verum

end;

then A18: (seq_n^ (log 2,3)) /" (seq_n^ (159 / 100)) is convergent by SEQ_2:def 6;
then A19: lim ((seq_n^ (log 2,3)) /" (seq_n^ (159 / 100))) = 0 by A4, SEQ_2:def 7;
hence seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) by A18, 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)) )
A20: not seq_n^ (159 / 100) in Big_Oh (seq_n^ (log 2,3)) by A18, A19, ASYMPT_0:16;
hence not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) by ASYMPT_0:19; :: thesis: not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100))
not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) by A20, ASYMPT_0:19;
hence not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100)) by XBOOLE_0:def 4; :: thesis: verum