:: The de l'Hospital Theorem
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received February 20, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PARTFUN1, NUMBERS, REAL_1, SEQ_1, SUBSET_1, FCONT_1, ARYTM_3,
RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2, TARSKI, XBOOLE_0, FUNCT_2, FUNCT_1,
LIMFUNC2, LIMFUNC1, RCOMP_1, CARD_1, XXREAL_1, ARYTM_1, FDIFF_1,
VALUED_1, XXREAL_0, NAT_1, ASYMPT_1, VALUED_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1,
COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1,
LIMFUNC1, LIMFUNC2, LIMFUNC3, XXREAL_0;
constructors PARTFUN1, FUNCOP_1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1,
RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, LIMFUNC2,
LIMFUNC3, VALUED_1, XXREAL_2, RELSET_1, SEQ_4, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, RCOMP_1,
VALUED_0, XXREAL_2, XBOOLE_0, SEQ_4, FUNCT_2, SEQ_1, SEQ_2;
requirements SUBSET, ARITHM, NUMERALS;
definitions TARSKI;
equalities PROB_1, LIMFUNC1;
expansions TARSKI;
theorems TARSKI, NAT_1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, ROLLE, SEQ_2,
SEQ_4, LIMFUNC2, LIMFUNC1, LIMFUNC3, ZFMISC_1, FUNCT_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, VALUED_1,
XXREAL_1, XXREAL_2, FUNCT_2, VALUED_0, ORDINAL1, SEQ_1;
schemes FUNCT_2;
begin
reserve f,g for PartFunc of REAL,REAL,
r,r1,r2,g1,g2,g3,g4,g5,g6,x,x0,t,c for Real,
a,b,s for Real_Sequence,
n,k for Element of NAT;
theorem
f is_continuous_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1
& g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_convergent_in
x0
proof
assume that
A1: f is_continuous_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
now
let s such that
A3: s is convergent & lim s=x0 and
A4: rng s c= dom f \ {x0};
dom f \ {x0} c= dom f by XBOOLE_1:36;
then rng s c= dom f by A4;
hence f/*s is convergent & lim (f/*s) = f.x0 by A1,A3,FCONT_1:def 1;
end;
hence thesis by A2,LIMFUNC3:def 1;
end;
theorem Th2:
f is_right_convergent_in x0 & lim_right(f,x0) = t iff (for r st
x0<r ex t st t<r & x0<t & t in dom f) & for a st a is convergent & lim a = x0 &
rng a c= dom f /\ right_open_halfline(x0) holds f/*a is convergent & lim(f/*a)
= t
proof
thus f is_right_convergent_in x0 & lim_right(f,x0) = t implies (for r st x0<
r ex t st t<r & x0<t & t in dom f) & for a st a is convergent & lim a = x0 &
rng a c= dom f /\ right_open_halfline(x0) holds f/*a is convergent & lim(f/*a)
= t by LIMFUNC2:def 4,def 8;
reconsider t as Real;
(for r st x0<r ex t st t<r & x0<t & t in dom f) & (for a st a is
convergent & lim a = x0 & rng a c= dom f /\ right_open_halfline(x0) holds f/*a
is convergent & lim(f/*a) = t) implies f is_right_convergent_in x0 & lim_right(
f,x0) = t
proof
assume that
A1: for r st x0<r ex t st t<r & x0<t & t in dom f and
A2: for a st a is convergent & lim a = x0 & rng a c= dom f /\
right_open_halfline(x0) holds f/*a is convergent & lim(f/*a) = t;
thus f is_right_convergent_in x0 by A1,A2,LIMFUNC2:def 4;
hence thesis by A2,LIMFUNC2:def 8;
end;
hence thesis;
end;
theorem Th3:
f is_left_convergent_in x0 & lim_left(f,x0) = t iff (for r st r<
x0 ex t st r<t & t<x0 & t in dom f) & for a st a is convergent & lim a = x0 &
rng a c= dom f /\ left_open_halfline(x0) holds f/*a is convergent & lim(f/*a) =
t
proof
thus f is_left_convergent_in x0 & lim_left(f,x0) = t implies (for r st r<x0
ex t st r<t & t<x0 & t in dom f) & for a st a is convergent & lim a = x0 & rng
a c= dom f /\ left_open_halfline(x0) holds f/*a is convergent & lim(f/*a) = t
by LIMFUNC2:def 1,def 7;
reconsider t as Real;
(for r st r<x0 ex t st r<t & t<x0 & t in dom f) & (for a st a is
convergent & lim a = x0 & rng a c= dom f /\ left_open_halfline(x0) holds f/*a
is convergent & lim(f/*a) = t) implies f is_left_convergent_in x0 & lim_left(f,
x0) = t
proof
assume that
A1: for r st r<x0 ex t st r<t & t<x0 & t in dom f and
A2: for a st a is convergent & lim a = x0 & rng a c= dom f /\
left_open_halfline(x0) holds f/*a is convergent & lim(f/*a) = t;
thus f is_left_convergent_in x0 by A1,A2,LIMFUNC2:def 1;
hence thesis by A2,LIMFUNC2:def 7;
end;
hence thesis;
end;
theorem Th4:
(ex N being Neighbourhood of x0 st N\{x0} c=dom f) implies for r1
,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 &
g2 in dom f
proof
given N being Neighbourhood of x0 such that
A1: N\{x0} c= dom f;
consider r be Real such that
A2: 0<r and
A3: N=].x0-r,x0+r.[ by RCOMP_1:def 6;
N\{x0}=].x0-r,x0.[ \/ ].x0,x0+r.[ by A2,A3,LIMFUNC3:4;
hence thesis by A1,A2,LIMFUNC3:5;
end;
theorem
(ex N being Neighbourhood of x0 st N c= dom f & N c= dom g & f
is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f/g) & N
c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 & (f`|N)/(g`|N)
is_divergent_to+infty_in x0) implies f/g is_divergent_to+infty_in x0
proof
given N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: N c= dom g and
A3: f is_differentiable_on N and
A4: g is_differentiable_on N and
A5: N \ {x0} c= dom (f/g) and
A6: N c= dom ((f`|N)/(g`|N)) and
A7: f.x0 = 0 & g.x0 = 0 and
A8: (f`|N)/(g`|N) is_divergent_to+infty_in x0;
consider r be Real such that
A9: 0<r and
A10: N = ].x0-r,x0+r.[ by RCOMP_1:def 6;
A11: for x st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|N)/(g`|N)) .c
proof
A12: x0+0<x0+r by A9,XREAL_1:8;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A12;
then
A13: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A14: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A15: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A16: x0-r<x and
A17: x<x0;
set f1 = (f.x)(#)g - (g.x)(#)f;
A18: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A19: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x<x0+r by A17,A12,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A16;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A20: [.x,x0.] c= N by A10,A13,XXREAL_2:def 12;
then
A21: [.x,x0.] c= dom f & [.x,x0.] c= dom g by A1,A2;
then
A22: [.x,x0.] c= dom f1 by A19,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A23: ((f.x)(#)g)|[.x,x0.] is continuous by A2,A20,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A24: ((g.x)(#)f)|[.x,x0.] is continuous by A1,A20,FCONT_1:20,XBOOLE_1:1;
[.x,x0.] c= dom((f.x)(#)g - (g.x)(#)f) by A21,A19,XBOOLE_1:19;
then
A25: ((f.x)(#)g - (g.x)(#)f)|[.x,x0.] is continuous by A24,A18,A19,A23,
FCONT_1:18;
A26: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then
A27: ].x,x0.[ c= N by A20;
A28: x in [.x,x0.] by A17,XXREAL_1:1;
then x in dom f1 by A22;
then
A29: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A30: x in dom ((f.x) (#) g) by XBOOLE_0:def 4;
A31: x0 in [.x,x0.] by A17,XXREAL_1:1;
then x0 in dom f1 by A22;
then
A32: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A33: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A34: x in dom ((g.x)(#)f) by A29,XBOOLE_0:def 4;
A35: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A22,A28,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A30,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A34,VALUED_1:def 5
.= 0;
A36: x0 in dom ((g.x)(#)f) by A32,XBOOLE_0:def 4;
not x in {x0} by A17,TARSKI:def 1;
then
A37: x in [.x,x0.]\{x0} by A28,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A38: ].x,x0.[ c= dom ((f.x)(#)g) by A27;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A39: ].x,x0.[ c= dom ((g.x)(#)f) by A27;
then ].x,x0.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A38,XBOOLE_1:19;
then
A40: ].x,x0.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A3,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A41: (g.x)(#)f is_differentiable_on ].x,x0.[ by A39,FDIFF_1:20;
g is_differentiable_on ].x,x0.[ by A4,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A42: (f.x)(#)g is_differentiable_on ].x,x0.[ by A38,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A22,A31,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A33,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A36,VALUED_1:def 5
.= 0;
then consider t such that
A43: t in ].x,x0.[ and
A44: diff(f1,t)=0 by A17,A25,A41,A40,A42,A22,A35,FDIFF_1:19,ROLLE:1;
A45: (g.x)(#)f is_differentiable_in t by A41,A43,FDIFF_1:9;
A46: f is_differentiable_in t by A3,A27,A43,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A42,A43,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A44,A45,FDIFF_1:14;
then
A47: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A46,FDIFF_1:15;
take t;
A48: t in [.x,x0.] by A26,A43;
[.x,x0.]\{x0} c= N\{x0} by A20,XBOOLE_1:33;
then
A49: [.x,x0.]\{x0} c= dom(f/g) by A5;
then [.x,x0.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x,x0.]\{x0} c= dom g\g"{0} by A15;
then
A50: x in dom g & not x in g"{0} by A37,XBOOLE_0:def 5;
A51: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A50,FUNCT_1:def 7;
end;
A52: [.x,x0.] c= dom ((f`|N)/(g`|N)) by A6,A20;
then [.x,x0.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x,x0.] c= dom (g`|N)\(g`|N)"{0} by A14;
then
A53: t in dom (g`|N) & not t in (g`|N)"{0} by A48,XBOOLE_0:def 5;
A54: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A20,A48,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A53,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A27,A43,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A47,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A51,A54,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A49,A37,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A20,A48,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A20,A48,FDIFF_1:def 7;
hence thesis by A43,A52,A48,RFUNCT_1:def 1;
end;
A55: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
left_open_halfline(x0) holds (f/g)/*a is divergent_to+infty
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A56: a is convergent and
A57: lim a = x0 and
A58: rng a c= dom (f/g) /\ left_open_halfline(x0);
consider k such that
A59: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A56,A57,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT, Real] means $2 in ].a1.$1,x0.[ & (((f/g)
/*a)^\k).$1=((f`|N)/(g`|N)).$2;
A60: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in left_open_halfline(x0) by A58,XBOOLE_0:def 4;
then a.(n+k) in {g1:g1<x0} by XXREAL_1:229;
then ex g1 st a.(n+k)=g1 & g1<x0;
hence a1.n<x0 by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence x0-r<a1.n by A59;
end;
A61: for n ex c be Element of REAL st X[n,c]
proof
let n;
A62: rng a1 c= rng a by VALUED_0:21;
x0-r<a1.n & a1.n<x0 by A60;
then consider c such that
A63: c in ].a1.n,x0.[ and
A64: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A11;
take c;
A65: dom (f/g) /\ left_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A58;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A64,A62,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A58,A63,A65,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A66: for n holds X[n,b.n] from FUNCT_2:sch 3(A61);
A67: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then b.n in ].a1.n,x0.[ by A66;
then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
hence a1.n<=b.n & b.n<= d.n by SEQ_1:57;
end;
A68: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
A69: x0<x0+r by A9,XREAL_1:29;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A69;
then
A70: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A71: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A72: x=b.n by FUNCT_2:113;
a1.n<x0 by A60;
then
A73: a1.n<x0+r by A69,XXREAL_0:2;
x0-r<a1.n by A60;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A73;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A70,
XXREAL_1:25,XXREAL_2:def 12;
then ].a1.n,x0.[ c= ].x0-r,x0+r.[;
then
A74: ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A75: x in ].a1.n,x0.[ by A66,A72;
then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1 = x & a1.n<g1 & g1<x0;
then not x in {x0} by TARSKI:def 1;
hence thesis by A75,A74,XBOOLE_0:def 5;
end;
A76: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A77: now
let n be Nat;
A78: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A66,A78;
hence (((f`|N)/(g`|N))/*b).n <= (((f/g)/*a)^\k).n by A71,A76,FUNCT_2:108
,XBOOLE_1:1,A78;
end;
lim a1=x0 by A56,A57,SEQ_4:20;
then b is convergent & lim b=x0 by A56,A68,A67,SEQ_2:19,20;
then ((f`|N)/(g`|N))/*b is divergent_to+infty by A8,A71,LIMFUNC3:def 2;
then ((f/g)/*a)^\k is divergent_to+infty by A77,LIMFUNC1:42;
hence thesis by LIMFUNC1:7;
end;
A79: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom (f/g)
& g2<r2 & x0<g2 & g2 in dom (f/g) by A5,Th4;
then for r1 st r1<x0 ex t st r1<t & t<x0 & t in dom (f/g) by LIMFUNC3:8;
then
A80: f/g is_left_divergent_to+infty_in x0 by A55,LIMFUNC2:def 2;
A81: for x st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|N)/(g`|N)). c
proof
A82: x0-r<x0 by A9,XREAL_1:44;
x0+0<x0+r by A9,XREAL_1:8;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A82;
then
A83: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A84: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A85: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A86: x0<x and
A87: x<x0+r;
set f1 = (f.x)(#)g - (g.x)(#)f;
A88: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
x0-r<x by A86,A82,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A87;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A89: [.x0,x.] c= N by A10,A83,XXREAL_2:def 12;
then [.x0,x.] c= dom f & [.x0,x.] c= dom g by A1,A2;
then
A90: [.x0,x.] c= dom f /\ dom g by XBOOLE_1:19;
then
A91: [.x0,x.] c= dom f1 by A88,VALUED_1:12;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x0,x.] is continuous by A89,FCONT_1:16;
then
A92: ((f.x)(#)g)|[.x0,x.] is continuous by A2,A89,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x0,x.] is continuous by A89,FCONT_1:16;
then ((g.x)(#)f)|[.x0,x.] is continuous by A1,A89,FCONT_1:20,XBOOLE_1:1;
then
A93: ((f.x)(#)g - (g.x)(#)f)|[.x0,x.] is continuous by A90,A88,A92,FCONT_1:18;
A94: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then
A95: ].x0,x.[ c= N by A89;
A96: x in [.x0,x.] by A86,XXREAL_1:1;
then x in dom f1 by A91;
then
A97: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A98: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A99: x0 in [.x0,x.] by A86,XXREAL_1:1;
then x0 in dom f1 by A91;
then
A100: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A101: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A102: x in dom ((g.x)(#)f) by A97,XBOOLE_0:def 4;
A103: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A91,A96,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A98,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A102,VALUED_1:def 5
.= 0;
A104: x0 in dom ((g.x)(#)f) by A100,XBOOLE_0:def 4;
not x in {x0} by A86,TARSKI:def 1;
then
A105: x in [.x0,x.]\{x0} by A96,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A106: ].x0,x.[ c= dom ((f.x)(#)g) by A95;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A107: ].x0,x.[ c= dom ((g.x)(#)f) by A95;
then ].x0,x.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A106,XBOOLE_1:19;
then
A108: ].x0,x.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A3,A89,A94,FDIFF_1:26,XBOOLE_1:1;
then
A109: (g.x)(#)f is_differentiable_on ].x0,x.[ by A107,FDIFF_1:20;
g is_differentiable_on ].x0,x.[ by A4,A89,A94,FDIFF_1:26,XBOOLE_1:1;
then
A110: (f.x)(#)g is_differentiable_on ].x0,x.[ by A106,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A91,A99,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A101,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A104,VALUED_1:def 5
.= 0;
then consider t such that
A111: t in ].x0,x.[ and
A112: diff(f1,t)=0 by A86,A93,A109,A108,A110,A91,A103,FDIFF_1:19,ROLLE:1;
A113: (g.x)(#)f is_differentiable_in t by A109,A111,FDIFF_1:9;
A114: f is_differentiable_in t by A3,A95,A111,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A110,A111,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A112,A113,FDIFF_1:14;
then
A115: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A114,FDIFF_1:15;
take t;
A116: t in [.x0,x.] by A94,A111;
[.x0,x.]\{x0} c= N\{x0} by A89,XBOOLE_1:33;
then
A117: [.x0,x.]\{x0} c= dom(f/g) by A5;
then [.x0,x.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x0,x.]\{x0} c= dom g\g"{0} by A85;
then
A118: x in dom g & not x in g"{0} by A105,XBOOLE_0:def 5;
A119: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A118,FUNCT_1:def 7;
end;
A120: [.x0,x.] c= dom ((f`|N)/(g`|N)) by A6,A89;
then [.x0,x.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x0,x.] c= dom (g`|N)\(g`|N)"{0} by A84;
then
A121: t in dom (g`|N) & not t in (g`|N)"{0} by A116,XBOOLE_0:def 5;
A122: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A89,A116,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A121,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A95,A111,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A115,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A119,A122,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A117,A105,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A89,A116,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A89,A116,FDIFF_1:def 7;
hence thesis by A111,A120,A116,RFUNCT_1:def 1;
end;
A123: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
right_open_halfline(x0) holds (f/g)/*a is divergent_to+infty
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A124: a is convergent and
A125: lim a = x0 and
A126: rng a c= dom (f/g) /\ right_open_halfline(x0);
consider k such that
A127: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A124,A125,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].x0,a1.$1.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A128: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in right_open_halfline(x0) by A126,XBOOLE_0:def 4;
then a.(n+k) in {g1:x0<g1} by XXREAL_1:230;
then ex g1 st a.(n+k)=g1 & x0<g1;
hence x0<a1.n by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence a1.n<x0+r by A127;
end;
A129: for n ex c be Element of REAL st X[n,c]
proof
let n;
A130: rng a1 c= rng a by VALUED_0:21;
x0<a1.n & a1.n<x0+r by A128;
then consider c such that
A131: c in ].x0,a1.n.[ and
A132: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A81;
take c;
A133: dom (f/g) /\ right_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A126;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A132,A130,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A126,A131,A133,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A134: for n holds X[n,b.n] from FUNCT_2:sch 3(A129);
A135: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then b.n in ].x0,a1.n.[ by A134;
then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
hence d.n<=b.n & b.n<=a1.n by SEQ_1:57;
end;
A136: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
A137: x0-r<x0 by A9,XREAL_1:44;
x0<x0+r by A9,XREAL_1:29;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A137;
then
A138: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A139: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A140: x=b.n by FUNCT_2:113;
x0<a1.n by A128;
then
A141: x0-r<a1.n by A137,XXREAL_0:2;
a1.n<x0+r by A128;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A141;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A138,
XXREAL_1:25,XXREAL_2:def 12;
then ].x0,a1.n.[ c= ].x0-r,x0+r.[;
then
A142: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A143: x in ].x0,a1.n.[ by A134,A140;
then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1 = x & x0<g1 & g1<a1.n;
then not x in {x0} by TARSKI:def 1;
hence thesis by A143,A142,XBOOLE_0:def 5;
end;
A144: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A145: now
let n be Nat;
A146: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A134,A146;
hence (((f`|N)/(g`|N))/*b).n <= (((f/g)/*a)^\k).n by A139,A144,
FUNCT_2:108,XBOOLE_1:1,A146;
end;
lim a1=x0 by A124,A125,SEQ_4:20;
then b is convergent & lim b=x0 by A124,A136,A135,SEQ_2:19,20;
then ((f`|N)/(g`|N))/*b is divergent_to+infty by A8,A139,LIMFUNC3:def 2;
then ((f/g)/*a)^\k is divergent_to+infty by A145,LIMFUNC1:42;
hence thesis by LIMFUNC1:7;
end;
for r1 st x0<r1 ex t st t<r1 & x0<t & t in dom (f/g) by A79,LIMFUNC3:8;
then f/g is_right_divergent_to+infty_in x0 by A123,LIMFUNC2:def 5;
hence thesis by A80,LIMFUNC3:12;
end;
theorem
(ex N being Neighbourhood of x0 st N c= dom f & N c= dom g & f
is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f/g) & N
c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 & (f`|N)/(g`|N)
is_divergent_to-infty_in x0) implies f/g is_divergent_to-infty_in x0
proof
given N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: N c= dom g and
A3: f is_differentiable_on N and
A4: g is_differentiable_on N and
A5: N \ {x0} c= dom (f/g) and
A6: N c= dom ((f`|N)/(g`|N)) and
A7: f.x0 = 0 & g.x0 = 0 and
A8: (f`|N)/(g`|N) is_divergent_to-infty_in x0;
consider r be Real such that
A9: 0<r and
A10: N = ].x0-r,x0+r.[ by RCOMP_1:def 6;
A11: for x st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|N)/(g`|N)) .c
proof
A12: x0+0<x0+r by A9,XREAL_1:8;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A12;
then
A13: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A14: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A15: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A16: x0-r<x and
A17: x<x0;
set f1 = (f.x)(#)g - (g.x)(#)f;
A18: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A19: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x<x0+r by A17,A12,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A16;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A20: [.x,x0.] c= N by A10,A13,XXREAL_2:def 12;
then
A21: [.x,x0.] c= dom f & [.x,x0.] c= dom g by A1,A2;
then
A22: [.x,x0.] c= dom f1 by A19,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A23: ((f.x)(#)g)|[.x,x0.] is continuous by A2,A20,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A24: ((g.x)(#)f)|[.x,x0.] is continuous by A1,A20,FCONT_1:20,XBOOLE_1:1;
[.x,x0.] c= dom((f.x)(#)g - (g.x)(#)f) by A21,A19,XBOOLE_1:19;
then
A25: ((f.x)(#)g - (g.x)(#)f)|[.x,x0.] is continuous by A18,A19,A24,A23,
FCONT_1:18;
A26: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then
A27: ].x,x0.[ c= N by A20;
A28: x in [.x,x0.] by A17,XXREAL_1:1;
then x in dom f1 by A22;
then
A29: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A30: x in dom ((f.x) (#) g) by XBOOLE_0:def 4;
A31: x0 in [.x,x0.] by A17,XXREAL_1:1;
then x0 in dom f1 by A22;
then
A32: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A33: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A34: x in dom ((g.x)(#)f) by A29,XBOOLE_0:def 4;
A35: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A22,A28,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A30,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A34,VALUED_1:def 5
.= 0;
A36: x0 in dom ((g.x)(#)f) by A32,XBOOLE_0:def 4;
not x in {x0} by A17,TARSKI:def 1;
then
A37: x in [.x,x0.]\{x0} by A28,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A38: ].x,x0.[ c= dom ((f.x)(#)g) by A27;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A39: ].x,x0.[ c= dom ((g.x)(#)f) by A27;
then ].x,x0.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A38,XBOOLE_1:19;
then
A40: ].x,x0.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A3,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A41: (g.x)(#)f is_differentiable_on ].x,x0.[ by A39,FDIFF_1:20;
g is_differentiable_on ].x,x0.[ by A4,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A42: (f.x)(#)g is_differentiable_on ].x,x0.[ by A38,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A22,A31,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A33,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A36,VALUED_1:def 5
.= 0;
then consider t such that
A43: t in ].x,x0.[ and
A44: diff(f1,t)=0 by A17,A25,A41,A40,A42,A22,A35,FDIFF_1:19,ROLLE:1;
A45: (g.x)(#)f is_differentiable_in t by A41,A43,FDIFF_1:9;
A46: f is_differentiable_in t by A3,A27,A43,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A42,A43,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A44,A45,FDIFF_1:14;
then
A47: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A46,FDIFF_1:15;
take t;
A48: t in [.x,x0.] by A26,A43;
[.x,x0.]\{x0} c= N\{x0} by A20,XBOOLE_1:33;
then
A49: [.x,x0.]\{x0} c= dom(f/g) by A5;
then [.x,x0.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x,x0.]\{x0} c= dom g\g"{0} by A15;
then
A50: x in dom g & not x in g"{0} by A37,XBOOLE_0:def 5;
A51: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A50,FUNCT_1:def 7;
end;
A52: [.x,x0.] c= dom ((f`|N)/(g`|N)) by A6,A20;
then [.x,x0.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x,x0.] c= dom (g`|N)\(g`|N)"{0} by A14;
then
A53: t in dom (g`|N) & not t in (g`|N)"{0} by A48,XBOOLE_0:def 5;
A54: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A20,A48,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A53,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A27,A43,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A47,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A51,A54,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A49,A37,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A20,A48,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A20,A48,FDIFF_1:def 7;
hence thesis by A43,A52,A48,RFUNCT_1:def 1;
end;
A55: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
left_open_halfline(x0) holds (f/g)/*a is divergent_to-infty
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A56: a is convergent and
A57: lim a = x0 and
A58: rng a c= dom (f/g) /\ left_open_halfline(x0);
consider k such that
A59: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A56,A57,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].a1.$1,x0.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A60: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in left_open_halfline(x0) by A58,XBOOLE_0:def 4;
then a.(n+k) in {g1:g1<x0} by XXREAL_1:229;
then ex g1 st a.(n+k)=g1 & g1<x0;
hence a1.n<x0 by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence x0-r<a1.n by A59;
end;
A61: for n ex c be Element of REAL st X[n,c]
proof
let n;
A62: rng a1 c= rng a by VALUED_0:21;
x0-r<a1.n & a1.n<x0 by A60;
then consider c such that
A63: c in ].a1.n,x0.[ and
A64: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A11;
take c;
A65: dom (f/g) /\ left_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A58;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A64,A62,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A58,A63,A65,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A66: for n holds X[n,b.n] from FUNCT_2:sch 3(A61);
A67: now
let n be Nat;
A68: n in NAT by ORDINAL1:def 12;
b.n in ].a1.n,x0.[ by A66,A68;
then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
hence a1.n<=b.n & b.n<= d.n by SEQ_1:57;
end;
A69: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
A70: x0<x0+r by A9,XREAL_1:29;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A70;
then
A71: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A72: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A73: x=b.n by FUNCT_2:113;
a1.n<x0 by A60;
then
A74: a1.n<x0+r by A70,XXREAL_0:2;
x0-r<a1.n by A60;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A74;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A71,
XXREAL_1:25,XXREAL_2:def 12;
then ].a1.n,x0.[ c= ].x0-r,x0+r.[;
then
A75: ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A76: x in ].a1.n,x0.[ by A66,A73;
then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1 = x & a1.n<g1 & g1<x0;
then not x in {x0} by TARSKI:def 1;
hence thesis by A76,A75,XBOOLE_0:def 5;
end;
A77: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A78: now
let n be Nat;
A79: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A66,A79;
hence (((f/g)/*a)^\k).n <= (((f`|N)/(g`|N))/*b).n by A72,A77,FUNCT_2:108
,XBOOLE_1:1,A79;
end;
lim a1=x0 by A56,A57,SEQ_4:20;
then b is convergent & lim b=x0 by A56,A69,A67,SEQ_2:19,20;
then ((f`|N)/(g`|N))/*b is divergent_to-infty by A8,A72,LIMFUNC3:def 3;
then ((f/g)/*a)^\k is divergent_to-infty by A78,LIMFUNC1:43;
hence thesis by LIMFUNC1:7;
end;
A80: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom (f/g)
& g2<r2 & x0<g2 & g2 in dom (f/g) by A5,Th4;
then for r1 st r1<x0 ex t st r1<t & t<x0 & t in dom (f/g) by LIMFUNC3:8;
then
A81: f/g is_left_divergent_to-infty_in x0 by A55,LIMFUNC2:def 3;
A82: for x st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|N)/(g`|N)). c
proof
A83: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A84: x0-r<x0 by A9,XREAL_1:44;
x0+0<x0+r by A9,XREAL_1:8;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A84;
then
A85: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
let x such that
A86: x0<x and
A87: x<x0+r;
x0-r<x by A86,A84,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A87;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A88: [.x0,x.] c= N by A10,A85,XXREAL_2:def 12;
then
A89: [.x0,x.] c= dom f & [.x0,x.] c= dom g by A1,A2;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x0,x.] is continuous by A88,FCONT_1:16;
then
A90: ((f.x)(#)g)|[.x0,x.] is continuous by A2,A88,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x0,x.] is continuous by A88,FCONT_1:16;
then
A91: ((g.x)(#)f)|[.x0,x.] is continuous by A1,A88,FCONT_1:20,XBOOLE_1:1;
A92: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A93: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
then [.x0,x.] c= dom((f.x)(#)g - (g.x)(#)f) by A89,XBOOLE_1:19;
then
A94: ((f.x)(#)g - (g.x)(#)f)|[.x0,x.] is continuous by A92,A93,A91,A90,
FCONT_1:18;
A95: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then
A96: ].x0,x.[ c= N by A88;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A97: ].x0,x.[ c= dom ((f.x)(#)g) by A96;
g is_differentiable_on ].x0,x.[ by A4,A88,A95,FDIFF_1:26,XBOOLE_1:1;
then
A98: (f.x)(#)g is_differentiable_on ].x0,x.[ by A97,FDIFF_1:20;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A99: ].x0,x.[ c= dom ((g.x)(#)f) by A96;
then ].x0,x.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A97,XBOOLE_1:19;
then
A100: ].x0,x.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A3,A88,A95,FDIFF_1:26,XBOOLE_1:1;
then
A101: (g.x)(#)f is_differentiable_on ].x0,x.[ by A99,FDIFF_1:20;
set f1 = (f.x)(#)g - (g.x)(#)f;
A102: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
then
A103: [.x0,x.] c= dom f1 by A89,XBOOLE_1:19;
A104: x in [.x0,x.] by A86,XXREAL_1:1;
then x in dom f1 by A103;
then
A105: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A106: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A107: x0 in [.x0,x.] by A86,XXREAL_1:1;
then x0 in dom f1 by A103;
then
A108: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A109: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A110: x in dom ((g.x)(#)f) by A105,XBOOLE_0:def 4;
A111: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A103,A104,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A106,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A110,VALUED_1:def 5
.= 0;
A112: x0 in dom ((g.x)(#)f) by A108,XBOOLE_0:def 4;
not x in {x0} by A86,TARSKI:def 1;
then
A113: x in [.x0,x.]\{x0} by A104,XBOOLE_0:def 5;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A103,A107,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A109,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A112,VALUED_1:def 5
.= 0;
then consider t such that
A114: t in ].x0,x.[ and
A115: diff(f1,t)=0 by A86,A94,A101,A100,A98,A103,A111,FDIFF_1:19,ROLLE:1;
A116: (g.x)(#)f is_differentiable_in t by A101,A114,FDIFF_1:9;
A117: f is_differentiable_in t by A3,A96,A114,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A98,A114,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A115,A116,FDIFF_1:14;
then
A118: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A117,FDIFF_1:15;
take t;
A119: t in [.x0,x.] by A95,A114;
[.x0,x.]\{x0} c= N\{x0} by A88,XBOOLE_1:33;
then
A120: [.x0,x.]\{x0} c= dom(f/g) by A5;
then [.x0,x.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x0,x.]\{x0} c= dom g\g"{0} by A102;
then
A121: x in dom g & not x in g"{0} by A113,XBOOLE_0:def 5;
A122: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A121,FUNCT_1:def 7;
end;
A123: [.x0,x.] c= dom ((f`|N)/(g`|N)) by A6,A88;
then [.x0,x.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x0,x.] c= dom (g`|N)\(g`|N)"{0} by A83;
then
A124: t in dom (g`|N) & not t in (g`|N)"{0} by A119,XBOOLE_0:def 5;
A125: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A88,A119,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A124,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A96,A114,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A118,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A122,A125,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A120,A113,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A88,A119,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A88,A119,FDIFF_1:def 7;
hence thesis by A114,A123,A119,RFUNCT_1:def 1;
end;
A126: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
right_open_halfline(x0) holds (f/g)/*a is divergent_to-infty
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A127: a is convergent and
A128: lim a = x0 and
A129: rng a c= dom (f/g) /\ right_open_halfline(x0);
consider k such that
A130: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A127,A128,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].x0,a1.$1.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A131: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in right_open_halfline(x0) by A129,XBOOLE_0:def 4;
then a.(n+k) in {g1:x0<g1} by XXREAL_1:230;
then ex g1 st a.(n+k)=g1 & x0<g1;
hence x0<a1.n by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence a1.n<x0+r by A130;
end;
A132: for n ex c be Element of REAL st X[n,c]
proof
let n;
A133: rng a1 c= rng a by VALUED_0:21;
x0<a1.n & a1.n<x0+r by A131;
then consider c such that
A134: c in ].x0,a1.n.[ and
A135: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A82;
take c;
A136: dom (f/g) /\ right_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A129;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A135,A133,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A129,A134,A136,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A137: for n holds X[n,b.n] from FUNCT_2:sch 3(A132);
A138: now
let n be Nat;
A139: n in NAT by ORDINAL1:def 12;
b.n in ].x0,a1.n.[ by A137,A139;
then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
hence d.n<=b.n & b.n<=a1.n by SEQ_1:57;
end;
A140: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
A141: x0-r<x0 by A9,XREAL_1:44;
x0<x0+r by A9,XREAL_1:29;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A141;
then
A142: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A143: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A144: x=b.n by FUNCT_2:113;
x0<a1.n by A131;
then
A145: x0-r<a1.n by A141,XXREAL_0:2;
a1.n<x0+r by A131;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A145;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A142,
XXREAL_1:25,XXREAL_2:def 12;
then ].x0,a1.n.[ c= ].x0-r,x0+r.[;
then
A146: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A147: x in ].x0,a1.n.[ by A137,A144;
then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1 = x & x0<g1 & g1<a1.n;
then not x in {x0} by TARSKI:def 1;
hence thesis by A147,A146,XBOOLE_0:def 5;
end;
A148: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A149: now
let n be Nat;
A150: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A137,A150;
hence (((f/g)/*a)^\k).n <= (((f`|N)/(g`|N))/*b).n by A143,A148,
FUNCT_2:108,XBOOLE_1:1,A150;
end;
lim a1=x0 by A127,A128,SEQ_4:20;
then b is convergent & lim b=x0 by A127,A140,A138,SEQ_2:19,20;
then ((f`|N)/(g`|N))/*b is divergent_to-infty by A8,A143,LIMFUNC3:def 3;
then ((f/g)/*a)^\k is divergent_to-infty by A149,LIMFUNC1:43;
hence thesis by LIMFUNC1:7;
end;
for r1 st x0<r1 ex t st t<r1 & x0<t & t in dom (f/g) by A80,LIMFUNC3:8;
then f/g is_right_divergent_to-infty_in x0 by A126,LIMFUNC2:def 6;
hence thesis by A81,LIMFUNC3:13;
end;
theorem
x0 in dom f /\ dom g & (ex r st r>0 & [.x0,x0+r.] c= dom f & [.x0,x0+r
.] c= dom g & f is_differentiable_on ].x0,x0+r.[ & g is_differentiable_on ].x0,
x0+r.[ & ].x0,x0+r.[ c= dom (f/g) & [.x0,x0+r.] c= dom ((f`|(].x0,x0+r.[))/(g`|
(].x0,x0+r.[))) & f.x0 = 0 & g.x0 = 0 & f is_continuous_in x0 & g
is_continuous_in x0 & (f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))
is_right_convergent_in x0) implies f/g is_right_convergent_in x0 & ex r st r>0
& lim_right(f/g,x0) = lim_right(((f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))),x0)
proof
assume
A1: x0 in dom f /\ dom g;
given r such that
A2: r>0 and
A3: [.x0,x0+r.] c= dom f and
A4: [.x0,x0+r.] c= dom g and
A5: f is_differentiable_on ].x0,x0+r.[ and
A6: g is_differentiable_on ].x0,x0+r.[ and
A7: ].x0,x0+r.[ c= dom (f/g) and
A8: [.x0,x0+r.] c= dom ((f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))) and
A9: f.x0 = 0 & g.x0 = 0 and
A10: f is_continuous_in x0 and
A11: g is_continuous_in x0 and
A12: (f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[)) is_right_convergent_in x0;
A13: ].x0,x0+r.[ c= [.x0,x0+r.] by XXREAL_1:25;
then
A14: ].x0,x0+r.[ c= dom g by A4;
A15: ].x0,x0+r.[ c= dom f by A3,A13;
A16: for x st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|].x0,x0+r.[
)/(g`|].x0,x0+r.[)).c
proof
let x;
assume that
A17: x0<x and
A18: x<x0+r;
set f1 = (f.x)(#)g - (g.x)(#)f;
A19: dom((g.x)(#)f) = dom f by VALUED_1:def 5;
A20: dom((f.x)(#)g) = dom g by VALUED_1:def 5;
then
A21: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by A19,VALUED_1:12;
A22: [.x0,x.] c= [.x0,x0+r.]
proof
let y be object;
assume
A23: y in [.x0,x.];
then reconsider y as Real;
y <= x by A23,XXREAL_1:1;
then
A24: y <= x0+r by A18,XXREAL_0:2;
x0 <= y by A23,XXREAL_1:1;
hence thesis by A24,XXREAL_1:1;
end;
then
A25: [.x0,x.] c= dom f & [.x0,x.] c= dom g by A3,A4;
then
A26: [.x0,x.] c= dom f1 by A21,XBOOLE_1:19;
A27: x in [.x0,x.] by A17,XXREAL_1:1;
then x in dom f1 by A26;
then
A28: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A29: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A30: x in dom ((g.x)(#)f) by A28,XBOOLE_0:def 4;
A31: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A26,A27,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A29,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A30,VALUED_1:def 5
.= 0;
A32: ].x0,x0+r.[ c= dom f by A3,A13;
not x in {x0} by A17,TARSKI:def 1;
then
A33: x in [.x0,x.]\{x0} by A27,XBOOLE_0:def 5;
x in {g1:x0<g1 & g1<x0+r} by A17,A18;
then
A34: x in ].x0,x0+r.[ by RCOMP_1:def 2;
A35: x0 in [.x0,x.] by A17,XXREAL_1:1;
then x0 in dom f1 by A26;
then
A36: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A37: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A38: [.x0,x.] c= dom((f.x)(#)g - (g.x)(#)f) by A25,A21,XBOOLE_1:19;
A39: x0 in dom ((g.x)(#)f) by A36,XBOOLE_0:def 4;
A40: ].x0,x0+r.[ c= dom g by A4,A13;
A41: ].x0,x.[ c= ].x0,x0+r.[
proof
let y be object;
assume y in ].x0,x.[;
then y in {g2:x0<g2 & g2<x} by RCOMP_1:def 2;
then consider g2 such that
A42: g2=y & x0<g2 and
A43: g2<x;
g2<x0+r by A18,A43,XXREAL_0:2;
then y in {g3:x0<g3 & g3<x0+r} by A42;
hence thesis by RCOMP_1:def 2;
end;
then
A44: ].x0,x.[ c= dom ((f.x)(#)g) by A14,A20;
x0 in dom f by A1,XBOOLE_0:def 4;
then
A45: {x0,x} c= dom f by A34,A32,ZFMISC_1:32;
].x0,x.[ c= dom f by A41,A32;
then ].x0,x.[ \/ {x0,x} c= dom f by A45,XBOOLE_1:8;
then
A46: [.x0,x.] c= dom f by A17,XXREAL_1:128;
x0 in dom g by A1,XBOOLE_0:def 4;
then
A47: {x0,x} c= dom g by A34,A40,ZFMISC_1:32;
].x0,x.[ c= dom g by A41,A40;
then ].x0,x.[ \/ {x0,x} c= dom g by A47,XBOOLE_1:8;
then
A48: [.x0,x.] c= dom g by A17,XXREAL_1:128;
g is_differentiable_in x by A6,A34,FDIFF_1:9;
then
A49: g is_continuous_in x by FDIFF_1:24;
for s st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.]
holds g/*s is convergent & g.(lim s) = lim (g/*s)
proof
let s such that
A50: rng s c= [.x0,x.] and
A51: s is convergent and
A52: lim s in [.x0,x.];
set z = lim s;
A53: rng s c= dom g by A48,A50;
A54: z in ].x0,x.[ \/ {x0,x} by A17,A52,XXREAL_1:128;
now
per cases by A54,XBOOLE_0:def 3;
suppose
z in ].x0,x.[;
then g is_differentiable_in z by A6,A41,FDIFF_1:9;
then g is_continuous_in z by FDIFF_1:24;
hence thesis by A51,A53,FCONT_1:def 1;
end;
suppose
A55: z in {x0,x};
now
per cases by A55,TARSKI:def 2;
suppose
z = x0;
hence thesis by A11,A51,A53,FCONT_1:def 1;
end;
suppose
z = x;
hence thesis by A49,A51,A53,FCONT_1:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then g|[.x0,x.] is continuous by A48,FCONT_1:13;
then
A56: ((f.x)(#)g)|[.x0,x.] is continuous by A4,A22,FCONT_1:20,XBOOLE_1:1;
f is_differentiable_in x by A5,A34,FDIFF_1:9;
then
A57: f is_continuous_in x by FDIFF_1:24;
for s st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.]
holds f/*s is convergent & f.(lim s) = lim (f/*s)
proof
let s;
assume that
A58: rng s c= [.x0,x.] and
A59: s is convergent and
A60: lim s in [.x0,x.];
set z = lim s;
A61: rng s c= dom f by A46,A58;
A62: z in ].x0,x.[ \/ {x0,x} by A17,A60,XXREAL_1:128;
now
per cases by A62,XBOOLE_0:def 3;
suppose
z in ].x0,x.[;
then f is_differentiable_in z by A5,A41,FDIFF_1:9;
then f is_continuous_in z by FDIFF_1:24;
hence thesis by A59,A61,FCONT_1:def 1;
end;
suppose
A63: z in {x0,x};
now
per cases by A63,TARSKI:def 2;
suppose
z = x0;
hence thesis by A10,A59,A61,FCONT_1:def 1;
end;
suppose
z = x;
hence thesis by A57,A59,A61,FCONT_1:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then f|[.x0,x.] is continuous by A46,FCONT_1:13;
then ((g.x)(#)f)|[.x0,x.] is continuous by A3,A22,FCONT_1:20,XBOOLE_1:1;
then
A64: ((f.x)(#)g - (g.x)(#)f)|[.x0,x.] is continuous by A20,A19,A21,A38,A56,
FCONT_1:18;
g is_differentiable_on ].x0,x.[ by A6,A41,FDIFF_1:26;
then
A65: (f.x)(#)g is_differentiable_on ].x0,x.[ by A44,FDIFF_1:20;
A66: ].x0,x.[ c= dom ((g.x)(#)f) by A15,A41,A19;
then ].x0,x.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A44,XBOOLE_1:19;
then
A67: ].x0,x.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A5,A41,FDIFF_1:26;
then
A68: (g.x)(#)f is_differentiable_on ].x0,x.[ by A66,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A26,A35,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A37,VALUED_1:def 5
.= 0 - (g.x)*0 by A9,A39,VALUED_1:def 5
.= 0;
then consider t such that
A69: t in ].x0,x.[ and
A70: diff(f1,t)=0 by A17,A64,A68,A67,A65,A26,A31,FDIFF_1:19,ROLLE:1;
A71: (g.x)(#)f is_differentiable_in t by A68,A69,FDIFF_1:9;
A72: f is_differentiable_in t by A5,A41,A69,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A65,A69,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A70,A71,FDIFF_1:14;
then
A73: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A72,FDIFF_1:15;
A74: dom (f`|].x0,x0+r.[) /\ (dom (g`|].x0,x0+r.[) \ (g`|].x0,x0+r.[)"{0}
) c= dom (g`|].x0,x0+r.[)\(g`|].x0,x0+r.[)"{0} by XBOOLE_1:17;
A75: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
now
let y be object;
assume
A76: y in [.x0,x.]\{x0};
then y in [.x0,x.] by XBOOLE_0:def 5;
then y in {g4: x0<=g4 & g4<=x} by RCOMP_1:def 1;
then consider g4 such that
A77: g4=y and
A78: x0<=g4 and
A79: g4<=x;
not y in {x0} by A76,XBOOLE_0:def 5;
then x0<>g4 by A77,TARSKI:def 1;
then
A80: x0<g4 by A78,XXREAL_0:1;
g4<x0+r by A18,A79,XXREAL_0:2;
then y in {g5: x0<g5 & g5<x0+r} by A77,A80;
hence y in ].x0,x0+r.[ by RCOMP_1:def 2;
end;
then [.x0,x.]\{x0} c= ].x0,x0+r.[;
then
A81: [.x0,x.]\{x0} c= dom(f/g) by A7;
then [.x0,x.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x0,x.]\{x0} c= dom g\g"{0} by A75;
then
A82: x in dom g & not x in g"{0} by A33,XBOOLE_0:def 5;
A83: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A82,FUNCT_1:def 7;
end;
take t;
].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then
A84: t in [.x0,x.] by A69;
x0<=x0+r by A2,XREAL_1:29;
then x0 in {g6: x0<=g6 & g6<=x0+r};
then ].x0,x0+r.[ c= [.x0,x0+r.] & x0 in [.x0,x0+r.] by RCOMP_1:def 1
,XXREAL_1:25;
then [.x0,x.] c= [.x0,x0+r.] by A34,XXREAL_2:def 12;
then
A85: [.x0,x.] c= dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) by A8;
then [.x0,x.] c= dom (f`|].x0,x0+r.[) /\ (dom (g`|].x0,x0+r.[)\(g`|].x0,
x0+r.[)"{0}) by RFUNCT_1:def 1;
then [.x0,x.] c= dom (g`|].x0,x0+r.[)\(g`|].x0,x0+r.[)"{0} by A74;
then
A86: t in dom (g`|].x0,x0+r.[) & not t in (g`|].x0,x0+r.[)"{0} by A84,
XBOOLE_0:def 5;
A87: now
assume diff(g,t)=0;
then (g`|].x0,x0+r.[).t=0 by A6,A41,A69,FDIFF_1:def 7;
then (g`|].x0,x0+r.[).t in {0} by TARSKI:def 1;
hence contradiction by A86,FUNCT_1:def 7;
end;
g is_differentiable_in t by A6,A41,A69,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A73,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A83,A87,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A81,A33,RFUNCT_1:def 1;
then (f/g).x = ((f`|].x0,x0+r.[).t)*diff(g,t)" by A5,A41,A69,FDIFF_1:def 7;
then (f/g).x = ((f`|].x0,x0+r.[).t)*((g`|].x0,x0+r.[).t)" by A6,A41,A69,
FDIFF_1:def 7;
hence thesis by A69,A85,A84,RFUNCT_1:def 1;
end;
A88: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
right_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) =
lim_right(((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)),x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A89: a is convergent and
A90: lim a = x0 and
A91: rng a c= dom (f/g) /\ right_open_halfline(x0);
consider k such that
A92: for n st k<=n holds x0-r<a.n & a.n<x0+r by A2,A89,A90,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].x0,a1.$1.[ & (((f/g)/*
a)^\k).$1=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).$2;
A93: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in right_open_halfline(x0) by A91,XBOOLE_0:def 4;
then a.(n+k) in {g1:x0<g1} by XXREAL_1:230;
then ex g1 st a.(n+k)=g1 & x0<g1;
hence x0<a1.n by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence a1.n<x0+r by A92;
end;
A94: for n ex c be Element of REAL st X[n,c]
proof
let n;
A95: rng a1 c= rng a by VALUED_0:21;
x0<a1.n & a1.n<x0+r by A93;
then consider c such that
A96: c in ].x0,a1.n.[ and
A97: (f/g).(a1.n)=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).c by A16;
take c;
A98: dom (f/g) /\ right_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A91;
then ((f/g)/*(a^\k)).n=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).c by A97,A95,
FUNCT_2:108,XBOOLE_1:1;
hence thesis by A91,A96,A98,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A99: for n holds X[n,b.n] from FUNCT_2:sch 3(A94);
A100: rng b c= dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) /\
right_open_halfline(x0)
proof
let x be object;
assume x in rng b;
then consider n such that
A101: x=b.n by FUNCT_2:113;
x0<=x0+r by A2,XREAL_1:29;
then x0 in {g3: x0<=g3 & g3<=x0+r};
then
A102: x0 in [.x0,x0+r.] by RCOMP_1:def 1;
x0<a1.n & a1.n<x0+r by A93;
then a1.n in {g4: x0<=g4 & g4<=x0+r};
then a1.n in [.x0,x0+r.] by RCOMP_1:def 1;
then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= [.x0,x0+r.] by A102,
XXREAL_1:25,XXREAL_2:def 12;
then ].x0,a1.n.[ c= [.x0,x0+r.];
then
A103: ].x0,a1.n.[ c= dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) by A8;
A104: x in ].x0,a1.n.[ by A99,A101;
then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1 = x & x0<g1 & g1<a1.n;
then x in {g2: x0<g2};
then x in right_open_halfline(x0) by XXREAL_1:230;
hence thesis by A104,A103,XBOOLE_0:def 4;
end;
A105: now
let n be Nat;
A106: n in NAT by ORDINAL1:def 12;
b.n in ].x0,a1.n.[ by A99,A106;
then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
hence d.n<=b.n & b.n<=a1.n by SEQ_1:57;
end;
A107: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A89,A90,SEQ_4:20;
then
A108: b is convergent & lim b=x0 by A89,A107,A105,SEQ_2:19,20;
A109: dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) /\ right_open_halfline(x0)
c= dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) by XBOOLE_1:17;
A110: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A111: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).(b.n) by A99,A111;
hence (((f/g)/*a)^\k).n = (((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[))/*b).n by
A100,A109,FUNCT_2:108,XBOOLE_1:1,A111;
end;
lim_right(((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)),x0)= lim_right(((f`|].
x0,x0+r.[)/(g`|].x0,x0+r.[)),x0);
then
A112: ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[))/*b is convergent by A12,A108,A100,
LIMFUNC2:def 8;
then
A113: ((f/g)/*a)^\k is convergent by A110,SEQ_4:18;
lim (((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[))/*b) = lim_right(((f`|].x0,
x0+ r.[)/(g`|].x0,x0+r.[)),x0) by A12,A108,A100,LIMFUNC2:def 8;
then lim (((f/g)/*a)^\k) = lim_right(((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)),
x0) by A112,A110,SEQ_4:19;
hence thesis by A113,SEQ_4:21,22;
end;
A114: for r1 st x0<r1 ex t st t<r1 & x0<t & t in dom (f/g) by A2,A7,LIMFUNC2:4;
hence f/g is_right_convergent_in x0 by A88,Th2;
take r;
thus r>0 by A2;
thus thesis by A114,A88,Th2;
end;
theorem
x0 in dom f /\ dom g & (ex r st r>0 & [.x0-r,x0.] c= dom f & [.x0-r,x0
.] c= dom g & f is_differentiable_on ].x0-r,x0.[ & g is_differentiable_on ].x0-
r,x0.[ & ].x0-r,x0.[ c= dom (f/g) & [.x0-r,x0.] c= dom ((f`|(].x0-r,x0.[))/(g`|
(].x0-r,x0.[))) & f.x0 = 0 & g.x0 = 0 & f is_continuous_in x0 & g
is_continuous_in x0 & (f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))
is_left_convergent_in x0) implies f/g is_left_convergent_in x0 & ex r st r>0 &
lim_left(f/g,x0) = lim_left(((f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))),x0)
proof
assume
A1: x0 in dom f /\ dom g;
given r such that
A2: r>0 and
A3: [.x0-r,x0.] c= dom f and
A4: [.x0-r,x0.] c= dom g and
A5: f is_differentiable_on ].x0-r,x0.[ and
A6: g is_differentiable_on ].x0-r,x0.[ and
A7: ].x0-r,x0.[ c= dom (f/g) and
A8: [.x0-r,x0.] c= dom ((f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))) and
A9: f.x0 = 0 & g.x0 = 0 and
A10: f is_continuous_in x0 and
A11: g is_continuous_in x0 and
A12: (f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[)) is_left_convergent_in x0;
A13: ].x0-r,x0.[ c= [.x0-r,x0.] by XXREAL_1:25;
then
A14: ].x0-r,x0.[ c= dom g by A4;
A15: ].x0-r,x0.[ c= dom f by A3,A13;
A16: for x st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|].x0-r,x0.[
)/(g`|].x0-r,x0.[)).c
proof
let x;
assume that
A17: x0-r<x and
A18: x<x0;
x in {g1:x0-r<g1 & g1<x0} by A17,A18;
then
A19: x in ].x0-r,x0.[ by RCOMP_1:def 2;
].x0-r,x0.[ c= dom f & x0 in dom f by A1,A3,A13,XBOOLE_0:def 4;
then
A20: {x,x0} c= dom f by A19,ZFMISC_1:32;
A21: ].x,x0.[ c= ].x0-r,x0.[
proof
let y be object;
assume y in ].x,x0.[;
then y in {g2:x<g2 & g2<x0} by RCOMP_1:def 2;
then consider g2 such that
A22: g2=y and
A23: x<g2 and
A24: g2<x0;
x0-r<g2 by A17,A23,XXREAL_0:2;
then y in {g3:x0-r<g3 & g3<x0} by A22,A24;
hence thesis by RCOMP_1:def 2;
end;
then ].x,x0.[ c= dom f by A15;
then ].x,x0.[ \/ {x,x0} c= dom f by A20,XBOOLE_1:8;
then
A25: [.x,x0.] c= dom f by A18,XXREAL_1:128;
].x0-r,x0.[ c= dom ((f.x)(#)g) by A14,VALUED_1:def 5;
then
A26: ].x,x0.[ c= dom ((f.x)(#)g) by A21;
].x0-r,x0.[ c= dom ((g.x)(#)f) by A15,VALUED_1:def 5;
then
A27: ].x,x0.[ c= dom ((g.x)(#)f) by A21;
then ].x,x0.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A26,XBOOLE_1:19;
then
A28: ].x,x0.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A5,A21,FDIFF_1:26;
then
A29: (g.x)(#)f is_differentiable_on ].x,x0.[ by A27,FDIFF_1:20;
].x0-r,x0.[ c= dom g & x0 in dom g by A1,A4,A13,XBOOLE_0:def 4;
then
A30: {x,x0} c= dom g by A19,ZFMISC_1:32;
set f1 = (f.x)(#)g - (g.x)(#)f;
A31: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A32: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
A33: [.x,x0.] c= [.x0-r,x0.]
proof
let y be object;
assume
A34: y in [.x,x0.];
then reconsider y as Real;
x <= y by A34,XXREAL_1:1;
then
A35: x0-r <= y by A17,XXREAL_0:2;
y <= x0 by A34,XXREAL_1:1;
hence thesis by A35,XXREAL_1:1;
end;
then
A36: [.x,x0.] c= dom f & [.x,x0.] c= dom g by A3,A4;
then
A37: [.x,x0.] c= dom f1 by A32,XBOOLE_1:19;
A38: x in [.x,x0.] by A18,XXREAL_1:1;
then x in dom f1 by A37;
then
A39: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A40: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A41: x0 in [.x,x0.] by A18,XXREAL_1:1;
then x0 in dom f1 by A37;
then
A42: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A43: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A44: x in dom ((g.x)(#)f) by A39,XBOOLE_0:def 4;
A45: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A37,A38,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A40,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A44,VALUED_1:def 5
.= 0;
A46: x0 in dom ((g.x)(#)f) by A42,XBOOLE_0:def 4;
not x in {x0} by A18,TARSKI:def 1;
then
A47: x in [.x,x0.]\{x0} by A38,XBOOLE_0:def 5;
].x,x0.[ c= dom g by A14,A21;
then ].x,x0.[ \/ {x,x0} c= dom g by A30,XBOOLE_1:8;
then
A48: [.x,x0.] c= dom g by A18,XXREAL_1:128;
g is_differentiable_in x by A6,A19,FDIFF_1:9;
then
A49: g is_continuous_in x by FDIFF_1:24;
for s st rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.]
holds g/*s is convergent & g.(lim s) = lim (g/*s)
proof
let s such that
A50: rng s c= [.x,x0.] and
A51: s is convergent and
A52: lim s in [.x,x0.];
set z = lim s;
A53: rng s c= dom g by A48,A50;
A54: z in ].x,x0.[ \/ {x,x0} by A18,A52,XXREAL_1:128;
now
per cases by A54,XBOOLE_0:def 3;
suppose
z in ].x,x0.[;
then g is_differentiable_in z by A6,A21,FDIFF_1:9;
then g is_continuous_in z by FDIFF_1:24;
hence thesis by A51,A53,FCONT_1:def 1;
end;
suppose
A55: z in {x,x0};
now
per cases by A55,TARSKI:def 2;
suppose
z = x0;
hence thesis by A11,A51,A53,FCONT_1:def 1;
end;
suppose
z = x;
hence thesis by A49,A51,A53,FCONT_1:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then g|[.x,x0.] is continuous by A48,FCONT_1:13;
then
A56: ((f.x)(#)g)|[.x,x0.] is continuous by A4,A33,FCONT_1:20,XBOOLE_1:1;
A57: [.x,x0.] c= dom((f.x)(#)g - (g.x)(#)f) by A36,A32,XBOOLE_1:19;
f is_differentiable_in x by A5,A19,FDIFF_1:9;
then
A58: f is_continuous_in x by FDIFF_1:24;
for s st rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.]
holds f/*s is convergent & f.(lim s) = lim (f/*s)
proof
let s;
assume that
A59: rng s c= [.x,x0.] and
A60: s is convergent and
A61: lim s in [.x,x0.];
set z = lim s;
A62: rng s c= dom f by A25,A59;
A63: z in ].x,x0.[ \/ {x,x0} by A18,A61,XXREAL_1:128;
now
per cases by A63,XBOOLE_0:def 3;
suppose
z in ].x,x0.[;
then f is_differentiable_in z by A5,A21,FDIFF_1:9;
then f is_continuous_in z by FDIFF_1:24;
hence thesis by A60,A62,FCONT_1:def 1;
end;
suppose
A64: z in {x,x0};
now
per cases by A64,TARSKI:def 2;
suppose
z = x0;
hence thesis by A10,A60,A62,FCONT_1:def 1;
end;
suppose
z = x;
hence thesis by A58,A60,A62,FCONT_1:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then f|[.x,x0.] is continuous by A25,FCONT_1:13;
then ((g.x)(#)f)|[.x,x0.] is continuous by A3,A33,FCONT_1:20,XBOOLE_1:1;
then
A65: ((f.x)(#)g - (g.x)(#)f)|[.x,x0.] is continuous by A31,A32,A57,A56,
FCONT_1:18;
g is_differentiable_on ].x,x0.[ by A6,A21,FDIFF_1:26;
then
A66: (f.x)(#)g is_differentiable_on ].x,x0.[ by A26,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A37,A41,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A43,VALUED_1:def 5
.= 0 - (g.x)*0 by A9,A46,VALUED_1:def 5
.= 0;
then consider t such that
A67: t in ].x,x0.[ and
A68: diff(f1,t)=0 by A18,A65,A29,A28,A66,A37,A45,FDIFF_1:19,ROLLE:1;
A69: (g.x)(#)f is_differentiable_in t by A29,A67,FDIFF_1:9;
A70: f is_differentiable_in t by A5,A21,A67,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A66,A67,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A68,A69,FDIFF_1:14;
then
A71: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A70,FDIFF_1:15;
A72: dom (f`|].x0-r,x0.[) /\ (dom (g`|].x0-r,x0.[) \ (g`|].x0-r,x0.[)"{0}
) c= dom (g`|].x0-r,x0.[)\(g`|].x0-r,x0.[)"{0} by XBOOLE_1:17;
A73: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
now
let y be object;
assume
A74: y in [.x,x0.]\{x0};
then y in [.x,x0.] by XBOOLE_0:def 5;
then y in {g4: x<=g4 & g4<=x0} by RCOMP_1:def 1;
then consider g4 such that
A75: g4=y and
A76: x<=g4 and
A77: g4<=x0;
not y in {x0} by A74,XBOOLE_0:def 5;
then x0<>g4 by A75,TARSKI:def 1;
then
A78: g4<x0 by A77,XXREAL_0:1;
x0-r<g4 by A17,A76,XXREAL_0:2;
then y in {g5: x0-r<g5 & g5<x0} by A75,A78;
hence y in ].x0-r,x0.[ by RCOMP_1:def 2;
end;
then [.x,x0.]\{x0} c= ].x0-r,x0.[;
then
A79: [.x,x0.]\{x0} c= dom(f/g) by A7;
then [.x,x0.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x,x0.]\{x0} c= dom g\g"{0} by A73;
then
A80: x in dom g & not x in g"{0} by A47,XBOOLE_0:def 5;
A81: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A80,FUNCT_1:def 7;
end;
take t;
].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then
A82: t in [.x,x0.] by A67;
x0-r<=x0 by A2,XREAL_1:44;
then x0 in {g6: x0-r<=g6 & g6<=x0};
then ].x0-r,x0.[ c= [.x0-r,x0.] & x0 in [.x0-r,x0.] by RCOMP_1:def 1
,XXREAL_1:25;
then [.x,x0.] c= [.x0-r,x0.] by A19,XXREAL_2:def 12;
then
A83: [.x,x0.] c= dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) by A8;
then [.x,x0.] c= dom (f`|].x0-r,x0.[) /\ (dom (g`|].x0-r,x0.[)\(g`|].x0-r
,x0.[)"{0}) by RFUNCT_1:def 1;
then [.x,x0.] c= dom (g`|].x0-r,x0.[)\(g`|].x0-r,x0.[)"{0} by A72;
then
A84: t in dom (g`|].x0-r,x0.[) & not t in (g`|].x0-r,x0.[)"{0} by A82,
XBOOLE_0:def 5;
A85: now
assume diff(g,t)=0;
then (g`|].x0-r,x0.[).t=0 by A6,A21,A67,FDIFF_1:def 7;
then (g`|].x0-r,x0.[).t in {0} by TARSKI:def 1;
hence contradiction by A84,FUNCT_1:def 7;
end;
g is_differentiable_in t by A6,A21,A67,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A71,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A81,A85,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A79,A47,RFUNCT_1:def 1;
then (f/g).x = ((f`|].x0-r,x0.[).t)*diff(g,t)" by A5,A21,A67,FDIFF_1:def 7;
then (f/g).x = ((f`|].x0-r,x0.[).t)*((g`|].x0-r,x0.[).t)" by A6,A21,A67,
FDIFF_1:def 7;
hence thesis by A67,A83,A82,RFUNCT_1:def 1;
end;
A86: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
left_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) = lim_left
(((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)),x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A87: a is convergent and
A88: lim a = x0 and
A89: rng a c= dom (f/g) /\ left_open_halfline(x0);
consider k such that
A90: for n st k<=n holds x0-r<a.n & a.n<x0+r by A2,A87,A88,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].a1.$1,x0.[ & (((f/g)/*
a)^\k).$1=((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).$2;
A91: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in left_open_halfline(x0) by A89,XBOOLE_0:def 4;
then a.(n+k) in {g1:g1<x0} by XXREAL_1:229;
then ex g1 st a.(n+k)=g1 & g1<x0;
hence a1.n<x0 by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence x0-r<a1.n by A90;
end;
A92: for n ex c be Element of REAL st X[n,c]
proof
let n;
A93: rng a1 c= rng a by VALUED_0:21;
x0-r<a1.n & a1.n<x0 by A91;
then consider c such that
A94: c in ].a1.n,x0.[ and
A95: (f/g).(a1.n)= ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).c by A16;
take c;
A96: dom (f/g) /\ left_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A89;
then ((f/g)/*(a^\k)).n=((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).c by A95,A93,
FUNCT_2:108,XBOOLE_1:1;
hence thesis by A89,A94,A96,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A97: for n holds X[n,b.n] from FUNCT_2:sch 3(A92);
A98: rng b c= dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) /\ left_open_halfline(x0)
proof
let x be object;
assume x in rng b;
then consider n such that
A99: x=b.n by FUNCT_2:113;
x0-r<=x0 by A2,XREAL_1:44;
then x0 in {g3: x0-r<=g3 & g3<=x0};
then
A100: x0 in [.x0-r,x0.] by RCOMP_1:def 1;
x0-r<a1.n & a1.n<x0 by A91;
then a1.n in {g4: x0-r<=g4 & g4<=x0};
then a1.n in [.x0-r,x0.] by RCOMP_1:def 1;
then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= [.x0-r,x0.] by A100,
XXREAL_1:25,XXREAL_2:def 12;
then ].a1.n,x0.[ c= [.x0-r,x0.];
then
A101: ].a1.n,x0.[ c= dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) by A8;
A102: x in ].a1.n,x0.[ by A97,A99;
then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1 = x & a1.n<g1 & g1<x0;
then x in {g2: g2<x0};
then x in left_open_halfline(x0) by XXREAL_1:229;
hence thesis by A102,A101,XBOOLE_0:def 4;
end;
A103: now
let n be Nat;
A104: n in NAT by ORDINAL1:def 12;
b.n in ].a1.n,x0.[ by A97,A104;
then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
hence a1.n<=b.n & b.n<=d.n by SEQ_1:57;
end;
A105: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A87,A88,SEQ_4:20;
then
A106: b is convergent & lim b=x0 by A87,A105,A103,SEQ_2:19,20;
A107: dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) /\ left_open_halfline(x0) c=
dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) by XBOOLE_1:17;
A108: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A109: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).(b.n) by A97,A109;
hence (((f/g)/*a)^\k).n = (((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[))/*b).n by
A98,A107,FUNCT_2:108,XBOOLE_1:1,A109;
end;
lim_left(((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)),x0)= lim_left(((f`|].x0
-r,x0.[)/(g`|].x0-r,x0.[)),x0);
then
A110: ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[))/*b is convergent by A12,A106,A98,
LIMFUNC2:def 7;
then
A111: ((f/g)/*a)^\k is convergent by A108,SEQ_4:18;
lim (((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[))/*b) = lim_left(((f`|].x0-r,
x0 .[)/(g`|].x0-r,x0.[)),x0) by A12,A106,A98,LIMFUNC2:def 7;
then lim (((f/g)/*a)^\k) = lim_left(((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)),
x0) by A110,A108,SEQ_4:19;
hence thesis by A111,SEQ_4:21,22;
end;
A112: for r1 st r1<x0 ex t st r1<t & t<x0 & t in dom (f/g) by A2,A7,LIMFUNC2:3;
hence f/g is_left_convergent_in x0 by A86,Th3;
take r;
thus r>0 by A2;
thus thesis by A112,A86,Th3;
end;
theorem
(ex N being Neighbourhood of x0 st N c= dom f & N c= dom g & f
is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f/g) & N
c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 & (f`|N)/(g`|N) is_convergent_in
x0) implies f/g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim(f/g
,x0) = lim(((f`|N)/(g`|N)),x0)
proof
given N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: N c= dom g and
A3: f is_differentiable_on N and
A4: g is_differentiable_on N and
A5: N \ {x0} c= dom (f/g) and
A6: N c= dom ((f`|N)/(g`|N)) and
A7: f.x0 = 0 & g.x0 = 0 and
A8: (f`|N)/(g`|N) is_convergent_in x0;
consider r be Real such that
A9: 0<r and
A10: N = ].x0-r,x0+r.[ by RCOMP_1:def 6;
A11: for x st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|N)/(g`|N)). c
proof
A12: x0-r<x0 by A9,XREAL_1:44;
x0+0<x0+r by A9,XREAL_1:8;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A12;
then
A13: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A14: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A15: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A16: x0<x and
A17: x<x0+r;
set f1 = (f.x)(#)g - (g.x)(#)f;
A18: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A19: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x0-r<x by A16,A12,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A17;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A20: [.x0,x.] c= N by A10,A13,XXREAL_2:def 12;
then
A21: [.x0,x.] c= dom f & [.x0,x.] c= dom g by A1,A2;
then
A22: [.x0,x.] c= dom f1 by A19,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x0,x.] is continuous by A20,FCONT_1:16;
then
A23: ((f.x)(#)g)|[.x0,x.] is continuous by A2,A20,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x0,x.] is continuous by A20,FCONT_1:16;
then
A24: ((g.x)(#)f)|[.x0,x.] is continuous by A1,A20,FCONT_1:20,XBOOLE_1:1;
[.x0,x.] c= dom((f.x)(#)g - (g.x)(#)f) by A21,A19,XBOOLE_1:19;
then
A25: ((f.x)(#)g - (g.x)(#)f)|[.x0,x.] is continuous by A18,A19,A24,A23,
FCONT_1:18;
A26: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then
A27: ].x0,x.[ c= N by A20;
A28: x in [.x0,x.] by A16,XXREAL_1:1;
then x in dom f1 by A22;
then
A29: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A30: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A31: x0 in [.x0,x.] by A16,XXREAL_1:1;
then x0 in dom f1 by A22;
then
A32: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A33: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A34: x in dom ((g.x)(#)f) by A29,XBOOLE_0:def 4;
A35: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A22,A28,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A30,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A34,VALUED_1:def 5
.= 0;
A36: x0 in dom ((g.x)(#)f) by A32,XBOOLE_0:def 4;
not x in {x0} by A16,TARSKI:def 1;
then
A37: x in [.x0,x.]\{x0} by A28,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A38: ].x0,x.[ c= dom ((f.x)(#)g) by A27;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A39: ].x0,x.[ c= dom ((g.x)(#)f) by A27;
then ].x0,x.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A38,XBOOLE_1:19;
then
A40: ].x0,x.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A3,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A41: (g.x)(#)f is_differentiable_on ].x0,x.[ by A39,FDIFF_1:20;
g is_differentiable_on ].x0,x.[ by A4,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A42: (f.x)(#)g is_differentiable_on ].x0,x.[ by A38,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A22,A31,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A33,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A36,VALUED_1:def 5
.= 0;
then consider t such that
A43: t in ].x0,x.[ and
A44: diff(f1,t)=0 by A16,A25,A41,A40,A42,A22,A35,FDIFF_1:19,ROLLE:1;
A45: (g.x)(#)f is_differentiable_in t by A41,A43,FDIFF_1:9;
A46: f is_differentiable_in t by A3,A27,A43,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A42,A43,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A44,A45,FDIFF_1:14;
then
A47: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A46,FDIFF_1:15;
take t;
A48: t in [.x0,x.] by A26,A43;
[.x0,x.]\{x0} c= N\{x0} by A20,XBOOLE_1:33;
then
A49: [.x0,x.]\{x0} c= dom(f/g) by A5;
then [.x0,x.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x0,x.]\{x0} c= dom g\g"{0} by A15;
then
A50: x in dom g & not x in g"{0} by A37,XBOOLE_0:def 5;
A51: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A50,FUNCT_1:def 7;
end;
A52: [.x0,x.] c= dom ((f`|N)/(g`|N)) by A6,A20;
then [.x0,x.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x0,x.] c= dom (g`|N)\(g`|N)"{0} by A14;
then
A53: t in dom (g`|N) & not t in (g`|N)"{0} by A48,XBOOLE_0:def 5;
A54: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A20,A48,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A53,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A27,A43,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A47,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A51,A54,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A49,A37,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A20,A48,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A20,A48,FDIFF_1:def 7;
hence thesis by A43,A52,A48,RFUNCT_1:def 1;
end;
A55: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
right_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) = lim(((f
`|N)/(g`|N)),x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A56: a is convergent and
A57: lim a = x0 and
A58: rng a c= dom (f/g) /\ right_open_halfline(x0);
consider k such that
A59: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A56,A57,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].x0,a1.$1.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A60: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in right_open_halfline(x0) by A58,XBOOLE_0:def 4;
then a.(n+k) in {g1:x0<g1} by XXREAL_1:230;
then ex g1 st a.(n+k)=g1 & x0<g1;
hence x0<a1.n by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence a1.n<x0+r by A59;
end;
A61: for n ex c be Element of REAL st X[n,c]
proof
let n;
A62: rng a1 c= rng a by VALUED_0:21;
x0<a1.n & a1.n<x0+r by A60;
then consider c such that
A63: c in ].x0,a1.n.[ and
A64: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A11;
take c;
A65: dom (f/g) /\ right_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A58;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A64,A62,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A58,A63,A65,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A66: for n holds X[n,b.n] from FUNCT_2:sch 3(A61);
A67: now
let n be Nat;
A68: n in NAT by ORDINAL1:def 12;
b.n in ].x0,a1.n.[ by A66,A68;
then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
hence d.n<=b.n & b.n<=a1.n by SEQ_1:57;
end;
A69: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A56,A57,SEQ_4:20;
then
A70: b is convergent & lim b=x0 by A56,A69,A67,SEQ_2:19,20;
A71: x0-r<x0 by A9,XREAL_1:44;
x0<x0+r by A9,XREAL_1:29;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A71;
then
A72: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A73: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A74: x=b.n by FUNCT_2:113;
x0<a1.n by A60;
then
A75: x0-r<a1.n by A71,XXREAL_0:2;
a1.n<x0+r by A60;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A75;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A72,
XXREAL_1:25,XXREAL_2:def 12;
then ].x0,a1.n.[ c= ].x0-r,x0+r.[;
then
A76: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A77: x in ].x0,a1.n.[ by A66,A74;
then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1 = x & x0<g1 & g1<a1.n;
then not x in {x0} by TARSKI:def 1;
hence thesis by A77,A76,XBOOLE_0:def 5;
end;
A78: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A79: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A80: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A66,A80;
hence (((f/g)/*a)^\k).n = (((f`|N)/(g`|N))/*b).n by A73,A78,FUNCT_2:108
,XBOOLE_1:1,A80;
end;
lim(((f`|N)/(g`|N)),x0)=lim(((f`|N)/(g`|N)),x0);
then
A81: ((f`|N)/(g`|N))/*b is convergent by A8,A70,A73,LIMFUNC3:def 4;
then
A82: ((f/g)/*a)^\k is convergent by A79,SEQ_4:18;
lim (((f`|N)/(g`|N))/*b) = lim(((f`|N)/(g`|N)),x0) by A8,A70,A73,
LIMFUNC3:def 4;
then lim (((f/g)/*a)^\k) = lim(((f`|N)/(g`|N)),x0) by A81,A79,SEQ_4:19;
hence thesis by A82,SEQ_4:21,22;
end;
A83: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom (f/g)
& g2<r2 & x0<g2 & g2 in dom (f/g) by A5,Th4;
then for r1 st x0<r1 ex t st t<r1 & x0<t & t in dom (f/g) by LIMFUNC3:8;
then
A84: f/g is_right_convergent_in x0 & lim_right(f/g,x0)=lim(((f`|N)/(g`|N ))
,x0) by A55,Th2;
A85: for x st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|N)/(g`|N)) .c
proof
A86: x0+0<x0+r by A9,XREAL_1:8;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A86;
then
A87: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A88: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A89: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A90: x0-r<x and
A91: x<x0;
set f1 = (f.x)(#)g - (g.x)(#)f;
A92: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A93: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x<x0+r by A91,A86,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A90;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A94: [.x,x0.] c= N by A10,A87,XXREAL_2:def 12;
then
A95: [.x,x0.] c= dom f & [.x,x0.] c= dom g by A1,A2;
then
A96: [.x,x0.] c= dom f1 by A93,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x,x0.] is continuous by A94,FCONT_1:16;
then
A97: ((f.x)(#)g)|[.x,x0.] is continuous by A2,A94,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x,x0.] is continuous by A94,FCONT_1:16;
then
A98: ((g.x)(#)f)|[.x,x0.] is continuous by A1,A94,FCONT_1:20,XBOOLE_1:1;
[.x,x0.] c= dom((f.x)(#)g - (g.x)(#)f) by A95,A93,XBOOLE_1:19;
then
A99: ((f.x)(#)g - (g.x)(#)f)|[.x,x0.] is continuous by A92,A93,A98,A97,
FCONT_1:18;
A100: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then
A101: ].x,x0.[ c= N by A94;
A102: x in [.x,x0.] by A91,XXREAL_1:1;
then x in dom f1 by A96;
then
A103: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A104: x in dom ((f.x) (#) g) by XBOOLE_0:def 4;
A105: x0 in [.x,x0.] by A91,XXREAL_1:1;
then x0 in dom f1 by A96;
then
A106: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A107: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A108: x in dom ((g.x)(#)f) by A103,XBOOLE_0:def 4;
A109: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A96,A102,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A104,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A108,VALUED_1:def 5
.= 0;
A110: x0 in dom ((g.x)(#)f) by A106,XBOOLE_0:def 4;
not x in {x0} by A91,TARSKI:def 1;
then
A111: x in [.x,x0.]\{x0} by A102,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A112: ].x,x0.[ c= dom ((f.x)(#)g) by A101;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A113: ].x,x0.[ c= dom ((g.x)(#)f) by A101;
then ].x,x0.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A112,XBOOLE_1:19;
then
A114: ].x,x0.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A3,A94,A100,FDIFF_1:26,XBOOLE_1:1;
then
A115: (g.x)(#)f is_differentiable_on ].x,x0.[ by A113,FDIFF_1:20;
g is_differentiable_on ].x,x0.[ by A4,A94,A100,FDIFF_1:26,XBOOLE_1:1;
then
A116: (f.x)(#)g is_differentiable_on ].x,x0.[ by A112,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A96,A105,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A107,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A110,VALUED_1:def 5
.= 0;
then consider t such that
A117: t in ].x,x0.[ and
A118: diff(f1,t)=0 by A91,A99,A115,A114,A116,A96,A109,FDIFF_1:19,ROLLE:1;
A119: (g.x)(#)f is_differentiable_in t by A115,A117,FDIFF_1:9;
A120: f is_differentiable_in t by A3,A101,A117,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A116,A117,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A118,A119,FDIFF_1:14;
then
A121: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A120,FDIFF_1:15;
take t;
A122: t in [.x,x0.] by A100,A117;
[.x,x0.]\{x0} c= N\{x0} by A94,XBOOLE_1:33;
then
A123: [.x,x0.]\{x0} c= dom(f/g) by A5;
then [.x,x0.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x,x0.]\{x0} c= dom g\g"{0} by A89;
then
A124: x in dom g & not x in g"{0} by A111,XBOOLE_0:def 5;
A125: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A124,FUNCT_1:def 7;
end;
A126: [.x,x0.] c= dom ((f`|N)/(g`|N)) by A6,A94;
then [.x,x0.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x,x0.] c= dom (g`|N)\(g`|N)"{0} by A88;
then
A127: t in dom (g`|N) & not t in (g`|N)"{0} by A122,XBOOLE_0:def 5;
A128: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A94,A122,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A127,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A101,A117,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A121,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A125,A128,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A123,A111,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A94,A122,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A94,A122,FDIFF_1:def 7;
hence thesis by A117,A126,A122,RFUNCT_1:def 1;
end;
A129: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
left_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) = lim(((f`|
N)/(g`|N)),x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A130: a is convergent and
A131: lim a = x0 and
A132: rng a c= dom (f/g) /\ left_open_halfline(x0);
consider k such that
A133: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A130,A131,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].a1.$1,x0.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A134: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in left_open_halfline(x0) by A132,XBOOLE_0:def 4;
then a.(n+k) in {g1:g1<x0} by XXREAL_1:229;
then ex g1 st a.(n+k)=g1 & g1<x0;
hence a1.n<x0 by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence x0-r<a1.n by A133;
end;
A135: for n ex c be Element of REAL st X[n,c]
proof
let n;
A136: rng a1 c= rng a by VALUED_0:21;
x0-r<a1.n & a1.n<x0 by A134;
then consider c such that
A137: c in ].a1.n,x0.[ and
A138: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A85;
take c;
A139: dom (f/g) /\ left_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A132;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A138,A136,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A132,A137,A139,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A140: for n holds X[n,b.n] from FUNCT_2:sch 3(A135);
A141: now
let n be Nat;
A142: n in NAT by ORDINAL1:def 12;
b.n in ].a1.n,x0.[ by A140,A142;
then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
hence a1.n<=b.n & b.n<= d.n by SEQ_1:57;
end;
A143: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A130,A131,SEQ_4:20;
then
A144: b is convergent & lim b=x0 by A130,A143,A141,SEQ_2:19,20;
A145: x0<x0+r by A9,XREAL_1:29;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A145;
then
A146: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A147: rng b c= dom ((f`|N)/(g`|N)) \{x0}
proof
let x be object;
assume x in rng b;
then consider n such that
A148: x=b.n by FUNCT_2:113;
a1.n<x0 by A134;
then
A149: a1.n<x0+r by A145,XXREAL_0:2;
x0-r<a1.n by A134;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A149;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A146,
XXREAL_1:25,XXREAL_2:def 12;
then ].a1.n,x0.[ c= ].x0-r,x0+r.[;
then
A150: ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A151: x in ].a1.n,x0.[ by A140,A148;
then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1 = x & a1.n<g1 & g1<x0;
then not x in {x0} by TARSKI:def 1;
hence thesis by A151,A150,XBOOLE_0:def 5;
end;
A152: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A153: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A154: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A140,A154;
hence (((f/g)/*a)^\k).n = (((f`|N)/(g`|N))/*b).n by A147,A152,FUNCT_2:108
,XBOOLE_1:1, A154;
end;
lim(((f`|N)/(g`|N)),x0)=lim(((f`|N)/(g`|N)),x0);
then
A155: ((f`|N)/(g`|N))/*b is convergent by A8,A144,A147,LIMFUNC3:def 4;
then
A156: ((f/g)/*a)^\k is convergent by A153,SEQ_4:18;
lim (((f`|N)/(g`|N))/*b) = lim(((f`|N)/(g`|N)),x0) by A8,A144,A147,
LIMFUNC3:def 4;
then lim (((f/g)/*a)^\k) = lim(((f`|N)/(g`|N)),x0) by A155,A153,SEQ_4:19;
hence thesis by A156,SEQ_4:21,22;
end;
for r1 st r1<x0 ex t st r1<t & t<x0 & t in dom (f/g) by A83,LIMFUNC3:8;
then
A157: f/g is_left_convergent_in x0 & lim_left(f/g,x0)=lim(((f`|N)/(g`|N) ),
x0) by A129,Th3;
hence f/g is_convergent_in x0 by A84,LIMFUNC3:30;
take N;
thus thesis by A84,A157,LIMFUNC3:30;
end;
::$N l'Hospital Theorem
::$L https://en.wikipedia.org/wiki/L'Hopital's_rule l'Hospital Theorem
theorem
(ex N being Neighbourhood of x0 st N c= dom f & N c= dom g & f
is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f/g) & N
c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 & (f`|N)/(g`|N) is_continuous_in
x0) implies f/g is_convergent_in x0 & lim(f/g,x0) = diff(f,x0)/diff(g,x0)
proof
given N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: N c= dom g and
A3: f is_differentiable_on N and
A4: g is_differentiable_on N and
A5: N \ {x0} c= dom (f/g) and
A6: N c= dom ((f`|N)/(g`|N)) and
A7: f.x0 = 0 & g.x0 = 0 and
A8: (f`|N)/(g`|N) is_continuous_in x0;
consider r be Real such that
A9: 0<r and
A10: N = ].x0-r,x0+r.[ by RCOMP_1:def 6;
A11: for x st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|N)/(g`|N)) .c
proof
A12: x0+0<x0+r by A9,XREAL_1:8;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A12;
then
A13: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A14: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A15: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A16: x0-r<x and
A17: x<x0;
set f1 = (f.x)(#)g - (g.x)(#)f;
A18: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A19: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x<x0+r by A17,A12,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A16;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A20: [.x,x0.] c= N by A10,A13,XXREAL_2:def 12;
then
A21: [.x,x0.] c= dom f & [.x,x0.] c= dom g by A1,A2;
then
A22: [.x,x0.] c= dom f1 by A19,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A23: ((f.x)(#)g)|[.x,x0.] is continuous by A2,A20,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x,x0.] is continuous by A20,FCONT_1:16;
then
A24: ((g.x)(#)f)|[.x,x0.] is continuous by A1,A20,FCONT_1:20,XBOOLE_1:1;
[.x,x0.] c= dom((f.x)(#)g - (g.x)(#)f) by A21,A19,XBOOLE_1:19;
then
A25: ((f.x)(#)g - (g.x)(#)f)|[.x,x0.] is continuous by A18,A19,A24,A23,
FCONT_1:18;
A26: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then
A27: ].x,x0.[ c= N by A20;
A28: x in [.x,x0.] by A17,XXREAL_1:1;
then x in dom f1 by A22;
then
A29: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A30: x in dom ((f.x) (#) g) by XBOOLE_0:def 4;
A31: x0 in [.x,x0.] by A17,XXREAL_1:1;
then x0 in dom f1 by A22;
then
A32: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A33: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A34: x in dom ((g.x)(#)f) by A29,XBOOLE_0:def 4;
A35: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A22,A28,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A30,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A34,VALUED_1:def 5
.= 0;
A36: x0 in dom ((g.x)(#)f) by A32,XBOOLE_0:def 4;
not x in {x0} by A17,TARSKI:def 1;
then
A37: x in [.x,x0.]\{x0} by A28,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A38: ].x,x0.[ c= dom ((f.x)(#)g) by A27;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A39: ].x,x0.[ c= dom ((g.x)(#)f) by A27;
then ].x,x0.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A38,XBOOLE_1:19;
then
A40: ].x,x0.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A3,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A41: (g.x)(#)f is_differentiable_on ].x,x0.[ by A39,FDIFF_1:20;
g is_differentiable_on ].x,x0.[ by A4,A20,A26,FDIFF_1:26,XBOOLE_1:1;
then
A42: (f.x)(#)g is_differentiable_on ].x,x0.[ by A38,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A22,A31,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A33,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A36,VALUED_1:def 5
.= 0;
then consider t such that
A43: t in ].x,x0.[ and
A44: diff(f1,t)=0 by A17,A25,A41,A40,A42,A22,A35,FDIFF_1:19,ROLLE:1;
A45: (g.x)(#)f is_differentiable_in t by A41,A43,FDIFF_1:9;
A46: f is_differentiable_in t by A3,A27,A43,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A42,A43,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A44,A45,FDIFF_1:14;
then
A47: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A46,FDIFF_1:15;
take t;
A48: t in [.x,x0.] by A26,A43;
[.x,x0.]\{x0} c= N\{x0} by A20,XBOOLE_1:33;
then
A49: [.x,x0.]\{x0} c= dom(f/g) by A5;
then [.x,x0.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x,x0.]\{x0} c= dom g\g"{0} by A15;
then
A50: x in dom g & not x in g"{0} by A37,XBOOLE_0:def 5;
A51: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A50,FUNCT_1:def 7;
end;
A52: [.x,x0.] c= dom ((f`|N)/(g`|N)) by A6,A20;
then [.x,x0.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x,x0.] c= dom (g`|N)\(g`|N)"{0} by A14;
then
A53: t in dom (g`|N) & not t in (g`|N)"{0} by A48,XBOOLE_0:def 5;
A54: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A20,A48,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A53,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A27,A43,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A47,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A51,A54,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A49,A37,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A20,A48,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A20,A48,FDIFF_1:def 7;
hence thesis by A43,A52,A48,RFUNCT_1:def 1;
end;
A55: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
left_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) = diff(f,x0
)/diff(g,x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A56: a is convergent and
A57: lim a = x0 and
A58: rng a c= dom (f/g) /\ left_open_halfline(x0);
consider k such that
A59: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A56,A57,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].a1.$1,x0.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A60: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in left_open_halfline(x0) by A58,XBOOLE_0:def 4;
then a.(n+k) in {g1:g1<x0} by XXREAL_1:229;
then ex g1 st a.(n+k)=g1 & g1<x0;
hence a1.n<x0 by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence x0-r<a1.n by A59;
end;
A61: for n ex c be Element of REAL st X[n,c]
proof
let n;
A62: rng a1 c= rng a by VALUED_0:21;
x0-r<a1.n & a1.n<x0 by A60;
then consider c such that
A63: c in ].a1.n,x0.[ and
A64: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A11;
take c;
A65: dom (f/g) /\ left_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A58;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A64,A62,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A58,A63,A65,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A66: for n holds X[n,b.n] from FUNCT_2:sch 3(A61);
A67: x0<x0+r by A9,XREAL_1:29;
x0-r<x0 by A9,XREAL_1:44;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A67;
then
A68: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A69: rng b c= dom ((f`|N)/(g`|N)) /\ left_open_halfline(x0)
proof
let x be object;
assume x in rng b;
then consider n such that
A70: x=b.n by FUNCT_2:113;
a1.n<x0 by A60;
then
A71: a1.n<x0+r by A67,XXREAL_0:2;
x0-r<a1.n by A60;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A71;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A68,
XXREAL_1:25,XXREAL_2:def 12;
then ].a1.n,x0.[ c= ].x0-r,x0+r.[;
then
A72: ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A73: x in ].a1.n,x0.[ by A66,A70;
then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=x & a1.n<g1 & g1<x0;
then x in {g2:g2<x0};
then x in left_open_halfline(x0) by XXREAL_1:229;
hence thesis by A73,A72,XBOOLE_0:def 4;
end;
A74: now
let n be Nat;
A75: n in NAT by ORDINAL1:def 12;
b.n in ].a1.n,x0.[ by A66,A75;
then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
hence a1.n<=b.n & b.n<= d.n by SEQ_1:57;
end;
A76: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A56,A57,SEQ_4:20;
then
A77: b is convergent & lim b=x0 by A56,A76,A74,SEQ_2:19,20;
A78: dom ((f`|N)/(g`|N)) /\ left_open_halfline(x0) c= dom ((f`|N)/(g`| N)
) by XBOOLE_1:17;
then
A79: rng b c= dom ((f`|N)/(g`|N)) by A69;
then
A80: ((f`|N)/(g`|N))/*b is convergent by A8,A77,FCONT_1:def 1;
A81: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A82: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A66,A82;
hence (((f/g)/*a)^\k).n = (((f`|N)/(g`|N))/*b).n by A69,A78,FUNCT_2:108
,XBOOLE_1:1, A82;
end;
lim (((f`|N)/(g`|N))/*b) = ((f`|N)/(g`|N)).x0 by A8,A77,A79,FCONT_1:def 1;
then lim (((f`|N)/(g`|N))/*b) = ((f`|N).x0)*((g`|N).x0)" by A6,A10,A68,
RFUNCT_1:def 1
.= diff(f,x0)*((g`|N).x0)" by A3,A10,A68,FDIFF_1:def 7
.= diff(f,x0)*diff(g,x0)" by A4,A10,A68,FDIFF_1:def 7;
then lim (((f/g)/*a)^\k) = diff(f,x0)*diff(g,x0)" by A80,A81,SEQ_4:19;
then
A83: lim(((f/g)/*a)^\k) = diff(f,x0)/diff(g,x0) by XCMPLX_0:def 9;
((f/g)/*a)^\k is convergent by A80,A81,SEQ_4:18;
hence thesis by A83,SEQ_4:21,22;
end;
A84: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom (f/g)
& g2<r2 & x0<g2 & g2 in dom (f/g) by A5,Th4;
then for r1 st r1<x0 ex t st r1<t & t<x0 & t in dom (f/g) by LIMFUNC3:8;
then
A85: f/g is_left_convergent_in x0 & lim_left(f/g,x0)=diff(f,x0)/diff(g,x0)
by A55,Th3;
A86: for x st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|N)/(g`|N)). c
proof
A87: x0-r<x0 by A9,XREAL_1:44;
x0+0<x0+r by A9,XREAL_1:8;
then x0 in {g1: x0-r<g1 & g1<x0+r} by A87;
then
A88: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A89: dom (f`|N) /\ (dom (g`|N) \ (g`|N)"{0}) c= dom (g`|N)\(g`|N)"{0} by
XBOOLE_1:17;
A90: dom f /\ (dom g\g"{0}) c= dom g\g"{0} by XBOOLE_1:17;
let x such that
A91: x0<x and
A92: x<x0+r;
set f1 = (f.x)(#)g - (g.x)(#)f;
A93: dom((f.x)(#)g) = dom g & dom((g.x)(#)f) = dom f by VALUED_1:def 5;
then
A94: dom((f.x)(#)g - (g.x)(#)f) = dom f /\ dom g by VALUED_1:12;
x0-r<x by A91,A87,XXREAL_0:2;
then x in {g1: x0-r<g1 & g1<x0+r} by A92;
then x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then
A95: [.x0,x.] c= N by A10,A88,XXREAL_2:def 12;
then
A96: [.x0,x.] c= dom f & [.x0,x.] c= dom g by A1,A2;
then
A97: [.x0,x.] c= dom f1 by A94,XBOOLE_1:19;
g|N is continuous by A4,FDIFF_1:25;
then g|[.x0,x.] is continuous by A95,FCONT_1:16;
then
A98: ((f.x)(#)g)|[.x0,x.] is continuous by A2,A95,FCONT_1:20,XBOOLE_1:1;
f|N is continuous by A3,FDIFF_1:25;
then f|[.x0,x.] is continuous by A95,FCONT_1:16;
then
A99: ((g.x)(#)f)|[.x0,x.] is continuous by A1,A95,FCONT_1:20,XBOOLE_1:1;
[.x0,x.] c= dom((f.x)(#)g - (g.x)(#)f) by A96,A94,XBOOLE_1:19;
then
A100: ((f.x)(#)g - (g.x)(#)f)|[.x0,x.] is continuous by A93,A94,A99,A98,
FCONT_1:18;
A101: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then
A102: ].x0,x.[ c= N by A95;
A103: x in [.x0,x.] by A91,XXREAL_1:1;
then x in dom f1 by A97;
then
A104: x in dom ((f.x)(#)g) /\ dom ((g.x) (#)f) by VALUED_1:12;
then
A105: x in dom ((f.x) (#)g) by XBOOLE_0:def 4;
A106: x0 in [.x0,x.] by A91,XXREAL_1:1;
then x0 in dom f1 by A97;
then
A107: x0 in dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by VALUED_1:12;
then
A108: x0 in dom ((f.x)(#)g) by XBOOLE_0:def 4;
A109: x in dom ((g.x)(#)f) by A104,XBOOLE_0:def 4;
A110: f1.x = ((f.x)(#)g).x - ((g.x)(#)f).x by A97,A103,VALUED_1:13
.= (f.x)*(g.x) - ((g.x)(#)f).x by A105,VALUED_1:def 5
.= (g.x)*(f.x) - (g.x)*(f.x) by A109,VALUED_1:def 5
.= 0;
A111: x0 in dom ((g.x)(#)f) by A107,XBOOLE_0:def 4;
not x in {x0} by A91,TARSKI:def 1;
then
A112: x in [.x0,x.]\{x0} by A103,XBOOLE_0:def 5;
N c= dom ((f.x)(#)g) by A2,VALUED_1:def 5;
then
A113: ].x0,x.[ c= dom ((f.x)(#)g) by A102;
N c= dom ((g.x)(#)f) by A1,VALUED_1:def 5;
then
A114: ].x0,x.[ c= dom ((g.x)(#)f) by A102;
then ].x0,x.[ c= dom ((f.x)(#)g) /\ dom ((g.x)(#)f) by A113,XBOOLE_1:19;
then
A115: ].x0,x.[ c= dom ((f.x)(#)g - (g.x)(#)f) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A3,A95,A101,FDIFF_1:26,XBOOLE_1:1;
then
A116: (g.x)(#)f is_differentiable_on ].x0,x.[ by A114,FDIFF_1:20;
g is_differentiable_on ].x0,x.[ by A4,A95,A101,FDIFF_1:26,XBOOLE_1:1;
then
A117: (f.x)(#)g is_differentiable_on ].x0,x.[ by A113,FDIFF_1:20;
f1.x0 = ((f.x)(#)g).x0 - ((g.x)(#)f).x0 by A97,A106,VALUED_1:13
.= (f.x)*(g.x0) - ((g.x)(#)f).x0 by A108,VALUED_1:def 5
.= 0 - (g.x)*0 by A7,A111,VALUED_1:def 5
.= 0;
then consider t such that
A118: t in ].x0,x.[ and
A119: diff(f1,t)=0 by A91,A100,A116,A115,A117,A97,A110,FDIFF_1:19,ROLLE:1;
A120: (g.x)(#)f is_differentiable_in t by A116,A118,FDIFF_1:9;
A121: f is_differentiable_in t by A3,A102,A118,FDIFF_1:9;
(f.x)(#)g is_differentiable_in t by A117,A118,FDIFF_1:9;
then 0=diff((f.x)(#)g,t) - diff((g.x)(#)f,t) by A119,A120,FDIFF_1:14;
then
A122: 0=diff((f.x)(#)g,t) - (g.x)*diff(f,t) by A121,FDIFF_1:15;
take t;
A123: t in [.x0,x.] by A101,A118;
[.x0,x.]\{x0} c= N\{x0} by A95,XBOOLE_1:33;
then
A124: [.x0,x.]\{x0} c= dom(f/g) by A5;
then [.x0,x.]\{x0} c= dom f /\ (dom g\g"{0}) by RFUNCT_1:def 1;
then [.x0,x.]\{x0} c= dom g\g"{0} by A90;
then
A125: x in dom g & not x in g"{0} by A112,XBOOLE_0:def 5;
A126: now
assume g.x=0;
then g.x in {0} by TARSKI:def 1;
hence contradiction by A125,FUNCT_1:def 7;
end;
A127: [.x0,x.] c= dom ((f`|N)/(g`|N)) by A6,A95;
then [.x0,x.] c= dom (f`|N) /\ (dom (g`|N)\(g`|N)"{0}) by RFUNCT_1:def 1;
then [.x0,x.] c= dom (g`|N)\(g`|N)"{0} by A89;
then
A128: t in dom (g`|N) & not t in (g`|N)"{0} by A123,XBOOLE_0:def 5;
A129: now
assume diff(g,t)=0;
then (g`|N).t=0 by A4,A95,A123,FDIFF_1:def 7;
then (g`|N).t in {0} by TARSKI:def 1;
hence contradiction by A128,FUNCT_1:def 7;
end;
g is_differentiable_in t by A4,A102,A118,FDIFF_1:9;
then 0=(f.x)*diff(g,t) - (g.x)*diff(f,t) by A122,FDIFF_1:15;
then (f.x)/(g.x) = diff(f,t)/diff(g,t) by A126,A129,XCMPLX_1:94;
then (f.x)*(g.x)" = diff(f,t)/diff(g,t) by XCMPLX_0:def 9;
then (f.x)*(g.x)" = diff(f,t)*diff(g,t)" by XCMPLX_0:def 9;
then (f/g).x = diff(f,t)*diff(g,t)" by A124,A112,RFUNCT_1:def 1;
then (f/g).x = ((f`|N).t)*diff(g,t)" by A3,A95,A123,FDIFF_1:def 7;
then (f/g).x = ((f`|N).t)*((g`|N).t)" by A4,A95,A123,FDIFF_1:def 7;
hence thesis by A118,A127,A123,RFUNCT_1:def 1;
end;
A130: for a st a is convergent & lim a = x0 & rng a c= dom (f/g) /\
right_open_halfline(x0) holds (f/g)/*a is convergent & lim((f/g)/*a) = diff(f,
x0)/diff(g,x0)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a;
assume that
A131: a is convergent and
A132: lim a = x0 and
A133: rng a c= dom (f/g) /\ right_open_halfline(x0);
consider k such that
A134: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A131,A132,LIMFUNC3:7;
set a1 = a^\k;
defpred X[Element of NAT,Real] means $2 in ].x0,a1.$1.[ & (((f/g)/*
a)^\k).$1=((f`|N)/(g`|N)).$2;
A135: now
let n;
a.(n+k) in rng a by VALUED_0:28;
then a.(n+k) in right_open_halfline(x0) by A133,XBOOLE_0:def 4;
then a.(n+k) in {g1:x0<g1} by XXREAL_1:230;
then ex g1 st a.(n+k)=g1 & x0<g1;
hence x0<a1.n by NAT_1:def 3;
a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
hence a1.n<x0+r by A134;
end;
A136: for n ex c be Element of REAL st X[n,c]
proof
let n;
A137: rng a1 c= rng a by VALUED_0:21;
x0<a1.n & a1.n<x0+r by A135;
then consider c such that
A138: c in ].x0,a1.n.[ and
A139: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A86;
take c;
A140: dom (f/g) /\ right_open_halfline(x0) c= dom (f/g) by XBOOLE_1:17;
then rng a c= dom (f/g) by A133;
then ((f/g)/*(a^\k)).n=((f`|N)/(g`|N)).c by A139,A137,FUNCT_2:108
,XBOOLE_1:1;
hence thesis by A133,A138,A140,VALUED_0:27,XBOOLE_1:1;
end;
consider b such that
A141: for n holds X[n,b.n] from FUNCT_2:sch 3(A136);
A142: x0-r<x0 by A9,XREAL_1:44;
x0<x0+r by A9,XREAL_1:29;
then x0 in {g2: x0-r<g2 & g2<x0+r} by A142;
then
A143: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A144: rng b c= dom ((f`|N)/(g`|N)) /\ right_open_halfline(x0)
proof
let x be object;
assume x in rng b;
then consider n such that
A145: x=b.n by FUNCT_2:113;
x0<a1.n by A135;
then
A146: x0-r<a1.n by A142,XXREAL_0:2;
a1.n<x0+r by A135;
then a1.n in {g3: x0-r<g3 & g3<x0+r} by A146;
then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A143,
XXREAL_1:25,XXREAL_2:def 12;
then ].x0,a1.n.[ c= ].x0-r,x0+r.[;
then
A147: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10;
A148: x in ].x0,a1.n.[ by A141,A145;
then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=x & x0<g1 & g1<a1.n;
then x in {g2:x0<g2};
then x in right_open_halfline(x0) by XXREAL_1:230;
hence thesis by A148,A147,XBOOLE_0:def 4;
end;
A149: now
let n be Nat;
A150: n in NAT by ORDINAL1:def 12;
b.n in ].x0,a1.n.[ by A141,A150;
then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
hence d.n<=b.n & b.n<=a1.n by SEQ_1:57;
end;
A151: lim d=d.0 by SEQ_4:26
.=x0 by SEQ_1:57;
lim a1=x0 by A131,A132,SEQ_4:20;
then
A152: b is convergent & lim b=x0 by A131,A151,A149,SEQ_2:19,20;
A153: dom ((f`|N)/(g`|N)) /\ right_open_halfline(x0) c= dom ((f`|N)/(g`| N
)) by XBOOLE_1:17;
then
A154: rng b c= dom ((f`|N)/(g`|N)) by A144;
then
A155: ((f`|N)/(g`|N))/*b is convergent by A8,A152,FCONT_1:def 1;
A156: now
reconsider m = 0 as Nat;
take m;
let n be Nat such that
m <=n;
A157: n in NAT by ORDINAL1:def 12;
(((f/g)/*a)^\k).n=((f`|N)/(g`|N)).(b.n) by A141,A157;
hence (((f/g)/*a)^\k).n = (((f`|N)/(g`|N))/*b).n by A144,A153,FUNCT_2:108
,XBOOLE_1:1, A157;
end;
lim (((f`|N)/(g`|N))/*b) = ((f`|N)/(g`|N)).x0 by A8,A152,A154,FCONT_1:def 1
;
then lim (((f`|N)/(g`|N))/*b) = ((f`|N).x0)*((g`|N).x0)" by A6,A10,A143,
RFUNCT_1:def 1
.= diff(f,x0)*((g`|N).x0)" by A3,A10,A143,FDIFF_1:def 7
.= diff(f,x0)*diff(g,x0)" by A4,A10,A143,FDIFF_1:def 7;
then lim (((f/g)/*a)^\k) = diff(f,x0)*diff(g,x0)" by A155,A156,SEQ_4:19;
then
A158: lim(((f/g)/*a)^\k) = diff(f,x0)/diff(g,x0) by XCMPLX_0:def 9;
((f/g)/*a)^\k is convergent by A155,A156,SEQ_4:18;
hence thesis by A158,SEQ_4:21,22;
end;
for r1 st x0<r1 ex t st t<r1 & x0<t & t in dom (f/g) by A84,LIMFUNC3:8;
then f/g is_right_convergent_in x0 & lim_right(f/g,x0)=diff(f,x0)/diff(g,x0
) by A130,Th2;
hence thesis by A85,LIMFUNC3:30;
end;