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

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not f . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not f . n <= 0 )
assume A3: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (sqrt n) by A1;
hence not f . n <= 0 by A3, POWER:39; :: thesis: verum

end;

set h = f /" (seq_a^ 2,1,0 );
reconsider f = f as eventually-positive Real_Sequence by A2;
reconsider g = seq_a^ 2,1,0 as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = seq_a^ 2,1,0 & Big_Oh f c= Big_Oh s1 & not Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = f & g = seq_a^ 2,1,0 & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
consider N being Element of NAT such that
A4: for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log 2,n)) > n / 2 by Lm40;

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 (((f /" (seq_a^ 2,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 (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p
set N1 = max N,(max (2 * [/(log 2,(1 / p))\]),2);
A7: max N,(max (2 * [/(log 2,(1 / p))\]),2) >= N by XXREAL_0:25;
A8: max N,(max (2 * [/(log 2,(1 / p))\]),2) is Integer

proof

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

suppose max N,(max (2 * [/(log 2,(1 / p))\]),2) = N ; :: thesis: max N,(max (2 * [/(log 2,(1 / p))\]),2) is Integer

hence max N,(max (2 * [/(log 2,(1 / p))\]),2) is Integer ; :: thesis: verum

end;

suppose max N,(max (2 * [/(log 2,(1 / p))\]),2) = max (2 * [/(log 2,(1 / p))\]),2 ; :: thesis: max N,(max (2 * [/(log 2,(1 / p))\]),2) is Integer

hence max N,(max (2 * [/(log 2,(1 / p))\]),2) is Integer by XXREAL_0:16; :: thesis: verum

end;

end;

end;

A9: max N,(max (2 * [/(log 2,(1 / p))\]),2) >= max (2 * [/(log 2,(1 / p))\]),2 by XXREAL_0:25;
max (2 * [/(log 2,(1 / p))\]),2 >= 2 * [/(log 2,(1 / p))\] by XXREAL_0:25;
then A10: max N,(max (2 * [/(log 2,(1 / p))\]),2) >= 2 * [/(log 2,(1 / p))\] by A9, XXREAL_0:2;
reconsider N1 = max N,(max (2 * [/(log 2,(1 / p))\]),2) as Element of NAT by A7, A8, INT_1:16;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p )
A11: (f /" (seq_a^ 2,1,0 )) . n = (f . n) / (g . n) by Lm4;
A12: [/(log 2,(1 / p))\] >= log 2,(1 / p) by INT_1:def 5;
assume A13: n >= N1 ; :: thesis: abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p
then n >= 2 * [/(log 2,(1 / p))\] by A10, XXREAL_0:2;
then n / 2 >= [/(log 2,(1 / p))\] by XREAL_1:79;
then n / 2 >= log 2,(1 / p) by A12, XXREAL_0:2;
then - (n / 2) <= - (log 2,(1 / p)) by XREAL_1:26;
then 2 to_power (- (n / 2)) <= 2 to_power (- (log 2,(1 / p))) by PRE_FF:10;
then 2 to_power (- (n / 2)) <= 1 / (2 to_power (log 2,(1 / p))) by POWER:33;
then A14: 2 to_power (- (n / 2)) <= 1 / (1 / p) by A6, POWER:def 3;
A15: g . n = 2 to_power ((1 * n) + 0 ) by Def1
.= 2 to_power n ;
A16: max (2 * [/(log 2,(1 / p))\]),2 >= 2 by XXREAL_0:25;
then f . n = n to_power (sqrt n) by A1, A9, A13
.= 2 to_power ((sqrt n) * (log 2,n)) by A9, A16, A13, Lm3 ;
then A17: (f /" (seq_a^ 2,1,0 )) . n = 2 to_power (((sqrt n) * (log 2,n)) - n) by A11, A15, POWER:34
.= 2 to_power (- (n - ((sqrt n) * (log 2,n)))) ;
then A18: (f /" (seq_a^ 2,1,0 )) . n > 0 by POWER:39;
n >= N by A7, A13, XXREAL_0:2;
then n - ((sqrt n) * (log 2,n)) > n / 2 by A4;
then - (n - ((sqrt n) * (log 2,n))) < - (n / 2) by XREAL_1:26;
then 2 to_power (- (n - ((sqrt n) * (log 2,n)))) < 2 to_power (- (n / 2)) by POWER:44;
then (f /" (seq_a^ 2,1,0 )) . n < p by A17, A14, XXREAL_0:2;
hence abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p by A18, ABSVALUE:def 1; :: thesis: verum

end;

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