set f = seq_n^ 8;
let e be Real; :: thesis: ( 0 < e & e < 1 implies ex s being eventually-positive Real_Sequence st
( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s ) )
assume that
A1: 0 < e and
A2: e < 1 ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )
consider N being Element of NAT such that
A3: for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by A1, A2, Lm25;
set g = seq_a^ ((1 + e),1,0);
set h = (seq_n^ 8) /" (seq_a^ ((1 + e),1,0));
reconsider g = seq_a^ ((1 + e),1,0) as eventually-positive Real_Sequence by A1;
take g ; :: thesis: ( g = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )
thus g = seq_a^ ((1 + e),1,0) ; :: thesis: ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )

A4: 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^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p )
assume A5: p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p
reconsider p1 = p as Real by XREAL_0:def 1;
A6: (1 / p1) to_power (1 / 8) > 0 by A5, POWER:34;
set N1 = max (N,(max ([/((1 / p1) to_power (1 / 8))\],2)));
A7: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= N by XXREAL_0:25;
A8: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer

proof

per cases ( max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = N or max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = max ([/((1 / p) to_power (1 / 8))\],2) ) by XXREAL_0:16;

suppose max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = N ; :: thesis: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer

hence max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer ; :: thesis: verum

end;

suppose max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = max ([/((1 / p) to_power (1 / 8))\],2) ; :: thesis: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer

hence max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer by XXREAL_0:16; :: thesis: verum

end;

end;

end;

A9: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= max ([/((1 / p) to_power (1 / 8))\],2) by XXREAL_0:25;
max ([/((1 / p) to_power (1 / 8))\],2) >= [/((1 / p) to_power (1 / 8))\] by XXREAL_0:25;
then A10: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= [/((1 / p) to_power (1 / 8))\] by A9, XXREAL_0:2;
reconsider N1 = max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) as Element of NAT by A7, A8, INT_1:3;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs ((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p )
assume A11: n >= N1 ; :: thesis: abs ((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p
then n >= N by A7, XXREAL_0:2;
then (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by A3;
then A12: 2 to_power ((n * (log (2,(1 + e)))) - (8 * (log (2,n)))) > 2 to_power (8 * (log (2,n))) by POWER:39;
A13: max ([/((1 / p) to_power (1 / 8))\],2) >= 2 by XXREAL_0:25;
A14: g . n = (1 + e) to_power ((1 * n) + 0) by Def1;
((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n = ((seq_n^ 8) . n) / (g . n) by Lm4;
then A15: ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n = (n to_power 8) / ((1 + e) to_power n) by A9, A13, A11, A14, Def3
.= (2 to_power (8 * (log (2,n)))) / ((1 + e) to_power n) by A9, A13, A11, Lm3
.= (2 to_power (8 * (log (2,n)))) / (2 to_power (n * (log (2,(1 + e))))) by A1, Lm3
.= 2 to_power ((8 * (log (2,n))) - (n * (log (2,(1 + e))))) by POWER:29
.= 2 to_power (- ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) ;
[/((1 / p) to_power (1 / 8))\] >= (1 / p) to_power (1 / 8) by INT_1:def 7;
then N1 >= (1 / p) to_power (1 / 8) by A10, XXREAL_0:2;
then n >= (1 / p) to_power (1 / 8) by A11, XXREAL_0:2;
then n to_power 8 >= ((1 / p) to_power (1 / 8)) to_power 8 by A6, Lm6;
then n to_power 8 >= (1 / p1) to_power ((1 / 8) * 8) by A5, POWER:33;
then n to_power 8 >= 1 / p1 by POWER:25;
then 1 / (n to_power 8) <= 1 / (p ") by A5, XREAL_1:85;
then 1 / (2 to_power (8 * (log (2,n)))) <= p by A9, A13, A11, Lm3;
then A16: 2 to_power (- (8 * (log (2,n)))) <= p by POWER:28;
2 to_power (8 * (log (2,n))) > 0 by POWER:34;
then 1 / (2 to_power ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) < 1 / (2 to_power (8 * (log (2,n)))) by A12, XREAL_1:88;
then 2 to_power (- ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) < 1 / (2 to_power (8 * (log (2,n)))) by POWER:28;
then ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n < 2 to_power (- (8 * (log (2,n)))) by A15, POWER:28;
then A17: ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n < p by A16, XXREAL_0:2;
((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n > 0 by A15, POWER:34;
hence abs ((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0) < p by A17, ABSVALUE:def 1; :: thesis: verum

end;

then A18: (seq_n^ 8) /" (seq_a^ ((1 + e),1,0)) is convergent by SEQ_2:def 6;
then A19: lim ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) = 0 by A4, SEQ_2:def 7;
then not g in Big_Oh (seq_n^ 8) by A18, ASYMPT_0:16;
then A20: not seq_n^ 8 in Big_Omega g by ASYMPT_0:19;
seq_n^ 8 in Big_Oh g by A18, A19, ASYMPT_0:16;
hence ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g ) by A20, Th4; :: thesis: verum