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:64;
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:64;
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:7; :: 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:7
.= abs 0 ;
hence abs ((q . n) - p) < p1 by A15, ABSVALUE:2; :: 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:7
.= abs 0 ;
hence abs ((q . n) - (1 / c)) < p1 by A17, ABSVALUE:2; :: 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:106; :: 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:5;
then (f . n) * ((g ") . n) <= 1 by SEQ_1:8;
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:64;
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:8;
hence ( f in Big_Oh g & not g in Big_Oh f ) by A18, A5; :: thesis: verum