let f be PartFunc of REAL,REAL; for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Real; ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1:
f is_differentiable_in x0
; f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2:
N c= dom f
and
ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
;
now for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) )consider g being
Real such that A3:
0 < g
and A4:
N = ].(x0 - g),(x0 + g).[
by RCOMP_1:def 6;
set s2 =
seq_const x0;
let s1 be
Real_Sequence;
( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )assume that A5:
rng s1 c= dom f
and A6:
s1 is
convergent
and A7:
lim s1 = x0
and A8:
for
n being
Nat holds
s1 . n <> x0
;
( f /* s1 is convergent & f . x0 = lim (f /* s1) )consider l being
Nat such that A9:
for
m being
Nat st
l <= m holds
|.((s1 . m) - x0).| < g
by A6, A7, A3, SEQ_2:def 7;
reconsider c =
(seq_const x0) ^\ l as
V8()
Real_Sequence ;
deffunc H1(
Nat)
-> set =
(s1 . $1) - ((seq_const x0) . $1);
consider s3 being
Real_Sequence such that A10:
for
n being
Nat holds
s3 . n = H1(
n)
from SEQ_1:sch 1();
A11:
s3 = s1 - (seq_const x0)
by A10, RFUNCT_2:1;
then A12:
s3 is
convergent
by A6;
A13:
rng c = {x0}
then A20:
f /* c is
convergent
by SEQ_2:def 6;
lim (seq_const x0) =
(seq_const x0) . 0
by SEQ_4:26
.=
x0
by SEQ_1:57
;
then lim s3 =
x0 - x0
by A6, A7, A11, SEQ_2:12
.=
0
;
then A21:
lim (s3 ^\ l) = 0
by A12, SEQ_4:20;
A22:
now for n being Nat holds not s3 . n = 0 end; A24:
now for n being Nat holds not (s3 ^\ l) . n = 0 end;
s3 ^\ l is
0 -convergent
by A12, A21;
then reconsider h =
s3 ^\ l as
non-zero 0 -convergent Real_Sequence by A24, SEQ_1:5;
then A26:
((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c)
by FUNCT_2:63;
then A27:
((f /* (h + c)) - (f /* c)) + (f /* c) =
f /* (s1 ^\ l)
by A26, FUNCT_2:63
.=
(f /* s1) ^\ l
by A5, VALUED_0:27
;
rng (h + c) c= N
then A29:
(h ") (#) ((f /* (h + c)) - (f /* c)) is
convergent
by A1, A2, A13, Th12;
then A30:
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) =
0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c))))
by A21, SEQ_2:15
.=
0
;
then A32:
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c)
by FUNCT_2:63;
then A33:
(f /* (h + c)) - (f /* c) is
convergent
by A29;
then A34:
((f /* (h + c)) - (f /* c)) + (f /* c) is
convergent
by A20;
hence
f /* s1 is
convergent
by A27, SEQ_4:21;
f . x0 = lim (f /* s1)
lim (f /* c) = f . x0
by A17, A20, SEQ_2:def 7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) =
0 + (f . x0)
by A30, A32, A33, A20, SEQ_2:6
.=
f . x0
;
hence
f . x0 = lim (f /* s1)
by A34, A27, SEQ_4:22;
verum end;
hence
f is_continuous_in x0
by FCONT_1:2; verum