let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I c= dom f & inf I < sup I & ex r being Real st rng f = {r} holds
( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 0 ) )
let I be non empty Interval; :: thesis: ( I c= dom f & inf I < sup I & ex r being Real st rng f = {r} implies ( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 0 ) ) )
assume that
A1: I c= dom f and
A2: inf I < sup I and
A3: ex r being Real st rng f = {r} ; :: thesis: ( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 0 ) )
consider r being Real such that
A4: rng f = {r} by A3;

A5: now :: thesis: ( inf I in I implies ( f is_right_differentiable_in lower_bound I & Rdiff (f,(lower_bound I)) = 0 ) )

assume A6: inf I in I ; :: thesis: ( f is_right_differentiable_in lower_bound I & Rdiff (f,(lower_bound I)) = 0 )
then A7: inf I = lower_bound I by Lm5;
consider e being Real such that
A8: ( e > 0 & [.(lower_bound I),((lower_bound I) + e).] c= I ) by A6, A2, Lm14;
A9: ( e > 0 & [.(lower_bound I),((lower_bound I) + e).] c= dom f ) by A8, A1;
A10: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & 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))) = 0 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {(lower_bound I)} & 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))) = 0 )
let c be constant Real_Sequence; :: thesis: ( rng c = {(lower_bound I)} & 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))) = 0 ) )
assume that
A11: rng c = {(lower_bound I)} and
A12: rng (h + c) c= dom f and
for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )
A13: for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p )
assume A14: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p
take N = 0 ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p

hereby :: thesis: verum

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p )
assume N <= k ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p
A15: rng c c= I by A6, A7, A11, ZFMISC_1:31;
A16: f /* c = f * c by A1, A6, A7, A11, ZFMISC_1:31, FUNCT_2:def 11;
A17: f /* (h + c) = f * (h + c) by A12, FUNCT_2:def 11;
A18: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom (f * (h + c)) & k in dom (f * c) ) by A12, A1, A6, A7, A11, ZFMISC_1:31, RELAT_1:27;
then k in (dom (f * (h + c))) /\ (dom (f * c)) by XBOOLE_0:def 4;
then A19: k in dom ((f * (h + c)) - (f * c)) by VALUED_1:12;
( (h + c) . k in rng (h + c) & c . k in rng c ) by A18, ORDINAL1:def 12, FUNCT_1:3;
then ( f . ((h + c) . k) in rng f & f . (c . k) in rng f ) by A1, A12, A15, FUNCT_1:3;
then A20: ( f . ((h + c) . k) = r & f . (c . k) = r ) by A4, TARSKI:def 1;
((h ") (#) ((f /* (h + c)) - (f /* c))) . k = ((h ") . k) * (((f * (h + c)) - (f * c)) . k) by A16, A17, VALUED_1:5
.= ((h ") . k) * (((f * (h + c)) . k) - ((f * c) . k)) by A19, VALUED_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - ((f * c) . k)) by A18, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - (f . (c . k))) by A18, ORDINAL1:def 12, FUNCT_1:13 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p by A20, A14, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A13, SEQ_2:def 7; :: thesis: verum

end;

then for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ;
hence A21: f is_right_differentiable_in lower_bound I by A9, FDIFF_3:def 3; :: thesis: Rdiff (f,(lower_bound I)) = 0
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(lower_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A10;
hence Rdiff (f,(lower_bound I)) = 0 by A21, FDIFF_3:def 6; :: thesis: verum

end;

A22: now :: thesis: ( sup I in I implies ( f is_left_differentiable_in upper_bound I & Ldiff (f,(upper_bound I)) = 0 ) )

assume A23: sup I in I ; :: thesis: ( f is_left_differentiable_in upper_bound I & Ldiff (f,(upper_bound I)) = 0 )
then A24: sup I = upper_bound I by Lm6;
consider e being Real such that
A25: ( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I ) by A23, A2, Lm15;
A26: ( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= dom f ) by A25, A1;
A27: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & 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))) = 0 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {(upper_bound I)} & 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))) = 0 )
let c be constant Real_Sequence; :: thesis: ( rng c = {(upper_bound I)} & 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))) = 0 ) )
assume that
A28: rng c = {(upper_bound I)} and
A29: rng (h + c) c= dom f and
for n being Nat holds h . n < 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )
A30: for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p )
assume A31: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p
take N = 0 ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p

hereby :: thesis: verum

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p )
assume N <= k ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p
A32: rng c c= dom f by A1, A23, A24, A28, ZFMISC_1:31;
A33: f /* c = f * c by A1, A23, A24, A28, ZFMISC_1:31, FUNCT_2:def 11;
A34: f /* (h + c) = f * (h + c) by A29, FUNCT_2:def 11;
A35: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom (f * (h + c)) & k in dom (f * c) ) by A29, A1, A23, A24, A28, ZFMISC_1:31, RELAT_1:27;
then k in (dom (f * (h + c))) /\ (dom (f * c)) by XBOOLE_0:def 4;
then A36: k in dom ((f * (h + c)) - (f * c)) by VALUED_1:12;
( (h + c) . k in rng (h + c) & c . k in rng c ) by A35, ORDINAL1:def 12, FUNCT_1:3;
then ( f . ((h + c) . k) in rng f & f . (c . k) in rng f ) by A29, A32, FUNCT_1:3;
then A37: ( f . ((h + c) . k) = r & f . (c . k) = r ) by A4, TARSKI:def 1;
((h ") (#) ((f /* (h + c)) - (f /* c))) . k = ((h ") . k) * (((f * (h + c)) - (f * c)) . k) by A33, A34, VALUED_1:5
.= ((h ") . k) * (((f * (h + c)) . k) - ((f * c) . k)) by A36, VALUED_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - ((f * c) . k)) by A35, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * ((f . ((h + c) . k)) - (f . (c . k))) by A35, ORDINAL1:def 12, FUNCT_1:13 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . k) - 0).| < p by A37, A31, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A30, SEQ_2:def 7; :: thesis: verum

end;

then for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ;
hence A38: f is_left_differentiable_in upper_bound I by A26, FDIFF_3:def 4; :: thesis: Ldiff (f,(upper_bound I)) = 0
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {(upper_bound I)} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A27;
hence Ldiff (f,(upper_bound I)) = 0 by A38, FDIFF_3:def 5; :: thesis: verum

end;

set J = ].(inf I),(sup I).[;
A39: ].(inf I),(sup I).[ c= I by Lm13;
then A40: ].(inf I),(sup I).[ c= dom f by A1;
then A41: dom (f | ].(inf I),(sup I).[) = ].(inf I),(sup I).[ by RELAT_1:62;
for x being Real st x in ].(inf I),(sup I).[ holds
f | ].(inf I),(sup I).[ is_differentiable_in x

proof

let x be Real; :: thesis: ( x in ].(inf I),(sup I).[ implies f | ].(inf I),(sup I).[ is_differentiable_in x )
assume A42: x in ].(inf I),(sup I).[ ; :: thesis: f | ].(inf I),(sup I).[ is_differentiable_in x
then ( inf I < x & x < sup I ) by XXREAL_1:4;
then consider Z being open Subset of REAL such that
A43: ( x in Z & Z c= ].(inf I),(sup I).[ ) by Lm9;
consider N being Neighbourhood of x such that
A44: N c= Z by A43, RCOMP_1:18;
A45: N c= dom (f | ].(inf I),(sup I).[) by A41, A43, A44;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) holds
(h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) holds
(h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent
let c be constant Real_Sequence; :: thesis: ( rng c = {x} & rng (h + c) c= dom (f | ].(inf I),(sup I).[) implies (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent )
assume that
A46: rng c = {x} and
A47: rng (h + c) c= dom (f | ].(inf I),(sup I).[) ; :: thesis: (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent
for p being Real st 0 < p holds
ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p )
assume A48: 0 < p ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p
take N = 0 ; :: thesis: for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p
thus for k being Nat st N <= k holds
|.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p :: thesis: verum

proof

let k be Nat; :: thesis: ( N <= k implies |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p )
assume N <= k ; :: thesis: |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p
A49: rng c c= dom (f | ].(inf I),(sup I).[) by A41, A42, A46, ZFMISC_1:31;
A50: ( (f | ].(inf I),(sup I).[) /* (h + c) = (f | ].(inf I),(sup I).[) * (h + c) & (f | ].(inf I),(sup I).[) /* c = (f | ].(inf I),(sup I).[) * c ) by A47, A41, A42, A46, ZFMISC_1:31, FUNCT_2:def 11;
A51: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( k in dom (h + c) & k in dom c ) by ORDINAL1:def 12;
then ( k in dom ((f | ].(inf I),(sup I).[) * (h + c)) & k in dom ((f | ].(inf I),(sup I).[) * c) ) by A47, A41, A42, A46, ZFMISC_1:31, RELAT_1:27;
then k in (dom ((f | ].(inf I),(sup I).[) * (h + c))) /\ (dom ((f | ].(inf I),(sup I).[) * c)) by XBOOLE_0:def 4;
then A52: k in dom (((f | ].(inf I),(sup I).[) * (h + c)) - ((f | ].(inf I),(sup I).[) * c)) by VALUED_1:12;
A53: ( (h + c) . k in rng (h + c) & c . k in rng c ) by A51, ORDINAL1:def 12, FUNCT_1:3;
then A54: ( (f | ].(inf I),(sup I).[) . ((h + c) . k) = f . ((h + c) . k) & (f | ].(inf I),(sup I).[) . (c . k) = f . (c . k) ) by A49, A47, FUNCT_1:47;
dom (f | ].(inf I),(sup I).[) c= dom f by RELAT_1:60;
then ( f . ((h + c) . k) in rng f & f . (c . k) in rng f ) by A53, A49, A47, FUNCT_1:3;
then A55: ( f . ((h + c) . k) = r & f . (c . k) = r ) by A4, TARSKI:def 1;
((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k = ((h ") . k) * ((((f | ].(inf I),(sup I).[) * (h + c)) - ((f | ].(inf I),(sup I).[) * c)) . k) by A50, VALUED_1:5
.= ((h ") . k) * ((((f | ].(inf I),(sup I).[) * (h + c)) . k) - (((f | ].(inf I),(sup I).[) * c) . k)) by A52, VALUED_1:13
.= ((h ") . k) * (((f | ].(inf I),(sup I).[) . ((h + c) . k)) - (((f | ].(inf I),(sup I).[) * c) . k)) by A51, ORDINAL1:def 12, FUNCT_1:13
.= ((h ") . k) * (((f | ].(inf I),(sup I).[) . ((h + c) . k)) - ((f | ].(inf I),(sup I).[) . (c . k))) by A51, ORDINAL1:def 12, FUNCT_1:13 ;
hence |.((((h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c))) . k) - 0).| < p by A48, A54, A55, COMPLEX1:44; :: thesis: verum

end;

end;

hence (h ") (#) (((f | ].(inf I),(sup I).[) /* (h + c)) - ((f | ].(inf I),(sup I).[) /* c)) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence f | ].(inf I),(sup I).[ is_differentiable_in x by A45, FDIFF_2:11; :: thesis: verum

end;

then f is_differentiable_on ].(inf I),(sup I).[ by A40;
hence A56: f is_differentiable_on_interval I by A1, A2, A5, A22; :: thesis: for x being Real st x in I holds
(f `\ I) . x = 0
thus for x being Real st x in I holds
(f `\ I) . x = 0 :: thesis: verum

proof

let x be Real; :: thesis: ( x in I implies (f `\ I) . x = 0 )
assume A57: x in I ; :: thesis: (f `\ I) . x = 0

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A58: x = inf I ; :: thesis: (f `\ I) . x = 0

then x = lower_bound I by A57, Lm5;
hence (f `\ I) . x = 0 by A56, A5, A57, A58, Def2; :: thesis: verum

end;

suppose A59: x = sup I ; :: thesis: (f `\ I) . x = 0

then x = upper_bound I by A57, Lm6;
hence (f `\ I) . x = 0 by A56, A22, A57, A59, Def2; :: thesis: verum

end;

suppose A60: ( x <> inf I & x <> sup I ) ; :: thesis: (f `\ I) . x = 0

then A61: (f `\ I) . x = diff (f,x) by A56, A57, Def2;
( inf I <= x & x <= sup I ) by A57, XXREAL_2:61, XXREAL_2:62;
then ( inf I < x & x < sup I ) by A60, XXREAL_0:1;
then consider Z being open Subset of REAL such that
A62: ( x in Z & Z c= ].(inf I),(sup I).[ ) by Lm9;
A63: Z c= dom f by A1, A62, A39;
then A64: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) by A3, FDIFF_1:11;
(f `| Z) . x = 0 by A62, A63, A3, FDIFF_1:11;
hence (f `\ I) . x = 0 by A61, A62, A64, FDIFF_1:def 7; :: thesis: verum

end;

end;

end;