let f be PartFunc of REAL,REAL; for x0 being Real st f is_differentiable_in x0 holds
( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
let x0 be Real; ( f is_differentiable_in x0 implies ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) ) )
assume A1:
f is_differentiable_in x0
; ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
then consider N being Neighbourhood of x0 such that
A2:
N c= dom f
by FDIFF_2:11;
consider g1 being Real such that
A3:
g1 > 0
and
A4:
N = ].(x0 - g1),(x0 + g1).[
by RCOMP_1:def 6;
A5:
g1 > g1 / 2
by A3, XREAL_1:216;
A6:
ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f )
proof
take r =
g1 / 2;
( r > 0 & [.x0,(x0 + r).] c= dom f )
thus
r > 0
by A3, XREAL_1:215;
[.x0,(x0 + r).] c= dom f
|.((x0 + (g1 / 2)) - x0).| = g1 / 2
by A3, ABSVALUE:def 1;
then A7:
x0 + r in ].(x0 - g1),(x0 + g1).[
by A5, RCOMP_1:1;
x0 in ].(x0 - g1),(x0 + g1).[
by A4, RCOMP_1:16;
then
[.x0,(x0 + r).] c= ].(x0 - g1),(x0 + g1).[
by A7, XXREAL_2:def 12;
hence
[.x0,(x0 + r).] c= dom f
by A2, A4;
verum
end;
A8:
ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f )
proof
take r =
g1 / 2;
( 0 < r & [.(x0 - r),x0.] c= dom f )
thus
r > 0
by A3, XREAL_1:215;
[.(x0 - r),x0.] c= dom f
|.((x0 - (g1 / 2)) - x0).| =
|.((- (g1 / 2)) + 0).|
.=
|.(g1 / 2).|
by COMPLEX1:52
.=
g1 / 2
by A3, ABSVALUE:def 1
;
then A9:
x0 - r in ].(x0 - g1),(x0 + g1).[
by A5, RCOMP_1:1;
x0 in ].(x0 - g1),(x0 + g1).[
by A4, RCOMP_1:16;
then
[.(x0 - r),x0.] c= ].(x0 - g1),(x0 + g1).[
by A9, XXREAL_2:def 12;
hence
[.(x0 - r),x0.] c= dom f
by A2, A4;
verum
end;
diff (f,x0) = diff (f,x0)
;
then
( ( 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))) = diff (f,x0) ) ) & ( 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))) = diff (f,x0) ) ) )
by A1, FDIFF_2:12;
hence
( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
by A6, A8, Th9, Th15; verum