let f be PartFunc of REAL,REAL; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 )

( 0 < r & [.(x0 - r),x0.] c= dom f )

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; :: thesis: verum

( 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; :: thesis: ( 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 ; :: thesis: ( 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

A8:
ex r being Real st
take r = g1 / 2; :: thesis: ( r > 0 & [.x0,(x0 + r).] c= dom f )

thus r > 0 by A3, XREAL_1:215; :: thesis: [.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; :: thesis: verum

end;thus r > 0 by A3, XREAL_1:215; :: thesis: [.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; :: thesis: verum

( 0 < r & [.(x0 - r),x0.] c= dom f )

proof

diff (f,x0) = diff (f,x0)
;
take r = g1 / 2; :: thesis: ( 0 < r & [.(x0 - r),x0.] c= dom f )

thus r > 0 by A3, XREAL_1:215; :: thesis: [.(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; :: thesis: verum

end;thus r > 0 by A3, XREAL_1:215; :: thesis: [.(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; :: thesis: verum

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; :: thesis: verum