let f be PartFunc of REAL,REAL; for x0 being Real st f is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0 ) ) holds
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
let x0 be Real; ( f is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0 ) ) implies ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) ) )
assume A1:
f is_left_differentiable_in x0
; ( for r0 being Real holds
( not r0 > 0 or ex g being Real st
( g in dom f & g in [.(x0 - r0),x0.] & not f . g <> 0 ) ) or ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) ) )
then consider r2 being Real such that
A2:
0 < r2
and
A3:
[.(x0 - r2),x0.] c= dom f
;
given r0 being Real such that A4:
r0 > 0
and
A5:
for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0
; ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
set r3 = min (r0,r2);
A6:
0 < min (r0,r2)
by A4, A2, XXREAL_0:15;
then A7:
x0 - (min (r0,r2)) <= x0
by XREAL_1:43;
min (r0,r2) <= r2
by XXREAL_0:17;
then A8:
x0 - r2 <= x0 - (min (r0,r2))
by XREAL_1:13;
then
x0 - r2 <= x0
by A7, XXREAL_0:2;
then A9:
x0 in [.(x0 - r2),x0.]
by XXREAL_1:1;
x0 - (min (r0,r2)) in { g where g is Real : ( x0 - r2 <= g & g <= x0 ) }
by A7, A8;
then
x0 - (min (r0,r2)) in [.(x0 - r2),x0.]
by RCOMP_1:def 1;
then
[.(x0 - (min (r0,r2))),x0.] c= [.(x0 - r2),x0.]
by A9, XXREAL_2:def 12;
then A10:
[.(x0 - (min (r0,r2))),x0.] c= dom f
by A3;
min (r0,r2) <= r0
by XXREAL_0:17;
then A11:
x0 - r0 <= x0 - (min (r0,r2))
by XREAL_1:13;
then
x0 - r0 <= x0
by A7, XXREAL_0:2;
then A12:
x0 in [.(x0 - r0),x0.]
by XXREAL_1:1;
x0 - (min (r0,r2)) in { g where g is Real : ( x0 - r0 <= g & g <= x0 ) }
by A7, A11;
then
x0 - (min (r0,r2)) in [.(x0 - r0),x0.]
by RCOMP_1:def 1;
then A13:
[.(x0 - (min (r0,r2))),x0.] c= [.(x0 - r0),x0.]
by A12, XXREAL_2:def 12;
A14:
[.(x0 - (min (r0,r2))),x0.] c= dom (f ^)
A20:
x0 in [.(x0 - (min (r0,r2))),x0.]
by A7, XXREAL_1:1;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f ^) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
proof
let h be
non-zero 0 -convergent Real_Sequence;
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f ^) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )let c be
constant Real_Sequence;
( rng c = {x0} & rng (h + c) c= dom (f ^) & ( for n being Nat holds h . n < 0 ) implies ( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) ) )
assume that A21:
rng c = {x0}
and A22:
rng (h + c) c= dom (f ^)
and A23:
for
n being
Nat holds
h . n < 0
;
( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
A24:
for
m being
Element of
NAT holds
c . m = x0
A25:
(dom f) \ (f " {0}) c= dom f
by XBOOLE_1:36;
rng (h + c) c= (dom f) \ (f " {0})
by A22, RFUNCT_1:def 2;
then A26:
rng (h + c) c= dom f
by A25;
then A27:
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (
f,
x0)
by A1, A21, A23, Th9;
A28:
(h ") (#) ((f /* (h + c)) - (f /* c)) is
convergent
by A1, A21, A23, A26;
then A29:
- ((h ") (#) ((f /* (h + c)) - (f /* c))) is
convergent
;
x0 in dom (f ^)
by A20, A14;
then A30:
x0 in (dom f) \ (f " {0})
by RFUNCT_1:def 2;
rng c c= (dom f) \ (f " {0})
by A21, A30, TARSKI:def 1;
then A31:
rng c c= dom (f ^)
by RFUNCT_1:def 2;
then A32:
f /* c is
non-zero
by RFUNCT_2:11;
then A34:
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c)
by FUNCT_2:63;
A35:
f /* (h + c) is
non-zero
by A22, RFUNCT_2:11;
then A36:
(f /* (h + c)) (#) (f /* c) is
non-zero
by A32, SEQ_1:35;
then A37:
(f /* c) + ((f /* (h + c)) - (f /* c)) = f /* (h + c)
by FUNCT_2:63;
dom (f ^) = (dom f) \ (f " {0})
by RFUNCT_1:def 2;
then A38:
dom (f ^) c= dom f
by XBOOLE_1:36;
A39:
for
g being
Real st
0 < g holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g
then A42:
f /* c is
convergent
by SEQ_2:def 6;
then A43:
lim (f /* c) = f . x0
by A39, SEQ_2:def 7;
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) is
convergent
by A28;
then A44:
f /* (h + c) is
convergent
by A42, A34, A37;
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) =
(lim h) * (lim ((h ") (#) ((f /* (h + c)) - (f /* c))))
by A28, SEQ_2:15
.=
0
;
then
0 = (lim (f /* (h + c))) - (f . x0)
by A42, A43, A34, A44, SEQ_2:12;
then A45:
lim ((f /* (h + c)) (#) (f /* c)) = (f . x0) ^2
by A42, A43, A44, SEQ_2:15;
A46:
lim ((f /* (h + c)) (#) (f /* c)) <> 0
then A48:
(h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) = (- ((h ") (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c))
by FUNCT_2:63;
A49:
(f /* (h + c)) (#) (f /* c) is
convergent
by A42, A44;
then lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) =
(lim (- ((h ") (#) ((f /* (h + c)) - (f /* c))))) / ((f . x0) ^2)
by A36, A45, A46, A29, A48, SEQ_2:24
.=
(- (Ldiff (f,x0))) / ((f . x0) ^2)
by A28, A27, SEQ_2:10
.=
- ((Ldiff (f,x0)) / ((f . x0) ^2))
by XCMPLX_1:187
;
hence
(
(h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is
convergent &
lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
by A36, A49, A46, A29, A48, SEQ_2:23;
verum
end;
hence
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
by A6, A14, Th9; verum