let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for x0 being Complex st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Complex; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1: f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
A3: x0 in N by Th7;
now :: thesis: for s1 being Complex_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
A4: 0 < g and
A5: { y where y is Complex : |.(y - x0).| < g } c= N by Def5;
reconsider xx0 = x0 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider s2 = NAT --> xx0 as Complex_Sequence ;
let s1 be Complex_Sequence; :: thesis: ( 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
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Nat holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Nat such that
A10: for m being Nat st l <= m holds
|.((s1 . m) - x0).| < g by A7, A8, A4, COMSEQ_2:def 6;
A11: lim s2 = s2 . 0 by CFCONT_1:28
.= x0 ;
deffunc H1( Nat) -> Element of COMPLEX = In (((s1 . $1) - (s2 . $1)),COMPLEX);
consider s3 being Complex_Sequence such that
A12: for n being Element of NAT holds s3 . n = H1(n) from FUNCT_2:sch 4();
A13: for n being Nat holds s3 . n = (s1 . n) - (s2 . n)
proof
let n be Nat; :: thesis: s3 . n = (s1 . n) - (s2 . n)
n in NAT by ORDINAL1:def 12;
then s3 . n = H1(n) by A12;
hence s3 . n = (s1 . n) - (s2 . n) ; :: thesis: verum
end;
A14: s3 = s1 - s2 by A13, CFCONT_1:1;
A15: s2 is convergent by CFCONT_1:26;
then A16: s3 is convergent by A7, A14;
lim s3 = lim (s1 - s2) by A13, CFCONT_1:1
.= x0 - x0 by A7, A8, A15, A11, COMSEQ_2:26
.= 0c ;
then A17: lim (s3 ^\ l) = 0c by A16, CFCONT_1:21;
reconsider c = s2 ^\ l as constant Complex_Sequence ;
A18: now :: thesis: for n being Element of NAT holds not s3 . n = 0c
given n being Element of NAT such that A19: s3 . n = 0c ; :: thesis: contradiction
(s1 . n) - (s2 . n) = 0c by A13, A19;
hence contradiction by A9; :: thesis: verum
end;
A20: now :: thesis: for n being Element of NAT holds not (s3 ^\ l) . n = 0c
given n being Element of NAT such that A21: (s3 ^\ l) . n = 0c ; :: thesis: contradiction
A22: n + l in NAT by ORDINAL1:def 12;
s3 . (n + l) = 0c by A21, NAT_1:def 3;
hence contradiction by A18, A22; :: thesis: verum
end;
then A23: s3 ^\ l is non-zero by COMSEQ_1:4;
s3 ^\ l is convergent by A16, CFCONT_1:21;
then reconsider h = s3 ^\ l as non-zero 0 -convergent Complex_Sequence by A17, A23, Def1;
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 VALUED_1:1
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by CFCONT_1:1
.= (f /* (h + c)) . n ; :: thesis: verum
end;
then A24: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) ;
now :: thesis: for n being Element of NAT holds (h + c) . n = (s1 ^\ l) . n
let n be Element of NAT ; :: thesis: (h + c) . n = (s1 ^\ l) . n
A25: n + l in NAT by ORDINAL1:def 12;
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A14, Th18
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1, A25
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1
.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum
end;
then A26: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A24, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;
A27: rng c = {x0}
proof
thus rng c c= {x0} :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in {x0} )
assume y in rng c ; :: thesis: y in {x0}
then consider n being Element of NAT such that
A28: y = (s2 ^\ l) . n by FUNCT_2:113;
A29: n + l in NAT by ORDINAL1:def 12;
y = s2 . (n + l) by A28, NAT_1:def 3;
then y = x0 by FUNCOP_1:7, A29;
hence y in {x0} by TARSKI:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x0} or y in rng c )
assume y in {x0} ; :: thesis: y in rng c
then A30: y = x0 by TARSKI:def 1;
A31: 0 + l in NAT by ORDINAL1:def 12;
c . 0 = s2 . (0 + l) by NAT_1:def 3
.= y by A30, FUNCOP_1:7, A31 ;
hence y in rng c by FUNCT_2:4; :: thesis: verum
end;
A32: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p )
assume A33: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p
thus for m being Nat st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p :: thesis: verum
proof
let m be Nat; :: thesis: ( n <= m implies |.(((f /* c) . m) - (f /. x0)).| < p )
assume n <= m ; :: thesis: |.(((f /* c) . m) - (f /. x0)).| < p
A34: m + l in NAT by ORDINAL1:def 12;
A35: m in NAT by ORDINAL1:def 12;
{x0} c= dom f by A2, A3, ZFMISC_1:31;
then |.(((f /* c) . m) - (f /. x0)).| = |.((f /. (c . m)) - (f /. x0)).| by A27, FUNCT_2:109, A35
.= |.((f /. (s2 . (m + l))) - (f /. x0)).| by NAT_1:def 3
.= |.((f /. x0) - (f /. x0)).| by FUNCOP_1:7, A34
.= 0 by ABSVALUE:2 ;
hence |.(((f /* c) . m) - (f /. x0)).| < p by A33; :: thesis: verum
end;
end;
then A36: f /* c is convergent ;
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
A37: h . n <> 0 by A20;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by VALUED_1:5
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:5
.= (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 A37, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum
end;
then A38: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) ;
rng (h + c) c= N
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in N )
assume A39: y in rng (h + c) ; :: thesis: y in N
then consider n being Element of NAT such that
A40: y = (h + c) . n by FUNCT_2:113;
A41: n + l in NAT by ORDINAL1:def 12;
reconsider y1 = y as Complex by A39;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A14, Th18
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1, A41
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1
.= s1 . (l + n) ;
then |.(((h + c) . n) - x0).| < g by A10, NAT_1:12;
then y1 in { z where z is Complex : |.(z - x0).| < g } by A40;
hence y in N by A5; :: thesis: verum
end;
then A42: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A27, Th22;
then A43: (f /* (h + c)) - (f /* c) is convergent by A38;
then A44: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A36;
hence f /* s1 is convergent by A26, CFCONT_1:22; :: thesis: f /. x0 = lim (f /* s1)
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0c * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A17, A42, COMSEQ_2:30
.= 0 ;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0c + (lim (f /* c)) by A38, A43, A36, COMSEQ_2:14
.= f /. x0 by A32, A36, COMSEQ_2:def 6 ;
hence f /. x0 = lim (f /* s1) by A44, A26, CFCONT_1:23; :: thesis: verum
end;
hence f is_continuous_in x0 by A2, A3, CFCONT_1:31; :: thesis: verum