let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) <> 0 implies ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " ) )
set s = f /" g;
set als = |.(lim (f /" g)).|;
set ls = lim (f /" g);
assume that
A1: f /" g is convergent and
A2: lim (f /" g) <> 0 ; :: thesis: ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " )
consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
|.(lim (f /" g)).| / 2 < |.((f /" g) . m).| by A1, A2, SEQ_2:16;
A4: 0 < |.(lim (f /" g)).| by A2, COMPLEX1:47;
then 0 * 0 < |.(lim (f /" g)).| * |.(lim (f /" g)).| by XREAL_1:96;
then A5: 0 < (|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2 by XREAL_1:215;
consider N2 being Nat such that
A6: for n being Nat st n >= N2 holds
g . n > 0 by Def4;
consider N1 being Nat such that
A7: for n being Nat st n >= N1 holds
f . n > 0 by Def4;
A8: 0 <> |.(lim (f /" g)).| by A2, COMPLEX1:47;
A9: now :: thesis: for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.(((g /" f) . m) - ((lim (f /" g)) ")).| < p
set N3 = N1 + N2;
let p be Real; :: thesis: ( 0 < p implies ex n being set st
for m being Nat st n <= m holds
|.(((g /" f) . m) - ((lim (f /" g)) ")).| < p )
set N4 = (N1 + N2) + n1;
A10: 0 <> |.(lim (f /" g)).| / 2 by A2, COMPLEX1:47;
A11: (p * (|.(lim (f /" g)).| / 2)) / (|.(lim (f /" g)).| / 2) = (p * (|.(lim (f /" g)).| / 2)) * ((|.(lim (f /" g)).| / 2) ") by XCMPLX_0:def 9
.= p * ((|.(lim (f /" g)).| / 2) * ((|.(lim (f /" g)).| / 2) "))
.= p * 1 by A10, XCMPLX_0:def 7
.= p ;
assume A12: 0 < p ; :: thesis: ex n being set st
for m being Nat st n <= m holds
|.(((g /" f) . m) - ((lim (f /" g)) ")).| < p
then 0 * 0 < p * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2) by A5, XREAL_1:96;
then consider n2 being Nat such that
A13: for m being Nat st n2 <= m holds
|.(((f /" g) . m) - (lim (f /" g))).| < p * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2) by A1, SEQ_2:def 7;
take n = ((N1 + N2) + n1) + n2; :: thesis: for m being Nat st n <= m holds
|.(((g /" f) . m) - ((lim (f /" g)) ")).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((g /" f) . m) - ((lim (f /" g)) ")).| < p )
assume A14: n <= m ; :: thesis: |.(((g /" f) . m) - ((lim (f /" g)) ")).| < p
set asm = |.((f /" g) . m).|;
A15: (p * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2)) / (|.((f /" g) . m).| * |.(lim (f /" g)).|) = (p * ((2 ") * (|.(lim (f /" g)).| * |.(lim (f /" g)).|))) * ((|.((f /" g) . m).| * |.(lim (f /" g)).|) ") by XCMPLX_0:def 9
.= (p * (2 ")) * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) * ((|.(lim (f /" g)).| * |.((f /" g) . m).|) "))
.= (p * (2 ")) * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) * ((|.(lim (f /" g)).| ") * (|.((f /" g) . m).| "))) by XCMPLX_1:204
.= (p * (2 ")) * ((|.(lim (f /" g)).| * (|.(lim (f /" g)).| * (|.(lim (f /" g)).| "))) * (|.((f /" g) . m).| "))
.= (p * (2 ")) * ((|.(lim (f /" g)).| * 1) * (|.((f /" g) . m).| ")) by A8, XCMPLX_0:def 7
.= (p * (|.(lim (f /" g)).| / 2)) * (|.((f /" g) . m).| ")
.= (p * (|.(lim (f /" g)).| / 2)) / |.((f /" g) . m).| by XCMPLX_0:def 9 ;
n1 <= (N1 + N2) + n1 by NAT_1:12;
then n1 <= n by NAT_1:12;
then n1 <= m by A14, XXREAL_0:2;
then A16: |.(lim (f /" g)).| / 2 < |.((f /" g) . m).| by A3;
A17: 0 < |.(lim (f /" g)).| / 2 by A4, XREAL_1:215;
then 0 * 0 < p * (|.(lim (f /" g)).| / 2) by A12, XREAL_1:96;
then A18: (p * (|.(lim (f /" g)).| / 2)) / |.((f /" g) . m).| < (p * (|.(lim (f /" g)).| / 2)) / (|.(lim (f /" g)).| / 2) by A16, A17, XREAL_1:76;
N2 <= N1 + N2 by NAT_1:12;
then N2 <= (N1 + N2) + n1 by NAT_1:12;
then N2 <= n by NAT_1:12;
then N2 <= m by A14, XXREAL_0:2;
then A19: g . m <> 0 by A6;
N1 <= N1 + N2 by NAT_1:12;
then N1 <= (N1 + N2) + n1 by NAT_1:12;
then N1 <= n by NAT_1:12;
then N1 <= m by A14, XXREAL_0:2;
then f . m <> 0 by A7;
then (f . m) / (g . m) <> 0 by A19, XCMPLX_1:50;
then A20: (f /" g) . m <> 0 by Lm1;
then ((f /" g) . m) * (lim (f /" g)) <> 0 by A2, XCMPLX_1:6;
then 0 < |.(((f /" g) . m) * (lim (f /" g))).| by COMPLEX1:47;
then A21: 0 < |.((f /" g) . m).| * |.(lim (f /" g)).| by COMPLEX1:65;
n2 <= n by NAT_1:12;
then n2 <= m by A14, XXREAL_0:2;
then |.(((f /" g) . m) - (lim (f /" g))).| < p * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2) by A13;
then A22: |.(((f /" g) . m) - (lim (f /" g))).| / (|.((f /" g) . m).| * |.(lim (f /" g)).|) < (p * ((|.(lim (f /" g)).| * |.(lim (f /" g)).|) / 2)) / (|.((f /" g) . m).| * |.(lim (f /" g)).|) by A21, XREAL_1:74;
|.(((g /" f) . m) - ((lim (f /" g)) ")).| = |.(((g . m) / (f . m)) - ((lim (f /" g)) ")).| by Lm1
.= |.((((f . m) / (g . m)) ") - ((lim (f /" g)) ")).| by XCMPLX_1:213
.= |.((((f /" g) . m) ") - ((lim (f /" g)) ")).| by Lm1
.= |.(((f /" g) . m) - (lim (f /" g))).| / (|.((f /" g) . m).| * |.(lim (f /" g)).|) by A2, A20, SEQ_2:2 ;
hence |.(((g /" f) . m) - ((lim (f /" g)) ")).| < p by A22, A15, A18, A11, XXREAL_0:2; :: thesis: verum
end;
hence g /" f is convergent by SEQ_2:def 6; :: thesis: lim (g /" f) = (lim (f /" g)) "
hence lim (g /" f) = (lim (f /" g)) " by A9, SEQ_2:def 7; :: thesis: verum