let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( f in Big_Oh g & not g in Big_Oh f ) )
assume A1: ( f /" g is convergent & lim (f /" g) = 0 ) ; :: thesis: ( f in Big_Oh g & not g in Big_Oh f )
then consider N being Element of NAT such that
A2: for n being Element of NAT st N <= n holds
abs (((f /" g) . n) - 0 ) < 1 by SEQ_2:def 7;
consider N1 being Element of NAT such that
A3: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A4: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
A5: not g in Big_Oh f

proof

assume g in Big_Oh f ; :: thesis: contradiction
then consider t being Element of Funcs NAT ,REAL such that
A6: t = g and
A7: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A8: c > 0 and
A9: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A7;
reconsider q = NAT --> (1 / c) as Real_Sequence ;
set a = max N,N2;
A10: max N,N2 >= N2 by XXREAL_0:25;
A11: max N,N2 >= N by XXREAL_0:25;

now

take a = max N,N2; :: thesis: for n being Element of NAT st n >= a holds
q . n <= (f /" g) . n
let n be Element of NAT ; :: thesis: ( n >= a implies q . n <= (f /" g) . n )
assume A12: n >= a ; :: thesis: q . n <= (f /" g) . n
then n >= N by A11, XXREAL_0:2;
then ( g . n <= c * (f . n) & g . n >= 0 ) by A6, A9;
then A13: (g . n) * ((g . n) " ) <= (c * (f . n)) * ((g . n) " ) by XREAL_1:66;
n >= N2 by A10, A12, XXREAL_0:2;
then g . n > 0 by A4;
then 1 <= (c * (f . n)) * ((g . n) " ) by A13, XCMPLX_0:def 7;
then (c " ) * 1 <= (c " ) * (c * ((f . n) * ((g . n) " ))) by A8, XREAL_1:66;
then (c " ) * 1 <= ((c " ) * c) * ((f . n) * ((g . n) " )) ;
then (c " ) * 1 <= 1 * ((f . n) * ((g . n) " )) by A8, XCMPLX_0:def 7;
then 1 / c <= (1 * (f . n)) * ((g . n) " ) by XCMPLX_0:def 9;
then 1 / c <= (1 * (f . n)) / (g . n) by XCMPLX_0:def 9;
then 1 / c <= (f /" g) . n by Lm1;
hence q . n <= (f /" g) . n by FUNCOP_1:13; :: thesis: verum

end;

then A14: f /" g majorizes q by Def11;

now

take p = 1 / c; :: thesis: for p1 being real number st p1 > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
let p1 be real number ; :: thesis: ( p1 > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1 )
assume A15: p1 > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((q . n) - p) < p1 )
assume n >= N ; :: thesis: abs ((q . n) - p) < p1
abs ((q . n) - p) = abs ((1 / c) - (1 / c)) by FUNCOP_1:13
.= abs 0 ;
hence abs ((q . n) - p) < p1 by A15, ABSVALUE:7; :: thesis: verum

end;

then A16: q is convergent by SEQ_2:def 6;

now

let p1 be real number ; :: thesis: ( p1 > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1 )
assume A17: p1 > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((q . n) - (1 / c)) < p1 )
assume n >= N ; :: thesis: abs ((q . n) - (1 / c)) < p1
abs ((q . n) - (1 / c)) = abs ((1 / c) - (1 / c)) by FUNCOP_1:13
.= abs 0 ;
hence abs ((q . n) - (1 / c)) < p1 by A17, ABSVALUE:7; :: thesis: verum

end;

then lim q = 1 / c by A16, SEQ_2:def 7;
then 1 / c <= 0 by A1, A14, A16, Th4;
then (1 / c) * c <= 0 * c by A8;
hence contradiction by A8, XCMPLX_1:107; :: thesis: verum

end;

set b = max N,N1;
set a = max (max N,N1),N2;

A18: now

let n be Element of NAT ; :: thesis: ( n >= max (max N,N1),N2 implies ( f . n <= 1 * (g . n) & f . n >= 0 ) )
assume A19: n >= max (max N,N1),N2 ; :: thesis: ( f . n <= 1 * (g . n) & f . n >= 0 )
max (max N,N1),N2 >= max N,N1 by XXREAL_0:25;
then A20: n >= max N,N1 by A19, XXREAL_0:2;
max N,N1 >= N by XXREAL_0:25;
then n >= N by A20, XXREAL_0:2;
then abs (((f /" g) . n) - 0 ) < 1 by A2;
then (f /" g) . n <= 1 by ABSVALUE:12;
then (f . n) * ((g " ) . n) <= 1 by SEQ_1:12;
then A21: (f . n) * ((g . n) " ) <= 1 by VALUED_1:10;
max (max N,N1),N2 >= N2 by XXREAL_0:25;
then A22: n >= N2 by A19, XXREAL_0:2;
then A23: g . n <> 0 by A4;
g . n > 0 by A4, A22;
then ((f . n) * ((g . n) " )) * (g . n) <= 1 * (g . n) by A21, XREAL_1:66;
then (f . n) * (((g . n) " ) * (g . n)) <= 1 * (g . n) ;
then (f . n) * 1 <= 1 * (g . n) by A23, XCMPLX_0:def 7;
hence f . n <= 1 * (g . n) ; :: thesis: f . n >= 0
max N,N1 >= N1 by XXREAL_0:25;
then n >= N1 by A20, XXREAL_0:2;
hence f . n >= 0 by A3; :: thesis: verum

end;

f is Element of Funcs NAT ,REAL by FUNCT_2:11;
hence ( f in Big_Oh g & not g in Big_Oh f ) by A18, A5; :: thesis: verum