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