let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) )
assume that
A1: f2 . x0 <> 0 and
A2: f1 is_differentiable_in x0 and
A3: f2 is_differentiable_in x0 ; :: thesis: ( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
consider N1 being Neighbourhood of x0 such that
A4: N1 c= dom f1 by A2;
consider N3 being Neighbourhood of x0 such that
A5: N3 c= dom f2 and
A6: for g being Real st g in N3 holds
f2 . g <> 0 by A1, A3, FCONT_3:7, FDIFF_1:24;
consider N being Neighbourhood of x0 such that
A7: N c= N1 and
A8: N c= N3 by RCOMP_1:17;
A9: N c= (dom f2) \ (f2 " {0})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in (dom f2) \ (f2 " {0}) )
assume A10: x in N ; :: thesis: x in (dom f2) \ (f2 " {0})
then reconsider x9 = x as Real ;
f2 . x9 <> 0 by A6, A8, A10;
then not f2 . x9 in {0} by TARSKI:def 1;
then A11: not x9 in f2 " {0} by FUNCT_1:def 7;
x9 in N3 by A8, A10;
hence x in (dom f2) \ (f2 " {0}) by A5, A11, XBOOLE_0:def 5; :: thesis: verum
end;
A12: f2 is_continuous_in x0 by A3, FDIFF_1:24;
N c= dom f1 by A4, A7;
then A13: N c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A9, XBOOLE_1:19;
A14: for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 / f2) holds
( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
proof
dom (f2 ^) = (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
then A15: dom (f2 ^) c= dom f2 by XBOOLE_1:36;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 / f2) holds
( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f1 / f2) implies ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) )
assume that
A16: rng c = {x0} and
A17: rng (h + c) c= dom (f1 / f2) ; :: thesis: ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
A18: rng (h + c) c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A17, RFUNCT_1:def 1;
(dom f1) /\ ((dom f2) \ (f2 " {0})) c= (dom f2) \ (f2 " {0}) by XBOOLE_1:17;
then A19: rng (h + c) c= (dom f2) \ (f2 " {0}) by A18;
then A20: rng (h + c) c= dom (f2 ^) by RFUNCT_1:def 2;
then A21: f2 /* (h + c) is non-zero by RFUNCT_2:11;
A22: lim c = x0 by A16, Th4;
set u2 = f2 /* c;
set u1 = f1 /* c;
set v2 = f2 /* (h + c);
set h2 = (h ") (#) ((f2 /* (h + c)) - (f2 /* c));
set v1 = f1 /* (h + c);
set h1 = (h ") (#) ((f1 /* (h + c)) - (f1 /* c));
A23: f1 is_continuous_in x0 by A2, FDIFF_1:24;
A24: rng c c= (dom f1) /\ (dom (f2 ^))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in (dom f1) /\ (dom (f2 ^)) )
assume x in rng c ; :: thesis: x in (dom f1) /\ (dom (f2 ^))
then A25: x = x0 by A16, TARSKI:def 1;
x0 in N by RCOMP_1:16;
then x in (dom f1) /\ ((dom f2) \ (f2 " {0})) by A13, A25;
hence x in (dom f1) /\ (dom (f2 ^)) by RFUNCT_1:def 2; :: thesis: verum
end;
A26: (dom f1) /\ (dom (f2 ^)) c= dom (f2 ^) by XBOOLE_1:17;
then A27: f2 /* c is non-zero by A24, RFUNCT_2:11, XBOOLE_1:1;
(dom f1) /\ ((dom f2) \ (f2 " {0})) c= dom f1 by XBOOLE_1:17;
then A28: rng (h + c) c= dom f1 by A18;
then A29: rng (h + c) c= (dom f1) /\ (dom (f2 ^)) by A20, XBOOLE_1:19;
A30: (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) = (h ") (#) (((f1 (#) (f2 ^)) /* (h + c)) - ((f1 / f2) /* c)) by RFUNCT_1:31
.= (h ") (#) (((f1 (#) (f2 ^)) /* (h + c)) - ((f1 (#) (f2 ^)) /* c)) by RFUNCT_1:31
.= (h ") (#) (((f1 /* (h + c)) (#) ((f2 ^) /* (h + c))) - ((f1 (#) (f2 ^)) /* c)) by A29, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^)) /* c)) by A20, RFUNCT_2:12
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^) /* c))) by A24, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c))) by A24, A26, RFUNCT_2:12, XBOOLE_1:1
.= (h ") (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A21, A27, SEQ_1:50
.= ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c)) by SEQ_1:41 ;
rng c c= dom (f2 ^) by A24, A26;
then A31: rng c c= dom f2 by A15;
then A32: f2 /* c is convergent by A12, A22, FCONT_1:def 1;
(dom f1) /\ (dom (f2 ^)) c= dom f1 by XBOOLE_1:17;
then A33: rng c c= dom f1 by A24;
then A34: lim (f1 /* c) = f1 . x0 by A22, A23, FCONT_1:def 1;
(dom f2) \ (f2 " {0}) c= dom f2 by XBOOLE_1:36;
then A35: rng (h + c) c= dom f2 by A19;
diff (f2,x0) = diff (f2,x0) ;
then A36: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A3, A16, A35, Th12;
A37: f1 /* c is convergent by A33, A22, A23, FCONT_1:def 1;
then A38: (f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A36;
lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = diff (f2,x0) by A3, A16, A35, Th12;
then A39: lim ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) = (diff (f2,x0)) * (f1 . x0) by A36, A37, A34, SEQ_2:15;
set w1 = (f2 /* (h + c)) (#) (f2 /* c);
A40: lim (h + c) = x0 by A16, Th4;
A41: f2 /* (h + c) is convergent by A12, A35, A40, FCONT_1:def 1;
then A42: (f2 /* (h + c)) (#) (f2 /* c) is convergent by A32;
f2 /* (h + c) is non-zero by A20, RFUNCT_2:11;
then A43: (f2 /* (h + c)) (#) (f2 /* c) is non-zero by A27, SEQ_1:35;
A44: lim (f2 /* c) = f2 . x0 by A12, A31, A22, FCONT_1:def 1;
diff (f1,x0) = diff (f1,x0) ;
then A45: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A2, A16, A28, Th12;
then A46: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A32;
lim (f2 /* (h + c)) = f2 . x0 by A12, A35, A40, FCONT_1:def 1;
then A47: lim ((f2 /* (h + c)) (#) (f2 /* c)) = (f2 . x0) ^2 by A41, A32, A44, SEQ_2:15;
now :: thesis: for n being Element of NAT holds ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) . n = ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) . n
let n be Element of NAT ; :: thesis: ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) . n = ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) . n
thus ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) . n = ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) . n) by SEQ_1:8
.= ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) . n) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by RFUNCT_2:1
.= ((h ") . n) * ((((f1 /* (h + c)) . n) * ((f2 /* c) . n)) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by SEQ_1:8
.= ((h ") . n) * ((((((f1 /* (h + c)) . n) - ((f1 /* c) . n)) * ((f2 /* c) . n)) + (((f1 /* c) . n) * ((f2 /* c) . n))) - (((f1 /* c) . n) * ((f2 /* (h + c)) . n))) by SEQ_1:8
.= ((((h ") . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n))))
.= ((((h ") . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n)))) by RFUNCT_2:1
.= ((((h ") . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) - (f2 /* c)) . n))) by RFUNCT_2:1
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) - (f2 /* c)) . n))) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) . n) * (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) . n) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) . n by RFUNCT_2:1 ; :: thesis: verum
end;
then A48: (h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) = (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) ;
then A49: (h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) is convergent by A46, A38;
hence (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent by A1, A30, A42, A47, A43, SEQ_2:23; :: thesis: lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2)
lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = diff (f1,x0) by A2, A16, A28, Th12;
then lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) = (diff (f1,x0)) * (f2 . x0) by A32, A44, A45, SEQ_2:15;
then lim ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) = ((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0)) by A48, A46, A38, A39, SEQ_2:12;
hence lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) by A1, A30, A42, A47, A49, A43, SEQ_2:24; :: thesis: verum
end;
N c= dom (f1 / f2) by A13, RFUNCT_1:def 1;
hence ( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A14, Th12; :: thesis: verum