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:9;
A3: ((159 / 100) - (log (2,3))) / 2 <> 0 by A1;

A4: now :: thesis: for p being Real st p > 0 holds
ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n) - 0).| < p

A5: ((159 / 100) - (log (2,3))) * (1 / 2) < ((159 / 100) - (log (2,3))) * 1 by A2, XREAL_1:68;
let p be Real; :: thesis: ( p > 0 implies ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n) - 0).| < p )
assume A6: p > 0 ; :: thesis: ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n) - 0).| < p
reconsider p1 = p as Real ;
A7: (1 / p1) to_power (1 / (((159 / 100) - (log (2,3))) / 2)) > 0 by A6, POWER:34;
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;
max ([/((1 / p1) to_power (1 / (((159 / 100) - (log (2,3))) / 2)))\],2) in NAT by A10, A9, INT_1:3;
then reconsider N1 = max ([/((1 / p1) to_power (1 / (((159 / 100) - (log (2,3))) / 2)))\],2) as Nat ;
take N1 = N1; :: thesis: for n being Nat st n >= N1 holds
|.((((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N1 implies |.((((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n) - 0).| < p )
A12: n in NAT by ORDINAL1:def 12;
A13: ((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n = ((seq_n^ (log (2,3))) . n) / ((seq_n^ (159 / 100)) . n) by Lm4;
assume A14: n >= N1 ; :: thesis: |.((((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, A12;
then A15: ((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n = (n to_power (log (2,3))) / (n to_power (159 / 100)) by A10, A14, A13, Def3, A12
.= n to_power ((log (2,3)) - (159 / 100)) by A10, A14, POWER:29
.= 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 7;
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 A14, 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:33;
then n to_power (((159 / 100) - (log (2,3))) / 2) >= (1 / p) to_power 1 by A3, XCMPLX_1:87;
then n to_power (((159 / 100) - (log (2,3))) / 2) >= 1 / p1 by POWER:25;
then 1 / (n to_power (((159 / 100) - (log (2,3))) / 2)) <= 1 / (p ") by A6, XREAL_1:85;
then A16: n to_power (- (((159 / 100) - (log (2,3))) / 2)) <= p by A10, A14, POWER:28;
n > 1 by A11, A14, XXREAL_0:2;
then A17: n to_power (((159 / 100) - (log (2,3))) / 2) < n to_power ((159 / 100) - (log (2,3))) by A5, POWER:39;
n to_power (((159 / 100) - (log (2,3))) / 2) > 0 by A10, A14, POWER:34;
then 1 / (n to_power (((159 / 100) - (log (2,3))) / 2)) > 1 / (n to_power ((159 / 100) - (log (2,3)))) by A17, XREAL_1:88;
then n to_power (- (((159 / 100) - (log (2,3))) / 2)) > 1 / (n to_power ((159 / 100) - (log (2,3)))) by A10, A14, POWER:28;
then ((seq_n^ (log (2,3))) /" (seq_n^ (159 / 100))) . n < n to_power (- (((159 / 100) - (log (2,3))) / 2)) by A10, A14, A15, POWER:28;
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 A10, A14, A15, POWER:34;
hence |.((((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 A4, SEQ_2:def 7;
hence seq_n^ (log (2,3)) in Big_Oh (seq_n^ (159 / 100)) by A19, 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)) )
A21: not seq_n^ (159 / 100) in Big_Oh (seq_n^ (log (2,3))) by A19, A20, 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 A21, ASYMPT_0:19;
hence not seq_n^ (log (2,3)) in Big_Theta (seq_n^ (159 / 100)) by XBOOLE_0:def 4; :: thesis: verum