let f be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff f,x0 = Ldiff f,x0 holds
( f is_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 )
let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff f,x0 = Ldiff f,x0 implies ( f is_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 ) )
assume A1: ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff f,x0 = Ldiff f,x0 ) ; :: thesis: ( f is_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 )
A2: ex N being Neighbourhood of x0 st N c= dom f
proof
consider r1 being Real such that
A3: ( r1 > 0 & [.(x0 - r1),x0.] c= dom f ) by A1, Def4;
consider r2 being Real such that
A4: ( r2 > 0 & [.x0,(x0 + r2).] c= dom f ) by A1, Def3;
set r = min r1,r2;
min r1,r2 > 0 by A3, A4, XXREAL_0:15;
then reconsider N = ].(x0 - (min r1,r2)),(x0 + (min r1,r2)).[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N ; :: thesis: N c= dom f
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom f )
assume x in N ; :: thesis: x in dom f
then x in { g where g is Real : ( x0 - (min r1,r2) < g & g < x0 + (min r1,r2) ) } by RCOMP_1:def 2;
then consider g being Real such that
A5: ( g = x & x0 - (min r1,r2) < g & g < x0 + (min r1,r2) ) ;
now
per cases ( g <= x0 or g > x0 ) ;
suppose A6: g <= x0 ; :: thesis: x in dom f
min r1,r2 <= r1 by XXREAL_0:17;
then x0 - r1 <= x0 - (min r1,r2) by XREAL_1:15;
then x0 - r1 <= g by A5, XXREAL_0:2;
then g in { g1 where g1 is Real : ( x0 - r1 <= g1 & g1 <= x0 ) } by A6;
then g in [.(x0 - r1),x0.] by RCOMP_1:def 1;
hence x in dom f by A3, A5; :: thesis: verum
end;
suppose A7: g > x0 ; :: thesis: x in dom f
min r1,r2 <= r2 by XXREAL_0:17;
then x0 + (min r1,r2) <= x0 + r2 by XREAL_1:9;
then g <= x0 + r2 by A5, XXREAL_0:2;
then g in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r2 ) } by A7;
then g in [.x0,(x0 + r2).] by RCOMP_1:def 1;
hence x in dom f by A4, A5; :: thesis: verum
end;
end;
end;
hence x in dom f ; :: thesis: verum
end;
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
proof
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
let c be V6 Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 ) )
assume A8: ( rng c = {x0} & rng (h + c) c= dom f ) ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
A9: rng c c= dom f
proof
consider S being Neighbourhood of x0 such that
A10: S c= dom f by A2;
x0 in S by RCOMP_1:37;
hence rng c c= dom f by A8, A10, ZFMISC_1:37; :: thesis: verum
end;
now
per cases ( ex N being Element of NAT st
for n being Element of NAT st n >= N holds
h . n > 0 or for N being Element of NAT ex n being Element of NAT st
( n >= N & h . n <= 0 ) ) ;
suppose ex N being Element of NAT st
for n being Element of NAT st n >= N holds
h . n > 0 ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
then consider N being Element of NAT such that
A11: for n being Element of NAT st n >= N holds
h . n > 0 ;
set h1 = h ^\ N;
set c1 = c ^\ N;
A12: rng (c ^\ N) = {x0}
proof
thus rng (c ^\ N) c= {x0} by A8, VALUED_0:21; :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng (c ^\ N)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng (c ^\ N) )
assume x in {x0} ; :: thesis: x in rng (c ^\ N)
then A13: x = x0 by TARSKI:def 1;
A14: (c ^\ N) . 0 = c . (0 + N) by NAT_1:def 3
.= c . N ;
c . N in rng c by VALUED_0:28;
then (c ^\ N) . 0 = x by A8, A13, A14, TARSKI:def 1;
hence x in rng (c ^\ N) by VALUED_0:28; :: thesis: verum
end;
A15: (h ^\ N) + (c ^\ N) = (h + c) ^\ N by SEQM_3:37;
then rng ((h ^\ N) + (c ^\ N)) c= rng (h + c) by VALUED_0:21;
then A16: rng ((h ^\ N) + (c ^\ N)) c= dom f by A8, XBOOLE_1:1;
for n being Element of NAT holds (h ^\ N) . n > 0
proof
let n be Element of NAT ; :: thesis: (h ^\ N) . n > 0
A17: (h ^\ N) . n = h . (n + N) by NAT_1:def 3;
0 <= n by NAT_1:2;
then N + 0 <= n + N by XREAL_1:9;
hence (h ^\ N) . n > 0 by A11, A17; :: thesis: verum
end;
then A18: ( ((h ^\ N) " ) (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) is convergent & lim (((h ^\ N) " ) (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N)))) = Rdiff f,x0 ) by A1, A12, A16, Th15;
A19: ((h ^\ N) " ) (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) = ((h ^\ N) " ) (#) (((f /* (h + c)) ^\ N) - (f /* (c ^\ N))) by A8, A15, VALUED_0:27
.= ((h ^\ N) " ) (#) (((f /* (h + c)) ^\ N) - ((f /* c) ^\ N)) by A9, VALUED_0:27
.= ((h ^\ N) " ) (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:39
.= ((h " ) ^\ N) (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:41
.= ((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ N by SEQM_3:42 ;
hence (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A18, SEQ_4:35; :: thesis: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0
thus lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 by A1, A18, A19, SEQ_4:36; :: thesis: verum
end;
suppose A20: for N being Element of NAT ex n being Element of NAT st
( n >= N & h . n <= 0 ) ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
now
per cases ( ex M being Element of NAT st
for m being Element of NAT st m >= M holds
h . m < 0 or for M being Element of NAT ex m being Element of NAT st
( m >= M & h . m >= 0 ) ) ;
suppose ex M being Element of NAT st
for m being Element of NAT st m >= M holds
h . m < 0 ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
then consider M being Element of NAT such that
A21: for n being Element of NAT st n >= M holds
h . n < 0 ;
set h1 = h ^\ M;
set c1 = c ^\ M;
A22: rng (c ^\ M) = {x0}
proof
thus rng (c ^\ M) c= {x0} by A8, VALUED_0:21; :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng (c ^\ M)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng (c ^\ M) )
assume x in {x0} ; :: thesis: x in rng (c ^\ M)
then A23: x = x0 by TARSKI:def 1;
A24: (c ^\ M) . 0 = c . (0 + M) by NAT_1:def 3
.= c . M ;
c . M in rng c by VALUED_0:28;
then (c ^\ M) . 0 = x by A8, A23, A24, TARSKI:def 1;
hence x in rng (c ^\ M) by VALUED_0:28; :: thesis: verum
end;
A25: (h ^\ M) + (c ^\ M) = (h + c) ^\ M by SEQM_3:37;
then rng ((h ^\ M) + (c ^\ M)) c= rng (h + c) by VALUED_0:21;
then A26: rng ((h ^\ M) + (c ^\ M)) c= dom f by A8, XBOOLE_1:1;
for n being Element of NAT holds (h ^\ M) . n < 0
proof
let n be Element of NAT ; :: thesis: (h ^\ M) . n < 0
A27: (h ^\ M) . n = h . (n + M) by NAT_1:def 3;
0 <= n by NAT_1:2;
then M + 0 <= n + M by XREAL_1:9;
hence (h ^\ M) . n < 0 by A21, A27; :: thesis: verum
end;
then A28: ( ((h ^\ M) " ) (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) is convergent & lim (((h ^\ M) " ) (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M)))) = Ldiff f,x0 ) by A1, A22, A26, Th9;
A29: ((h ^\ M) " ) (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) = ((h ^\ M) " ) (#) (((f /* (h + c)) ^\ M) - (f /* (c ^\ M))) by A8, A25, VALUED_0:27
.= ((h ^\ M) " ) (#) (((f /* (h + c)) ^\ M) - ((f /* c) ^\ M)) by A9, VALUED_0:27
.= ((h ^\ M) " ) (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:39
.= ((h " ) ^\ M) (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:41
.= ((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ M by SEQM_3:42 ;
hence (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A28, SEQ_4:35; :: thesis: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0
thus lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 by A28, A29, SEQ_4:36; :: thesis: verum
end;
suppose A30: for M being Element of NAT ex m being Element of NAT st
( m >= M & h . m >= 0 ) ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 )
A31: ( h is non-zero & h is convergent & lim h = 0 ) by FDIFF_1:def 1;
defpred S1[ real number ] means $1 < 0 ;
defpred S2[ real number ] means $1 > 0 ;
A32: for N being Element of NAT ex n being Element of NAT st
( n >= N & S1[h . n] )
proof
let m be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= m & S1[h . n] )
consider n being Element of NAT such that
A33: ( n >= m & h . n <= 0 ) by A20;
take n ; :: thesis: ( n >= m & S1[h . n] )
thus n >= m by A33; :: thesis: S1[h . n]
h . n <> 0 by A31, SEQ_1:7;
hence S1[h . n] by A33; :: thesis: verum
end;
A34: for N being Element of NAT ex n being Element of NAT st
( n >= N & S2[h . n] )
proof
let m be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= m & S2[h . n] )
consider n being Element of NAT such that
A35: ( n >= m & h . n >= 0 ) by A30;
take n ; :: thesis: ( n >= m & S2[h . n] )
thus n >= m by A35; :: thesis: S2[h . n]
h . n <> 0 by A31, SEQ_1:7;
hence S2[h . n] by A35; :: thesis: verum
end;
consider q1 being V32 sequence of NAT such that
A36: ( ( for n being Element of NAT holds S1[(h * q1) . n] ) & ( for n being Element of NAT st ( for r being Real st r = h . n holds
S1[r] ) holds
ex m being Element of NAT st n = q1 . m ) ) from FDIFF_2:sch 1(A32);
consider q2 being V32 sequence of NAT such that
A37: ( ( for n being Element of NAT holds S2[(h * q2) . n] ) & ( for n being Element of NAT st ( for r being Real st r = h . n holds
S2[r] ) holds
ex m being Element of NAT st n = q2 . m ) ) from FDIFF_2:sch 1(A34);
set h1 = h * q1;
set h2 = h * q2;
set c1 = c * q1;
set c2 = c * q2;
reconsider h1 = h * q1 as subsequence of h ;
A39: h1 is convergent by A31, SEQ_4:29;
A40: lim h1 = 0 by A31, SEQ_4:30;
h1 is non-zero by A31;
then reconsider h1 = h1 as convergent_to_0 Real_Sequence by A39, A40, FDIFF_1:def 1;
A42: h * q2 is convergent by A31, SEQ_4:29;
A43: lim (h * q2) = 0 by A31, SEQ_4:30;
h * q2 is non-zero by A31;
then reconsider h2 = h * q2 as convergent_to_0 Real_Sequence by A42, A43, FDIFF_1:def 1;
A46: rng (c * q1) = {x0} by A8, VALUED_0:26;
reconsider c1 = c * q1 as V6 Real_Sequence ;
rng ((h + c) * q1) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * q1) c= dom f by A8, XBOOLE_1:1;
then rng (h1 + c1) c= dom f by RFUNCT_2:13;
then A47: ( (h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)) is convergent & lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) = Ldiff f,x0 ) by A1, A36, A46, Th9;
A48: rng (c * q2) = {x0} by A8, VALUED_0:26;
reconsider c2 = c * q2 as V6 Real_Sequence ;
rng ((h + c) * q2) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * q2) c= dom f by A8, XBOOLE_1:1;
then rng (h2 + c2) c= dom f by RFUNCT_2:13;
then A49: ( (h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2)) is convergent & lim ((h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2))) = Ldiff f,x0 ) by A1, A37, A48, Th15;
A50: (h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)) = (h1 " ) (#) ((f /* ((h + c) * q1)) - (f /* c1)) by RFUNCT_2:13
.= (h1 " ) (#) (((f /* (h + c)) * q1) - (f /* c1)) by A8, FUNCT_2:187
.= ((h " ) * q1) (#) (((f /* (h + c)) * q1) - (f /* c1)) by RFUNCT_2:16
.= ((h " ) * q1) (#) (((f /* (h + c)) * q1) - ((f /* c) * q1)) by A9, FUNCT_2:187
.= ((h " ) * q1) (#) (((f /* (h + c)) - (f /* c)) * q1) by RFUNCT_2:13
.= ((h " ) (#) ((f /* (h + c)) - (f /* c))) * q1 by RFUNCT_2:13 ;
A51: (h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2)) = (h2 " ) (#) ((f /* ((h + c) * q2)) - (f /* c2)) by RFUNCT_2:13
.= (h2 " ) (#) (((f /* (h + c)) * q2) - (f /* c2)) by A8, FUNCT_2:187
.= ((h " ) * q2) (#) (((f /* (h + c)) * q2) - (f /* c2)) by RFUNCT_2:16
.= ((h " ) * q2) (#) (((f /* (h + c)) * q2) - ((f /* c) * q2)) by A9, FUNCT_2:187
.= ((h " ) * q2) (#) (((f /* (h + c)) - (f /* c)) * q2) by RFUNCT_2:13
.= ((h " ) (#) ((f /* (h + c)) - (f /* c))) * q2 by RFUNCT_2:13 ;
set s = (h " ) (#) ((f /* (h + c)) - (f /* c));
A52: for g1 being real number st 0 < g1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
proof
let g1 be real number ; :: thesis: ( 0 < g1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1 )
assume A53: 0 < g1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
then consider n1 being Element of NAT such that
A54: for m being Element of NAT st n1 <= m holds
abs (((((h " ) (#) ((f /* (h + c)) - (f /* c))) * q1) . m) - (Ldiff f,x0)) < g1 by A47, A50, SEQ_2:def 7;
consider n2 being Element of NAT such that
A55: for m being Element of NAT st n2 <= m holds
abs (((((h " ) (#) ((f /* (h + c)) - (f /* c))) * q2) . m) - (Ldiff f,x0)) < g1 by A49, A51, A53, SEQ_2:def 7;
take n = max (q1 . n1),(q2 . n2); :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1 )
assume A56: n <= m ; :: thesis: abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
A57: ( n >= q1 . n1 & n >= q2 . n2 ) by XXREAL_0:25;
now
per cases ( h . m > 0 or h . m <= 0 ) ;
suppose h . m > 0 ; :: thesis: abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
then for r being Real st r = h . m holds
r > 0 ;
then consider k being Element of NAT such that
A58: m = q2 . k by A37;
X: dom q2 = NAT by FUNCT_2:def 1;
q2 . k >= q2 . n2 by A56, A57, A58, XXREAL_0:2;
then not k < n2 by X, VALUED_0:def 13;
then abs (((((h " ) (#) ((f /* (h + c)) - (f /* c))) * q2) . k) - (Ldiff f,x0)) < g1 by A55;
hence abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1 by A58, FUNCT_2:21; :: thesis: verum
end;
suppose A59: h . m <= 0 ; :: thesis: abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1
h . m <> 0 by A31, SEQ_1:7;
then for r being Real st r = h . m holds
r < 0 by A59;
then consider k being Element of NAT such that
A60: m = q1 . k by A36;
X: dom q1 = NAT by FUNCT_2:def 1;
q1 . k >= q1 . n1 by A56, A57, A60, XXREAL_0:2;
then not k < n1 by X, VALUED_0:def 13;
then abs (((((h " ) (#) ((f /* (h + c)) - (f /* c))) * q1) . k) - (Ldiff f,x0)) < g1 by A54;
hence abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1 by A60, FUNCT_2:21; :: thesis: verum
end;
end;
end;
hence abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff f,x0)) < g1 ; :: thesis: verum
end;
hence (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0
hence lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 by A52, SEQ_2:def 7; :: thesis: verum
end;
end;
end;
hence ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 ) ; :: thesis: verum
end;
end;
end;
hence ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 ) ; :: thesis: verum
end;
hence ( f is_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 ) by A1, A2, FDIFF_2:12; :: thesis: verum