set g = seq_n^ 8;
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log (2,n)) ) implies ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) ) )
assume A1: for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log (2,n)) ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) )
A2: f is eventually-positive

proof

take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 2 <= b₁ or not f . b₁ <= 0 )
let n be Nat; :: thesis: ( not 2 <= n or not f . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: n >= 2 ; :: thesis: not f . n <= 0
then log (2,n) >= log (2,2) by PRE_FF:10;
then A5: log (2,n) >= 1 by POWER:52;
n > 1 by A4, XXREAL_0:2;
then A6: f . n = (n to_power 2) / (log (2,n)) by A1, A3
.= (n to_power 2) * ((log (2,n)) ") ;
n to_power 2 > 0 by A4, POWER:34;
then (n to_power 2) * ((log (2,n)) ") > (n to_power 2) * 0 by A5, XREAL_1:68;
hence not f . n <= 0 by A6; :: thesis: verum

end;

set h = f /" (seq_n^ 8);
reconsider f = f as eventually-positive Real_Sequence by A2;

A7: now :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < p

A8: log (2,3) > log (2,2) by POWER:57;
let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < p )
assume A9: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < p
A10: [/(p to_power (- (1 / 6)))\] >= p to_power (- (1 / 6)) by INT_1:def 7;
reconsider p1 = p as Real ;
set N = max (3,[/(p1 to_power (- (1 / 6)))\]);
A11: max (3,[/(p1 to_power (- (1 / 6)))\]) >= 3 by XXREAL_0:25;
A12: max (3,[/(p1 to_power (- (1 / 6)))\]) is Integer by XXREAL_0:16;
A13: max (3,[/(p1 to_power (- (1 / 6)))\]) >= [/(p to_power (- (1 / 6)))\] by XXREAL_0:25;
max (3,[/(p1 to_power (- (1 / 6)))\]) in NAT by A11, A12, INT_1:3;
then reconsider N = max (3,[/(p1 to_power (- (1 / 6)))\]) as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.(((f /" (seq_n^ 8)) . n) - 0).| < p )
A14: n in NAT by ORDINAL1:def 12;
assume A15: n >= N ; :: thesis: |.(((f /" (seq_n^ 8)) . n) - 0).| < p
then A16: n >= 3 by A11, XXREAL_0:2;
then A17: n > 1 by XXREAL_0:2;
A18: (f /" (seq_n^ 8)) . n = (f . n) / ((seq_n^ 8) . n) by Lm4
.= ((n to_power 2) / (log (2,n))) / ((seq_n^ 8) . n) by A1, A17, A14
.= ((n to_power 2) / (log (2,n))) / (n to_power 8) by A11, A15, Def3, A14
.= ((n to_power 2) * ((log (2,n)) ")) / (n to_power 8)
.= (((log (2,n)) ") * (n to_power 2)) * ((n to_power 8) ")
.= ((log (2,n)) ") * ((n to_power 2) * ((n to_power 8) "))
.= ((log (2,n)) ") * ((n to_power 2) / (n to_power 8))
.= ((log (2,n)) ") * (n to_power (2 - 8)) by A11, A15, POWER:29
.= ((log (2,n)) ") * (n to_power (- 6))
.= ((log (2,n)) ") * (1 / (n to_power 6)) by A11, A15, POWER:28
.= (1 / (n to_power 6)) * (1 / (log (2,n)))
.= 1 / ((n to_power 6) * (log (2,n))) by XCMPLX_1:102 ;
n >= [/(p to_power (- (1 / 6)))\] by A13, A15, XXREAL_0:2;
then A19: n >= p to_power (- (1 / 6)) by A10, XXREAL_0:2;
p1 to_power (- (1 / 6)) > 0 by A9, POWER:34;
then n to_power 6 >= (p to_power (- (1 / 6))) to_power 6 by A19, Lm6;
then A20: n to_power 6 >= p1 to_power ((- (1 / 6)) * 6) by A9, POWER:33;
p1 to_power (- 1) > 0 by A9, POWER:34;
then 1 / (n to_power 6) <= 1 / (p to_power (- 1)) by A20, XREAL_1:85;
then 1 / (n to_power 6) <= 1 / (1 / (p1 to_power 1)) by A9, POWER:28;
then A21: 1 / (n to_power 6) <= p by POWER:25;
log (2,n) >= log (2,3) by A16, PRE_FF:10;
then log (2,n) > log (2,2) by A8, XXREAL_0:2;
then A22: log (2,n) > 1 by POWER:52;
A23: n to_power 6 > 0 by A11, A15, POWER:34;
then (n to_power 6) * 1 < (n to_power 6) * (log (2,n)) by A22, XREAL_1:68;
then (f /" (seq_n^ 8)) . n < 1 / (n to_power 6) by A23, A18, XREAL_1:88;
then (f /" (seq_n^ 8)) . n < p by A21, XXREAL_0:2;
hence |.(((f /" (seq_n^ 8)) . n) - 0).| < p by A22, A18, ABSVALUE:def 1; :: thesis: verum

end;

then A24: f /" (seq_n^ 8) is convergent by SEQ_2:def 6;
then A25: lim (f /" (seq_n^ 8)) = 0 by A7, SEQ_2:def 7;
then not seq_n^ 8 in Big_Oh f by A24, ASYMPT_0:16;
then A26: not f in Big_Omega (seq_n^ 8) by ASYMPT_0:19;
take f ; :: thesis: ( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) )
f in Big_Oh (seq_n^ 8) by A24, A25, ASYMPT_0:16;
hence ( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) ) by A26, Th4; :: thesis: verum