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 Nat such that
A2: for n being Nat st N <= n holds
|.(((f /" g) . n) - 0).| < 1 by SEQ_2:def 7;
consider N1 being Nat such that
A3: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
consider N2 being Nat such that
A4: for n being Nat st n >= N2 holds
g . n > 0 by Def4;
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 c = c as Element of REAL by XREAL_0:def 1;
set q = seq_const (1 / c);
reconsider a = max (N,N2) as Element of NAT by ORDINAL1:def 12;
A10: a >= N2 by XXREAL_0:25;
A11: a >= N by XXREAL_0:25;

now :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a holds
(seq_const (1 / c)) . n <= (f /" g) . n

take a = a; :: thesis: for n being Element of NAT st n >= a holds
(seq_const (1 / c)) . n <= (f /" g) . n
let n be Element of NAT ; :: thesis: ( n >= a implies (seq_const (1 / c)) . n <= (f /" g) . n )
assume A12: n >= a ; :: thesis: (seq_const (1 / c)) . 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 (seq_const (1 / c)) . n <= (f /" g) . n by SEQ_1:57; :: thesis: verum

end;

then A14: f /" g majorizes seq_const (1 / c) ;

now :: thesis: for p1 being Real st p1 > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1

set p = 1 / c;
let p1 be Real; :: thesis: ( p1 > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 )
assume A15: p1 > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
let n be Nat; :: thesis: ( n >= N implies |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 )
assume n >= N ; :: thesis: |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
|.(((seq_const (1 / c)) . n) - (1 / c)).| = |.((1 / c) - (1 / c)).| by SEQ_1:57
.= |.0.| ;
hence |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 by A15, ABSVALUE:2; :: thesis: verum

end;

then A16: seq_const (1 / c) is convergent by SEQ_2:def 6;

now :: thesis: for p1 being Real st p1 > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1

let p1 be Real; :: thesis: ( p1 > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 )
assume A17: p1 > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
let n be Nat; :: thesis: ( n >= N implies |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 )
assume n >= N ; :: thesis: |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1
|.(((seq_const (1 / c)) . n) - (1 / c)).| = |.((1 / c) - (1 / c)).| by SEQ_1:57
.= |.0.| ;
hence |.(((seq_const (1 / c)) . n) - (1 / c)).| < p1 by A17, ABSVALUE:2; :: thesis: verum

end;

then lim (seq_const (1 / c)) = 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;

reconsider b = max (N,N1) as Element of NAT by ORDINAL1:def 12;
reconsider a = max (b,N2) as Element of NAT by ORDINAL1:def 12;

A18: now :: thesis: for n being Element of NAT st n >= a holds
( f . n <= 1 * (g . n) & f . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= a implies ( f . n <= 1 * (g . n) & f . n >= 0 ) )
assume A19: n >= a ; :: thesis: ( f . n <= 1 * (g . n) & f . n >= 0 )
a >= b by XXREAL_0:25;
then A20: n >= b by A19, XXREAL_0:2;
b >= N by XXREAL_0:25;
then n >= N by A20, XXREAL_0:2;
then |.(((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;
a >= 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
b >= 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