let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_differentiable_in x0 holds
f is_Lcontinuous_in x0

let x0 be Real; :: thesis: ( f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0 )
assume A1: f is_left_differentiable_in x0 ; :: thesis:
A2: for a being Real_Sequence st rng a c= () /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) )
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set b = seq_const x0;
let a be Real_Sequence; :: thesis: ( rng a c= () /\ (dom f) & a is convergent & lim a = x0 implies ( f /* a is convergent & f . x0 = lim (f /* a) ) )
assume that
A3: rng a c= () /\ (dom f) and
A4: a is convergent and
A5: lim a = x0 ; :: thesis: ( f /* a is convergent & f . x0 = lim (f /* a) )
consider r being Real such that
A6: 0 < r and
A7: [.(x0 - r),x0.] c= dom f by A1;
consider n0 being Nat such that
A8: for k being Nat st k >= n0 holds
x0 - r < a . k by ;
deffunc H1( Nat) -> set = (a . \$1) - (() . \$1);
consider d being Real_Sequence such that
A9: for n being Nat holds d . n = H1(n) from SEQ_1:sch 1();
A10: d = a - () by ;
then A11: d is convergent by A4;
reconsider c = () ^\ n0 as constant Real_Sequence ;
A12: rng c = {x0}
proof
thus rng c c= {x0} :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in {x0} )
assume x in rng c ; :: thesis: x in {x0}
then consider n being Element of NAT such that
A13: x = (() ^\ n0) . n by FUNCT_2:113;
x = () . (n + n0) by ;
then x = x0 by SEQ_1:57;
hence x in {x0} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng c )
assume x in {x0} ; :: thesis: x in rng c
then A14: x = x0 by TARSKI:def 1;
c . 0 = () . (0 + n0) by NAT_1:def 3
.= x by ;
hence x in rng c by VALUED_0:28; :: thesis: verum
end;
A15: now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g
let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g )

assume A16: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g

reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g

let m be Nat; :: thesis: ( n <= m implies |.(((f /* c) . m) - (f . x0)).| < g )
assume n <= m ; :: thesis: |.(((f /* c) . m) - (f . x0)).| < g
A17: m in NAT by ORDINAL1:def 12;
x0 - r <= x0 by ;
then x0 in [.(x0 - r),x0.] by XXREAL_1:1;
then rng c c= dom f by ;
then |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by
.= |.((f . (() . (m + n0))) - (f . x0)).| by NAT_1:def 3
.= |.((f . x0) - (f . x0)).| by SEQ_1:57
.= 0 by ABSVALUE:2 ;
hence |.(((f /* c) . m) - (f . x0)).| < g by A16; :: thesis: verum
end;
then A18: f /* c is convergent by SEQ_2:def 6;
lim () = () . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
then lim d = x0 - x0 by
.= 0 ;
then A19: lim (d ^\ n0) = 0 by ;
A20: for n being Element of NAT holds
( d . n < 0 & d . n <> 0 )
proof
let n be Element of NAT ; :: thesis: ( d . n < 0 & d . n <> 0 )
A21: d . n = (a . n) - (() . n) by A9;
a . n in rng a by VALUED_0:28;
then a . n in left_open_halfline x0 by ;
then a . n in { r1 where r1 is Real : r1 < x0 } by XXREAL_1:229;
then A22: ex r1 being Real st
( r1 = a . n & r1 < x0 ) ;
then (a . n) - x0 < x0 - x0 by XREAL_1:9;
hence d . n < 0 by ; :: thesis: d . n <> 0
thus d . n <> 0 by ; :: thesis: verum
end;
A23: for n being Nat holds (d ^\ n0) . n < 0
proof
let n be Nat; :: thesis: (d ^\ n0) . n < 0
A24: n + n0 in NAT by ORDINAL1:def 12;
(d ^\ n0) . n = d . (n + n0) by NAT_1:def 3;
hence (d ^\ n0) . n < 0 by ; :: thesis: verum
end;
for n being Nat holds (d ^\ n0) . n <> 0 by A23;
then d ^\ n0 is non-zero by SEQ_1:5;
then reconsider h = d ^\ n0 as non-zero 0 -convergent Real_Sequence by ;
A25: rng a c= dom f by ;
now :: thesis: for n being Element of NAT holds (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
let n be Element of NAT ; :: thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by SEQ_1:7
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by RFUNCT_2:1
.= (f /* (h + c)) . n ; :: thesis: verum
end;
then A26: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;
now :: thesis: for n being Element of NAT holds (h + c) . n = (a ^\ n0) . n
let n be Element of NAT ; :: thesis: (h + c) . n = (a ^\ n0) . n
thus (h + c) . n = (((a - ()) + ()) ^\ n0) . n by
.= ((a - ()) + ()) . (n + n0) by NAT_1:def 3
.= ((a - ()) . (n + n0)) + (() . (n + n0)) by SEQ_1:7
.= ((a . (n + n0)) - (() . (n + n0))) + (() . (n + n0)) by RFUNCT_2:1
.= (a ^\ n0) . n by NAT_1:def 3 ; :: thesis: verum
end;
then A27: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (a ^\ n0) by
.= (f /* a) ^\ n0 by ;
A28: for n being Element of NAT holds (a ^\ n0) . n in [.(x0 - r),x0.]
proof
let n be Element of NAT ; :: thesis: (a ^\ n0) . n in [.(x0 - r),x0.]
a . (n + n0) in rng a by VALUED_0:28;
then (a ^\ n0) . n in rng a by NAT_1:def 3;
then (a ^\ n0) . n in left_open_halfline x0 by ;
then (a ^\ n0) . n in { g where g is Real : g < x0 } by XXREAL_1:229;
then A29: ex g being Real st
( g = (a ^\ n0) . n & g < x0 ) ;
( 0 <= n & 0 + n0 = n0 ) ;
then n0 <= n0 + n by XREAL_1:6;
then x0 - r <= a . (n + n0) by A8;
then x0 - r <= (a ^\ n0) . n by NAT_1:def 3;
then (a ^\ n0) . n in { g where g is Real : ( x0 - r <= g & g <= x0 ) } by A29;
hence (a ^\ n0) . n in [.(x0 - r),x0.] by RCOMP_1:def 1; :: thesis: verum
end;
rng (h + c) c= [.(x0 - r),x0.]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (h + c) or x in [.(x0 - r),x0.] )
assume x in rng (h + c) ; :: thesis: x in [.(x0 - r),x0.]
then consider n being Element of NAT such that
A30: x = (h + c) . n by FUNCT_2:113;
(h + c) . n = (((a - ()) + ()) ^\ n0) . n by
.= ((a - ()) + ()) . (n + n0) by NAT_1:def 3
.= ((a - ()) . (n + n0)) + (() . (n + n0)) by SEQ_1:7
.= ((a . (n + n0)) - (() . (n + n0))) + (() . (n + n0)) by RFUNCT_2:1
.= (a ^\ n0) . n by NAT_1:def 3 ;
hence x in [.(x0 - r),x0.] by ; :: thesis: verum
end;
then rng (h + c) c= dom f by A7;
then A31: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A23, A12;
then A32: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by
.= 0 ;
now :: thesis: for n being Element of NAT holds (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A33: h . n <> 0 by A23;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:8
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:8
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum
end;
then A34: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
then A35: (f /* (h + c)) - (f /* c) is convergent by A31;
then A36: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A18;
hence f /* a is convergent by ; :: thesis: f . x0 = lim (f /* a)
lim (f /* c) = f . x0 by ;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by
.= f . x0 ;
hence f . x0 = lim (f /* a) by ; :: thesis: verum
end;
x0 in dom f
proof
consider r being Real such that
A37: 0 < r and
A38: [.(x0 - r),x0.] c= dom f by A1;
x0 - r <= x0 by ;
then x0 in [.(x0 - r),x0.] by XXREAL_1:1;
hence x0 in dom f by A38; :: thesis: verum
end;
hence f is_Lcontinuous_in x0 by A2; :: thesis: verum