let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f . x0 <> 0 & f is_differentiable_in x0 holds
( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f . x0 <> 0 & f is_differentiable_in x0 implies ( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) ) )
reconsider f1 = (dom f) --> jj as PartFunc of (dom f),REAL by FUNCOP_1:45;
reconsider f1 = f1 as PartFunc of REAL,REAL ;
assume that
A1: f . x0 <> 0 and
A2: f is_differentiable_in x0 ; :: thesis: ( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) )
consider N being Neighbourhood of x0 such that
A3: N c= dom f by A2;
A4: x0 in N by RCOMP_1:16;
A5: dom f1 = dom f by FUNCOP_1:13;
A6: rng f1 = {1}
proof
thus rng f1 c= {1} by FUNCOP_1:13; :: according to XBOOLE_0:def 10 :: thesis: {1} c= rng f1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in rng f1 )
A7: x0 in N by RCOMP_1:16;
assume x in {1} ; :: thesis: x in rng f1
then x = 1 by TARSKI:def 1;
then f1 . x0 = x by A3, A7, FUNCOP_1:7;
hence x in rng f1 by A5, A3, A7, FUNCT_1:def 3; :: thesis: verum
end;
then A8: f1 is_differentiable_on N by A5, A3, FDIFF_1:11;
then A9: f1 is_differentiable_in x0 by A4, FDIFF_1:9;
0 = (f1 `| N) . x0 by A5, A3, A6, FDIFF_1:11, RCOMP_1:16
.= diff (f1,x0) by A8, A4, FDIFF_1:def 7 ;
then diff ((f1 / f),x0) = ((0 * (f . x0)) - ((diff (f,x0)) * (f1 . x0))) / ((f . x0) ^2) by A1, A2, A9, Th14;
then A10: diff ((f1 / f),x0) = (- ((diff (f,x0)) * (f1 . x0))) / ((f . x0) ^2)
.= (- ((diff (f,x0)) * 1)) / ((f . x0) ^2) by A3, A4, FUNCOP_1:7
.= - ((diff (f,x0)) / ((f . x0) ^2)) by XCMPLX_1:187 ;
A11: dom (f1 / f) = (dom f1) /\ ((dom f) \ (f " {0})) by RFUNCT_1:def 1
.= (dom f) \ (f " {0}) by A5, XBOOLE_1:28, XBOOLE_1:36
.= dom (f ^) by RFUNCT_1:def 2 ;
A12: (dom f) \ (f " {0}) c= dom f1 by A5, XBOOLE_1:36;
A13: now :: thesis: for r being Element of REAL st r in dom (f1 / f) holds
(f1 / f) . r = (f ^) . r
A14: (dom f) \ (f " {0}) = dom (f ^) by RFUNCT_1:def 2;
let r be Element of REAL ; :: thesis: ( r in dom (f1 / f) implies (f1 / f) . r = (f ^) . r )
assume A15: r in dom (f1 / f) ; :: thesis: (f1 / f) . r = (f ^) . r
thus (f1 / f) . r = (f1 . r) * ((f . r) ") by A15, RFUNCT_1:def 1
.= 1 * ((f . r) ") by A5, A12, A11, A15, A14, FUNCOP_1:7
.= (f ^) . r by A11, A15, RFUNCT_1:def 2 ; :: thesis: verum
end;
f1 / f is_differentiable_in x0 by A1, A2, A9, Th14;
hence ( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) ) by A10, A11, A13, PARTFUN1:5; :: thesis: verum