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 )
set f = seq_n^ 8;
set g = seq_a^ (1 + e),1,0 ;
set h = (seq_n^ 8) /" (seq_a^ (1 + e),1,0 );
A3: 1 + e > 0 + 0 by A1;
then reconsider g = seq_a^ (1 + e),1,0 as eventually-positive Real_Sequence ;
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 )
consider N being Element of NAT such that
A4: 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, Lm31;

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^ 8) /" (seq_a^ (1 + e),1,0 )) . 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^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p
reconsider p1 = p as Real by XREAL_0:def 1;
set N1 = max N,(max [/((1 / p1) to_power (1 / 8))\],2);
A7: ( max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= N & max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= max [/((1 / p) to_power (1 / 8))\],2 ) by XXREAL_0:25;
A8: ( max [/((1 / p) to_power (1 / 8))\],2 >= [/((1 / p) to_power (1 / 8))\] & max [/((1 / p) to_power (1 / 8))\],2 >= 2 ) by XXREAL_0:25;
then A9: ( max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= [/((1 / p) to_power (1 / 8))\] & max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= 2 ) by A7, XXREAL_0:2;
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;

then reconsider N1 = max N,(max [/((1 / p1) to_power (1 / 8))\],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^ 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 A10: n >= N1 ; :: thesis: abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p
p " > 0 by A6;
then A11: 1 / p > 0 ;
[/((1 / p) to_power (1 / 8))\] >= (1 / p) to_power (1 / 8) by INT_1:def 5;
then A12: N1 >= (1 / p) to_power (1 / 8) by A9, XXREAL_0:2;
A13: (1 / p1) to_power (1 / 8) > 0 by A11, POWER:39;
A14: n >= N by A7, A10, XXREAL_0:2;
A15: ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n = ((seq_n^ 8) . n) / (g . n) by Lm4;
g . n = (1 + e) to_power ((1 * n) + 0 ) by Def1;
then A16: ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n = (n to_power 8) / ((1 + e) to_power n) by A7, A8, A10, A15, Def3
.= (2 to_power (8 * (log 2,n))) / ((1 + e) to_power n) by A7, A8, A10, Lm3
.= (2 to_power (8 * (log 2,n))) / (2 to_power (n * (log 2,(1 + e)))) by A3, Lm3
.= 2 to_power ((8 * (log 2,n)) - (n * (log 2,(1 + e)))) by POWER:34
.= 2 to_power (- ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) ;
n >= (1 / p) to_power (1 / 8) by A10, A12, XXREAL_0:2;
then n to_power 8 >= ((1 / p) to_power (1 / 8)) to_power 8 by A13, Lm6;
then n to_power 8 >= (1 / p1) to_power ((1 / 8) * 8) by A11, POWER:38;
then n to_power 8 >= 1 / p1 by POWER:30;
then 1 / (n to_power 8) <= 1 / (1 / p) by A11, XREAL_1:87;
then 1 / (n to_power 8) <= 1 / (p " ) ;
then 1 / (n to_power 8) <= p ;
then 1 / (2 to_power (8 * (log 2,n))) <= p by A7, A8, A10, Lm3;
then A17: 2 to_power (- (8 * (log 2,n))) <= p by POWER:33;
(n * (log 2,(1 + e))) - (8 * (log 2,n)) > 8 * (log 2,n) by A4, A14;
then A18: 2 to_power ((n * (log 2,(1 + e))) - (8 * (log 2,n))) > 2 to_power (8 * (log 2,n)) by POWER:44;
2 to_power (8 * (log 2,n)) > 0 by POWER:39;
then 1 / (2 to_power ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) < 1 / (2 to_power (8 * (log 2,n))) by A18, XREAL_1:90;
then 2 to_power (- ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) < 1 / (2 to_power (8 * (log 2,n))) by POWER:33;
then ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n < 2 to_power (- (8 * (log 2,n))) by A16, POWER:33;
then A19: ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n < p by A17, XXREAL_0:2;
((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n > 0 by A16, POWER:39;
hence abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p by A19, ABSVALUE:def 1; :: thesis: verum

end;

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