:: Complex Function Differentiability
:: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received November 4, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, XCMPLX_0, COMSEQ_1, PARTFUN1,
ORDINAL2, NAT_1, FDIFF_1, VALUED_0, SEQ_2, CARD_1, SEQ_1, FUNCT_1,
COMPLEX1, RELAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FUNCOP_1, VALUED_1,
FUNCT_2, TARSKI, RCOMP_1, XBOOLE_0, FCONT_1, CFCONT_1, XXREAL_2,
CFDIFF_1, FUNCT_7, ASYMPT_1;
notations TARSKI, SUBSET_1, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1,
SEQ_1, RELSET_1, SEQ_2, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, CFCONT_1,
XXREAL_0;
constructors PARTFUN1, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_2, FINSEQ_4,
SEQM_3, PARTFUN2, SQUARE_1, COMSEQ_2, COMSEQ_3, CFCONT_1, XXREAL_0,
CFUNCT_1, RELSET_1, SEQ_1;
registrations FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, NUMBERS, ORDINAL1,
XREAL_0, XXREAL_0, COMSEQ_2, NAT_1, VALUED_0, VALUED_1, FUNCOP_1,
XCMPLX_0, SEQ_2, CFUNCT_1, SEQ_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI, COMSEQ_2, CFCONT_1, FUNCT_2;
equalities XCMPLX_0, XBOOLE_0, SUBSET_1, VALUED_1, COMPLEX1;
expansions XBOOLE_0, TARSKI, COMSEQ_2, FUNCT_2;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, COMPLEX1, SEQ_1, SEQ_2,
SEQ_4, COMSEQ_1, COMSEQ_2, CFUNCT_1, CFCONT_1, RELAT_1, XBOOLE_0,
XBOOLE_1, PARTFUN1, PARTFUN2, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0,
ORDINAL1, ABSVALUE, XREAL_0, FUNCOP_1, SUBSET_1, VALUED_1, VALUED_0;
schemes SEQ_1, COMSEQ_1, FUNCT_2;
begin
reserve k, k1, n, n1, m for Nat;
reserve X, y for set;
reserve p for Real;
reserve r for Real;
reserve a, a1, a2, b, b1, b2, x, x0, z, z0 for Complex;
reserve s1, s3, seq, seq1 for Complex_Sequence;
reserve Y for Subset of COMPLEX;
reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX;
reserve Nseq for increasing sequence of NAT;
definition
let x be Real;
let IT be Complex_Sequence;
attr IT is x-convergent means :Def1:
IT is convergent & lim IT = x;
end;
theorem
for rs be Real_Sequence, cs be Complex_Sequence st rs = cs & rs is
convergent holds cs is convergent;
definition
let r be Real;
func InvShift(r) -> Complex_Sequence means
:Def2:
for n holds it.n = 1/(n+r);
existence
proof
deffunc F(Real) = 1/($1+r);
ex seq st for n holds seq.n = F(n) from COMSEQ_1:sch 1;
hence thesis;
end;
uniqueness
proof
let f, g be Complex_Sequence such that
A1: for n holds f.n = 1/(n+r) and
A2: for n holds g.n = 1/(n+r);
let n be Element of NAT;
thus f.n = 1/(n+r) by A1
.= g.n by A2;
end;
end;
theorem Th2:
0 < r implies InvShift(r) is convergent
proof
assume
A1: 0 < r;
set seq = InvShift(r);
take g = 0c;
let p;
assume
A2: 0 < p;
consider k1 such that
A3: p" < k1 by SEQ_4:3;
take n = k1;
let m;
assume n <= m;
then n+r <= m+r by XREAL_1:6;
then
A4: 1/(m+r) <= 1/(n+r) by A1,XREAL_1:118;
A5: seq.m = 1/(m+r) by Def2;
(p") + 0 < k1+r by A1,A3,XREAL_1:8;
then 1/(k1+r) < 1/p" by A2,XREAL_1:76;
then 1/(m+r) < p by A4,XXREAL_0:2;
hence |.seq.m-g.| < p by A1,A5,ABSVALUE:def 1;
end;
registration
let r be positive Real;
cluster InvShift(r) -> convergent;
coherence by Th2;
end;
theorem Th3:
0 < r implies lim InvShift(r) = 0
proof
set seq = InvShift(r);
assume
A1: 0 < r;
now
let p;
assume
A2: 0 < p;
consider k1 such that
A3: p" < k1 by SEQ_4:3;
take n = k1;
let m;
assume n <= m;
then n+r <= m+r by XREAL_1:6;
then
A4: 1/(m+r) <= 1/(n+r) by A1,XREAL_1:118;
A5: seq.m = 1/(m+r) by Def2;
p"+ 0 < k1 + r by A1,A3,XREAL_1:8;
then 1/(k1+r) < 1/p" by A2,XREAL_1:76;
then 1/(m+r) < p by A4,XXREAL_0:2;
hence |.seq.m-0c.| < p by A1,A5,ABSVALUE:def 1;
end;
hence thesis by A1,COMSEQ_2:def 6;
end;
registration
let r be positive Real;
cluster InvShift(r) -> non-zero 0-convergent;
coherence
proof
set s = InvShift(r);
now
let n be Element of NAT;
1/(n+r) <> 0;
hence s.n <> 0c by Def2;
end;
hence s is non-zero by COMSEQ_1:4;
lim s = 0 by Th3;
hence thesis;
end;
end;
registration
cluster 0-convergent non-zero for Complex_Sequence;
existence
proof
take InvShift(1);
thus thesis;
end;
end;
registration
cluster 0-convergent non-zero -> convergent for Complex_Sequence;
coherence;
end;
registration
cluster constant for Complex_Sequence;
existence
proof
reconsider cs = NAT --> 0c as Complex_Sequence;
take cs;
thus thesis;
end;
end;
theorem
seq is constant iff for n,m holds seq.n = seq.m
proof
thus seq is constant implies for n,m holds seq.n = seq.m by VALUED_0:23;
assume that
A1: for n,m holds seq.n = seq.m and
A2: seq is non constant;
now
let n be Nat;
consider n1 be Nat such that
A3: seq.n1 <> seq.n by A2,VALUED_0:def 18;
thus contradiction by A1,A3;
end;
hence thesis;
end;
theorem
for n holds (seq*Nseq).n = seq.(Nseq.n)
proof
let n;
A1: n in NAT by ORDINAL1:def 12;
dom (seq*Nseq) = NAT by FUNCT_2:def 1;
hence thesis by FUNCT_1:12,A1;
end;
reserve h for 0-convergent non-zero Complex_Sequence;
reserve c for constant Complex_Sequence;
definition
let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is RestFunc-like means
:Def3:
for h holds (h")(#)(IT/*h) is convergent & lim ((h")(#)(IT/*h)) = 0;
end;
registration
cluster total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
existence
proof
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX;
take f = cf;
thus f is total;
let h;
now
let n be Nat;
A1: n in NAT & rng h c= dom f by ORDINAL1:def 12;
thus ((h")(#)(f/*h)).n = (h").n*((f/*h).n) by VALUED_1:5
.= (h").n*(f/.(h.n)) by A1,FUNCT_2:108
.= (h").n*0c
.= 0c;
end;
then (h")(#)(f/*h) is constant & ((h")(#)(f/*h)).0 = 0c by VALUED_0:def 18;
hence (h")(#)(f/*h) is convergent & lim ((h")(#)(f/*h)) = 0c by CFCONT_1:26
,27;
end;
end;
definition
mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX,COMPLEX;
end;
definition
let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is linear means
:Def4:
ex a st for z holds IT/.z = a*z;
end;
registration
cluster total linear for PartFunc of COMPLEX,COMPLEX;
existence
proof
deffunc F(Complex) = In(1r*$1,COMPLEX);
defpred P[set] means $1 in COMPLEX;
consider f such that
A1: (for a be Element of COMPLEX holds a in dom f iff P[a]) &
for a being Element of COMPLEX st a in dom f
holds f.a = F(a) from SEQ_1:sch 3;
take f;
for y being object holds y in COMPLEX implies y in dom f by A1;
then COMPLEX c= dom f;
then
A2: dom f = COMPLEX;
hence f is total by PARTFUN1:def 2;
take 1r;
let z;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
f/.z = f.z by A2,PARTFUN1:def 6
.= F(z) by A1;
hence thesis;
end;
end;
definition
mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX;
end;
reserve R, R1, R2 for C_RestFunc;
reserve L, L1, L2 for C_LinearFunc;
registration
let L1,L2;
cluster L1+L2 -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
proof
consider a2 such that
A1: for z holds L2/.z = a2*z by Def4;
consider a1 such that
A2: for z holds L1/.z = a1*z by Def4;
now
let z;
z in COMPLEX by XCMPLX_0:def 2;
hence (L1+L2)/.z = L1/.z+L2/.z by CFUNCT_1:64
.= a1*z+L2/.z by A2
.= a1*z+a2*z by A1
.= (a1+a2)*z;
end;
hence thesis;
end;
cluster L1-L2 -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
proof
consider a2 such that
A3: for z holds L2/.z = a2*z by Def4;
consider a1 such that
A4: for z holds L1/.z = a1*z by Def4;
now
let z;
z in COMPLEX by XCMPLX_0:def 2;
hence (L1-L2)/.z = L1/.z-L2/.z by CFUNCT_1:64
.= a1*z-L2/.z by A4
.= a1*z-a2*z by A3
.= (a1-a2)*z;
end;
hence thesis;
end;
end;
registration
let a,L;
cluster a(#)L -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
proof
consider b such that
A1: for z holds L/.z = b*z by Def4;
now
let z;
z in COMPLEX by XCMPLX_0:def 2;
hence (a(#)L)/.z = a*L/.z by CFUNCT_1:65
.= a*(b*z) by A1
.= a*b*z;
end;
hence thesis;
end;
end;
registration
let R1,R2;
cluster R1+R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
now
let h;
A1: (h")(#)((R1+R2)/*h) = (h")(#)((R1/*h)+(R2/*h)) by CFCONT_1:14
.= ((h")(#)(R1/*h))+((h")(#)(R2/*h)) by COMSEQ_1:10;
A2: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def3;
hence (h")(#)((R1+R2)/*h) is convergent by A1;
A3: lim ((h")(#)(R1/*h)) = 0 by Def3;
thus lim ((h")(#)((R1+R2)/*h)) =lim ((h")(#)(R1/*h)) + lim ((h")(#)(R2/*
h)) by A2,A1,COMSEQ_2:14
.= 0 by A3,Def3;
end;
hence thesis;
end;
cluster R1-R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
now
let h;
A4: (h")(#)((R1-R2)/*h) = (h")(#)((R1/*h)-(R2/*h)) by CFCONT_1:14
.= ((h")(#)(R1/*h))-((h")(#)(R2/*h)) by COMSEQ_1:15;
A5: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def3;
hence (h")(#)((R1-R2)/*h) is convergent by A4;
lim ((h")(#)(R1/*h)) = 0c & lim ((h")(#)(R2/*h)) = 0c by Def3;
hence lim ((h")(#)((R1-R2)/*h)) = 0c-0c by A5,A4,COMSEQ_2:26
.= 0c;
end;
hence thesis;
end;
cluster R1(#)R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
now
let h;
seq is non-zero implies seq" is non-zero
proof
assume that
A6: seq is non-zero and
A7: not seq" is non-zero;
consider n1 be Element of NAT such that
A8: (seq").n1 = 0c by A7,COMSEQ_1:4;
(seq.n1)" = (seq").n1 by VALUED_1:10;
hence contradiction by A6,A8,COMSEQ_1:4,XCMPLX_1:202;
end;
then
A9: h" is non-zero;
A10: (h")(#)((R1(#)R2)/*h) = ((R1/*h)(#)(R2/*h))/"h by CFCONT_1:14
.= ((R1/*h)(#)(R2/*h)(#)(h"))/"(h(#)(h")) by A9,COMSEQ_1:37
.= ((R1/*h)(#)(R2/*h)(#)(h"))(#)((h"")(#)(h")) by COMSEQ_1:30
.= h(#)(h")(#)((R1/*h)(#)((h")(#)(R2/*h))) by COMSEQ_1:8
.= h(#)(h")(#)(R1/*h)(#)((h")(#)(R2/*h)) by COMSEQ_1:8
.= h(#)((h")(#)(R1/*h))(#)((h")(#)(R2/*h)) by COMSEQ_1:8;
A11: (h")(#)(R1/*h) is convergent by Def3;
then
A12: h(#)((h")(#)(R1/*h)) is convergent;
lim ((h")(#)(R1/*h)) = 0c & lim h = 0c by Def1,Def3;
then
A13: lim (h(#)((h")(#)(R1/*h))) = 0*0 by A11,COMSEQ_2:30
.= 0c;
A14: (h")(#)(R2/*h) is convergent by Def3;
hence (h")(#)((R1(#)R2)/*h) is convergent by A12,A10;
lim ((h")(#)(R2/*h)) = 0c by Def3;
hence lim ((h")(#)((R1(#)R2)/*h)) = 0c*0c by A14,A12,A13,A10,COMSEQ_2:30
.= 0c;
end;
hence thesis;
end;
end;
registration
let a,R;
cluster a(#)R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
now
let h;
A1: (h")(#)((a(#)R)/*h) = (h")(#)(a(#)(R/*h)) by CFCONT_1:15
.= a(#)((h")(#)(R/*h)) by COMSEQ_1:13;
A2: (h")(#)(R/*h) is convergent by Def3;
hence (h")(#)((a(#)R)/*h) is convergent by A1;
lim ((h")(#)(R/*h)) = 0c by Def3;
hence lim ((h")(#)((a(#)R)/*h)) = a*0c by A2,A1,COMSEQ_2:18
.= 0c;
end;
hence thesis;
end;
end;
registration
let L1,L2;
cluster L1(#)L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
reconsider LL = L1(#)L2 as PartFunc of COMPLEX,COMPLEX;
LL is RestFunc-like
proof
let h;
consider b1 such that
A1: for z holds L1/.z = b1*z by Def4;
consider b2 such that
A2: for z holds L2/.z = b2*z by Def4;
A3: now
let n be Element of NAT;
A4: h.n <> 0c by COMSEQ_1:4;
thus ((h")(#)((L1(#)L2)/*h)).n = (h").n *((L1(#)L2)/*h).n by VALUED_1:5
.= (h").n*(L1(#)L2)/.(h.n) by FUNCT_2:115
.= (h").n*(L1/.(h.n)*L2/.(h.n)) by CFUNCT_1:64
.= (h").n*L1/.(h.n)*L2/.(h.n)
.= ((h.n)")*L1/.(h.n)*L2/.(h.n) by VALUED_1:10
.= ((h.n)")*((h.n)*b1)*L2/.(h.n) by A1
.= ((h.n)")*(h.n)*b1*L2/.(h.n)
.= 1r*b1*L2/.(h.n) by A4,XCMPLX_0:def 7
.= b1*(b2*(h.n)) by A2
.= b1*b2*(h.n)
.= ((b1*b2)(#)h).n by VALUED_1:6;
end;
then
A5: (h")(#)((L1(#)L2)/*h) = (b1*b2)(#)h;
thus (h")(#)(LL/*h) is convergent by A3,FUNCT_2:63;
lim h = 0c by Def1;
hence lim ((h")(#)(LL/*h)) = (b1*b2)*0c by A5,COMSEQ_2:18
.= 0c;
end;
hence thesis;
end;
end;
registration
let R,L;
cluster R(#)L -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
proof
consider b1 such that
A1: for z holds L/.z = b1*z by Def4;
now
let h;
A2: (h")(#)((R(#)L)/*h) = (h")(#)((R/*h)(#)(L/*h)) by CFCONT_1:14
.= ((h")(#)(R/*h))(#)(L/*h) by COMSEQ_1:8;
now
let n be Element of NAT;
thus (L/*h).n = L/.(h.n) by FUNCT_2:115
.= b1*(h.n) by A1
.= (b1(#)h).n by VALUED_1:6;
end;
then
A3: (L/*h) = b1(#)h;
lim h = 0c by Def1;
then
A4: lim (L/*h) = b1*0c by A3,COMSEQ_2:18
.= 0c;
A5: (h")(#)(R/*h) is convergent by Def3;
hence (h")(#)((R(#)L)/*h) is convergent by A2,A3;
lim ((h")(#)(R/*h)) = 0c by Def3;
hence lim ((h")(#)((R(#)L)/*h)) = 0c*0c by A2,A3,A4,A5,COMSEQ_2:30
.= 0c;
end;
hence thesis;
end;
cluster L(#)R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence;
end;
definition
let z0 be Complex;
mode Neighbourhood of z0 -> Subset of COMPLEX means
:Def5:
ex g be Real st 0 < g & {y where y is Complex : |.y-z0.| < g} c= it;
existence
proof
set N = {y where y is Complex : |.y-z0.| < 1};
take N;
N c= COMPLEX
proof
let z be object;
assume z in {y where y is Complex : |.y-z0.| < 1};
then ex y be Complex st z = y & |.y-z0.| < 1;
hence thesis by XCMPLX_0:def 2;
end;
hence thesis;
end;
end;
theorem Th6:
for g be Real st 0 < g holds
{y where y is Complex : |.y-z0.| < g} is Neighbourhood of z0
proof
let g be Real such that
A1: g > 0;
set N = {y where y is Complex : |.y-z0.| < g};
A2: N c= COMPLEX
proof
let z be object;
assume z in {y where y is Complex : |.y-z0.| < g};
then ex y be Complex st z = y & |.y-z0.| < g;
hence thesis by XCMPLX_0:def 2;
end;
thus thesis by A1,A2,Def5;
end;
theorem Th7:
for N being Neighbourhood of z0 holds z0 in N
proof
let N be Neighbourhood of z0;
consider g be Real such that
A1: 0 < g and
A2: {z where z is Complex : |.z-z0.| < g} c= N by Def5;
|.z0-z0.| = 0 by COMPLEX1:44;
then z0 in {z where z is Complex : |.z-z0.| < g} by A1;
hence thesis by A2;
end;
Lm1: for z0 be Complex for N1,N2 being Neighbourhood of z0 ex N being
Neighbourhood of z0 st N c= N1 & N c= N2
proof
let z0 be Complex;
let N1,N2 be Neighbourhood of z0;
consider a1 be Real such that
A1: 0 < a1 and
A2: {y where y is Complex : |.y-z0.| < a1} c= N1 by Def5;
consider a2 be Real such that
A3: 0 < a2 and
A4: {y where y is Complex : |.y-z0.| < a2} c= N2 by Def5;
set g = min(a1,a2);
take IT= {y where y is Complex : |.y-z0.| < g};
A5: g <= a2 by XXREAL_0:17;
A6: {y where y is Complex : |.y-z0.| < g} c= {y where y is Complex : |.y-z0
.| < a2}
proof
let z be object;
assume z in {y where y is Complex : |.y-z0.| < g};
then consider y be Complex such that
A7: z = y and
A8: |.y-z0.| < g;
|.y-z0.| < a2 by A5,A8,XXREAL_0:2;
hence thesis by A7;
end;
A9: g <= a1 by XXREAL_0:17;
A10: {y where y is Complex : |.y-z0.| < g} c= {y where y is Complex : |.y-z0
.| < a1}
proof
let z be object;
assume z in {y where y is Complex : |.y-z0.| < g};
then consider y be Complex such that
A11: z = y and
A12: |.y-z0.| < g;
|.y-z0.| < a1 by A9,A12,XXREAL_0:2;
hence thesis by A11;
end;
0 < g by A1,A3,XXREAL_0:15;
hence thesis by A2,A4,A10,A6,Th6;
end;
definition
let f;
let z0 be Complex;
pred f is_differentiable_in z0 means
ex N being Neighbourhood of z0 st N c= dom f &
ex L,R st for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0);
end;
definition
let f;
let z0 be Complex;
assume
A1: f is_differentiable_in z0;
func diff(f,z0) -> Element of COMPLEX means
:Def7:
ex N being Neighbourhood of z0 st N c= dom f &
ex L,R st it = L/.1r & for z st z in N holds f/.z-f/.z0 =
L/.(z-z0)+R/.(z-z0);
existence
proof
consider N being Neighbourhood of z0 such that
A2: N c= dom f and
A3: ex L, R st for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)
by A1;
consider L,R such that
A4: for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A3;
consider a be Complex such that
A5: for d be Complex holds L/.d = a*d by Def4;
take a;
L/.1r = a*1r by A5
.= a;
hence thesis by A2,A4;
end;
uniqueness
proof
set s0=InvShift(2);
let a, b be Element of COMPLEX;
assume that
A6: ex N being Neighbourhood of z0 st N c= dom f & ex L,R st a = L/.1r
& for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) and
A7: ex N being Neighbourhood of z0 st N c= dom f & ex L,R st b = L/.1r
& for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0);
consider N being Neighbourhood of z0 such that
N c= dom f and
A8: ex L,R st a = L/.1r & for z st z in N holds f/.z-f/.z0
= L/.(z-z0)+R/.(z-z0) by A6;
consider L,R such that
A9: a = L/.1r and
A10: for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A8;
consider a1 such that
A11: for b holds L/.b = a1*b by Def4;
consider N1 being Neighbourhood of z0 such that
N1 c= dom f and
A12: ex L,R st b = L/.1r & for z st z in N1 holds f/.z-f/.z0 = L/.(z-
z0) +R/.(z-z0) by A7;
consider L1,R1 such that
A13: b = L1/.1r and
A14: for z st z in N1 holds f/.z-f/.z0 = L1/.(z-z0)+R1/.(z-z0) by A12;
consider b1 such that
A15: for b holds L1/.b = b1*b by Def4;
reconsider s0 as Complex_Sequence;
consider N0 be Neighbourhood of z0 such that
A16: N0 c= N & N0 c= N1 by Lm1;
consider g be Real such that
A17: 0 < g and
A18: {y where y is Complex : |.y-z0.| < g} c= N0 by Def5;
set s1 = g(#)s0;
A19: now
let n;
thus s1.n = g*s0.n by VALUED_1:6
.= g*(1/(n+2)) by Def2
.= g/(n+2);
end;
now
let n be Element of NAT;
s1.n = g/(n+2) by A19;
hence 0 <> s1.n by A17;
end;
then
A20: s1 is non-zero by COMSEQ_1:4;
lim s0 = 0 by Th3;
then lim s1 = g*0 by COMSEQ_2:18;
then reconsider h = s1 as 0-convergent non-zero Complex_Sequence
by A20,Def1;
A21: for n ex x be Complex st x in N & x in N1 & h.n = x-z0
proof
let n;
reconsider g0 = g/(n+2) as Complex;
take x = z0+g0;
0+1 < n+1+1 by XREAL_1:6;
then
A22: g/(n+2) < g/1 by A17,XREAL_1:76;
|.z0+g0-z0.| = g/(n+2) by A17,ABSVALUE:def 1;
then x in {y where y is Complex : |.y-z0.| < g} by A22;
then x in N0 by A18;
hence thesis by A16,A19;
end;
A23: a = a1*1r by A9,A11;
A24: now
let z be Complex;
assume that
A25: z in N and
A26: z in N1;
reconsider t0=z0,t=z as Element of COMPLEX by XCMPLX_0:def 2;
f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A10,A25;
then L/.(z-z0)+R/.(z-z0) = L1/.(z-z0)+R1/.(z-z0) by A14,A26;
then a1*(t-t0)+R/.(t-t0) = L1/.(t-t0)+R1/.(t-t0) by A11;
then (a1*1r)*(z-z0)+R/.(z-z0) = (b1*1r)*(z-z0)+R1/.(z-z0) by A15;
hence a*(z-z0)+R/.(z-z0) = b*(z-z0)+R1/.(z-z0) by A13,A15,A23;
end;
A27: a-b in COMPLEX by XCMPLX_0:def 2;
now
dom R1 = COMPLEX by PARTFUN1:def 2;
then
A28: rng h c= dom R1;
dom R = COMPLEX by PARTFUN1:def 2;
then
A29: rng h c= dom R;
let n be Nat;
A30: n in NAT by ORDINAL1:def 12;
then
A31: h.n <> 0c by COMSEQ_1:4;
ex x be Complex st x in N & x in N1 & h.n = x-z0 by A21;
then a*(h.n)+R/.(h.n) = b*(h.n)+R1/.(h.n) by A24;
then
A32: (
a*(h.n))/(h.n)+(R/.(h.n))/(h.n) = (b*(h.n)+R1/.(h.n))/(h.n) by XCMPLX_1:62;
A33: (b*(h.n))/(h.n) = b*((h.n)/(h.n)) .= b*1 by A31,XCMPLX_1:60
.= b;
A34: (R1/.(h.n))/(h.n) = (R1/.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A30,A28,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
A35: (a*(h.n))/(h.n) = a*((h.n)/(h.n)) .= a*1 by A31,XCMPLX_1:60
.= a;
(R/.(h.n))/(h.n) = (R/.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A30,A29,FUNCT_2:109
.= ((h")(#)(R/*h)).n by VALUED_1:5;
hence a-b = (((h")(#)(R1/*h)).n+-((h")(#)(R/*h)).n) by A32,A35,A33,A34
.= (((h")(#)(R1/*h)).n+(-((h")(#)(R/*h))).n) by VALUED_1:8
.= ((h")(#)(R1/*h)+-((h")(#)(R/*h))).n by A30,VALUED_1:1;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = a-b by VALUED_0:def 18,A27;
then
A36: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = a-b by CFCONT_1:28;
A37: (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by Def3;
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by Def3;
then a-b = 0-0 by A36,A37,COMSEQ_2:26;
hence thesis;
end;
end;
definition
let f;
attr f is differentiable means
for x st x in dom f holds f is_differentiable_in x;
end;
definition
let f,X;
pred f is_differentiable_on X means
X c= dom f & f|X is differentiable;
end;
theorem Th8:
f is_differentiable_on X implies X is Subset of COMPLEX
by XBOOLE_1:1;
definition :: complex-membered set
let X be Subset of COMPLEX;
attr X is closed means
for s1 be Complex_Sequence st rng s1 c= X &
s1 is convergent holds lim s1 in X;
end;
definition
let X be Subset of COMPLEX;
attr X is open means
X` is closed;
end;
theorem Th9:
for X being Subset of COMPLEX st X is open for z0 be Complex st
z0 in X ex N being Neighbourhood of z0 st N c= X
proof
let X be Subset of COMPLEX;
assume X is open;
then
A1: X` is closed;
let z0 be Complex;
assume that
A2: z0 in X and
A3: for N be Neighbourhood of z0 holds not N c= X;
defpred P[Nat,Complex] means $2 in {y where y is Complex : |.y-z0
.| < 1/($1+1)} & $2 in X`;
now
let g be Real such that
A4: 0 < g;
set N = {y where y is Complex : |.y-z0.| < g};
N is Neighbourhood of z0 by A4,Th6;
then not N c= X by A3;
then consider x be object such that
A5: x in N and
A6: not x in X;
consider s be Complex such that
A7: x = s and
A8: |.s-z0.| < g by A5;
reconsider s as Element of COMPLEX by XCMPLX_0:def 2;
take s;
thus s in N by A8;
thus s in X` by A6,A7,XBOOLE_0:def 5;
end;
then
A9: for n being Element of NAT ex s be Element of COMPLEX st P[n,s];
consider s1 be sequence of COMPLEX such that
A10: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A9);
A11: rng s1 c= X`
proof
let y be object;
assume y in rng s1;
then consider y1 be object such that
A12: y1 in dom s1 and
A13: s1.y1 = y by FUNCT_1:def 3;
reconsider y1 as Element of NAT by A12;
s1.y1 in X` by A10;
hence thesis by A13;
end;
A14: now
let p be Real;
assume
A15: 0 < p;
consider n such that
A16: p" < n by SEQ_4:3;
take n;
let m be Nat;
assume n <= m;
then n+1 <= m+1 by XREAL_1:6;
then
A17: 1/(m+1) <= 1/(n+1) by XREAL_1:118;
m in NAT by ORDINAL1:def 12;
then s1.m in {y where y is Complex : |.y-z0.| < 1/(m+1)} by A10;
then ex y be Complex st s1.m = y & |.y-z0.| < 1/(m+1);
then
A18: |.s1.m-z0.| < 1/(n+1) by A17,XXREAL_0:2;
p"+0 < n+1 by A16,XREAL_1:8;
then 1/(n+1) < 1/p" by A15,XREAL_1:76;
hence |.s1.m - z0.| < p by A18,XXREAL_0:2;
end;
then
A19: s1 is convergent;
then lim s1 = z0 by A14,COMSEQ_2:def 6;
then z0 in COMPLEX \ X by A19,A11,A1;
hence contradiction by A2,XBOOLE_0:def 5;
end;
theorem
for X being Subset of COMPLEX st X is open for z0 be Complex st z0 in
X holds ex g be Real st {y where y is Complex : |.y-z0.| < g} c= X
proof
let X be Subset of COMPLEX such that
A1: X is open;
let z0 be Complex;
assume z0 in X;
then consider N be Neighbourhood of z0 such that
A2: N c= X by A1,Th9;
consider g be Real such that
0 < g and
A3: {y where y is Complex : |.y-z0.| < g} c= N by Def5;
take g;
thus thesis by A2,A3;
end;
theorem Th11:
for X being Subset of COMPLEX holds ((for z0 be Complex st z0 in
X holds ex N be Neighbourhood of z0 st N c= X) implies X is open)
proof
let X be Subset of COMPLEX;
assume that
A1: for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N
c= X and
A2: not X is open;
not X` is closed by A2;
then consider s1 be sequence of COMPLEX such that
A3: rng s1 c= X` and
A4: s1 is convergent and
A5: not lim s1 in X`;
lim s1 in COMPLEX by XCMPLX_0:def 2;
then lim s1 in X by A5,SUBSET_1:29;
then consider N be Neighbourhood of (lim s1) such that
A6: N c= X by A1;
consider g be Real such that
A7: 0 < g and
A8: {y where y is Complex : |.y-(lim s1).| < g} c= N by Def5;
consider n such that
A9: for m be Nat st n <= m
holds |.(s1.m)-(lim s1).| < g by A4,A7,
COMSEQ_2:def 6;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then
A10: s1.n in rng s1 by FUNCT_1:def 3;
|.s1.n-(lim s1).| < g by A9;
then s1.n in {y where y is Complex : |.y-(lim s1).| < g};
then s1.n in N by A8;
hence contradiction by A3,A6,A10,XBOOLE_0:def 5;
end;
theorem
for X be Subset of COMPLEX holds X is open iff for x be Complex st x
in X ex N be Neighbourhood of x st N c= X by Th9,Th11;
theorem Th13:
for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be
Real st X = {y where y is Complex : |.y-z0.| < r} holds X is open
proof
let X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Real;
reconsider X0 = X as Subset of COMPLEX;
assume
A1: X = {y where y is Complex : |.y-z0.| < r};
for x be Complex st x in X0 ex N be Neighbourhood of x st N c= X0
proof
let x be Complex;
reconsider r1 = (r- |.x-z0.|)/2 as Real;
set N = {y where y is Complex : |.y-x.| < r1};
assume x in X0;
then ex y be Complex st x = y & |.y-z0.| < r by A1;
then
A2: r - |.x-z0.| > 0 by XREAL_1:50;
then reconsider N as Neighbourhood of x by Th6;
r1 < r- |.x-z0.| by A2,XREAL_1:216;
then
A3: r1+|.x-z0.| < (r- |.x-z0.|)+|.x-z0.| by XREAL_1:8;
take N;
let z be object;
assume z in N;
then consider y1 be Complex such that
A4: z = y1 and
A5: |.y1-x.| < r1;
|.y1-x.|+|.x-z0.| < r1+|.x-z0.| by A5,XREAL_1:8;
then |.y1-z0.| <= |.y1-x.|+|.x-z0.| & |.y1-x.|+|.x-z0.| < r by A3,
COMPLEX1:63,XXREAL_0:2;
then |.y1-z0.| < r by XXREAL_0:2;
hence thesis by A1,A4;
end;
hence thesis by Th11;
end;
theorem
for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Real
st X = {y where y is Complex : |.y-z0.| <= r} holds X is closed
proof
let X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Real;
reconsider X0 = X as Subset of COMPLEX;
assume
A1: X = {y where y is Complex : |.y-z0.| <= r};
for s1 be Complex_Sequence st rng s1 c= X0 & s1 is convergent holds lim
s1 in X0
proof
reconsider r as Element of REAL by XREAL_0:def 1;
set s4 = seq_const r;
reconsider s2 = NAT --> z0 as Complex_Sequence;
let s1 be Complex_Sequence;
assume that
A2: rng s1 c= X0 and
A3: s1 is convergent;
set s3 = s1-s2;
A4: s2 is convergent by CFCONT_1:26;
then
A5: lim s3 = lim s1-lim s2 by A3,COMSEQ_2:26;
A6: for n be Element of NAT holds (|.s3.|).n <= r
proof
let n be Element of NAT;
now
let n be Element of NAT;
s3.n = s1.n+(-s2).n by VALUED_1:1
.= s1.n-s2.n by VALUED_1:8;
hence s3.n = s1.n-z0;
end;
then
A7: s3.n = s1.n-z0;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:def 3;
then s1.n in X0 by A2;
then ex y be Complex st y = s1.n & |.y-z0.| <= r by A1;
hence thesis by A7,VALUED_1:18;
end;
s3 is convergent by A3,A4;
then
A8: lim |.s3.| = |.lim s3.| by SEQ_2:27;
reconsider s3 = s1-s2 as convergent Complex_Sequence by A3,A4;
A9: for n be Nat holds |.s3.|.n <= s4.n
proof
let n be Nat;
A10: n in NAT by ORDINAL1:def 12;
(|.s3.|).n <= r by A6,A10;
hence thesis by SEQ_1:57;
end;
A11: for n be Element of NAT holds lim s2 = z0
proof
let n be Element of NAT;
lim s2 = s2.n by CFCONT_1:28
.= z0;
hence thesis;
end;
lim s4 = s4.0 by SEQ_4:26
.= r by SEQ_1:57;
then lim |.s3.| <= r by A9,SEQ_2:18;
then |.(lim s1)-z0.| <= r by A11,A5,A8;
hence thesis by A1;
end;
hence thesis;
end;
registration
cluster open for Subset of COMPLEX;
existence
proof
reconsider X = {y where y is Complex : |.y-0c.| < 1} as Subset of COMPLEX
by Th6;
X is open by Th13;
hence thesis;
end;
end;
reserve Z for open Subset of COMPLEX;
theorem Th15:
f is_differentiable_on Z iff Z c= dom f & for x st x in Z holds
f is_differentiable_in x
proof
thus f is_differentiable_on Z implies Z c= dom f & for x st x in Z holds f
is_differentiable_in x
proof
assume
A1: f is_differentiable_on Z;
hence
A2: Z c= dom f;
let x0;
A3: f|Z is differentiable by A1;
assume
A4: x0 in Z;
then x0 in dom (f|Z) by A2,RELAT_1:57;
then f|Z is_differentiable_in x0 by A3;
then consider N being Neighbourhood of x0 such that
A5: N c= dom(f|Z) and
A6: ex L,R st for x st x in N holds (f|Z)/.x-(f|Z)/.x0 = L/.(x-x0)+R/.
(x -x0);
take N;
dom(f|Z) = dom f/\Z by RELAT_1:61;
then dom(f|Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A5;
consider L,R such that
A7: for x st x in N holds (f|Z)/.x-(f|Z)/.x0 = L/.(x-x0)+R/.(x-x0) by A6;
take L, R;
let x;
assume
A8: x in N;
then (f|Z)/.x-(f|Z)/.x0 = L/.(x-x0)+R/.(x-x0) by A7;
then
A9: f/.x-(f|Z)/.x0 = L/.(x-x0)+R/.(x-x0) by A5,A8,PARTFUN2:15;
x0 in dom f/\ Z by A2,A4,XBOOLE_0:def 4;
hence thesis by A9,PARTFUN2:16;
end;
assume that
A10: Z c= dom f and
A11: for x st x in Z holds f is_differentiable_in x;
thus Z c= dom f by A10;
let x0;
assume x0 in dom (f|Z);
then
A12: x0 in Z by RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by Th9;
f is_differentiable_in x0 by A11,A12;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: ex L,R st for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0);
consider N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Lm1;
A18: N2 c= Z by A13,A16;
take N2;
N2 c= dom f by A14,A17;
then N2 c= dom f/\Z by A18,XBOOLE_1:19;
hence
A19: N2 c= dom(f|Z) by RELAT_1:61;
consider L,R such that
A20: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A15;
A21: x0 in N2 by Th7;
take L, R;
let x;
assume
A22: x in N2;
then f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A17,A20;
then (f|Z)/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A19,A22,PARTFUN2:15;
hence thesis by A19,A21,PARTFUN2:15;
end;
theorem
f is_differentiable_on Y implies Y is open
proof
assume
A1: f is_differentiable_on Y;
then
A2: Y c= dom f;
now
let x0 be Complex;
assume x0 in Y;
then
A3: x0 in dom (f|Y) by A2,RELAT_1:57;
f|Y is differentiable by A1;
then f|Y is_differentiable_in x0 by A3;
then consider N being Neighbourhood of x0 such that
A4: N c= dom(f|Y) and
ex L,R st for x st x in N holds (f|Y)/.x-(f|Y)/.x0 = L/.(x-x0)+R/.(x -
x0);
take N;
dom(f|Y) = dom f/\Y by RELAT_1:61;
then dom(f|Y) c= Y by XBOOLE_1:17;
hence N c= Y by A4;
end;
hence thesis by Th11;
end;
definition
let f, X;
assume
A1: f is_differentiable_on X;
func f`|X -> PartFunc of COMPLEX,COMPLEX means
:Def12:
dom it = X & for x st x in X holds it/.x = diff(f,x);
existence
proof
deffunc F(Element of COMPLEX) = diff(f,$1);
defpred P[set] means $1 in X;
consider F being PartFunc of COMPLEX,COMPLEX such that
A2: (for x be Element of COMPLEX holds x in dom F iff P[x]) & for x be
Element of COMPLEX st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
take F;
now
A3: X is Subset of COMPLEX by A1,Th8;
let y be object;
assume y in X;
hence y in dom F by A2,A3;
end;
then
A4: X c= dom F;
for y being object st y in dom F holds y in X by A2;
then dom F c= X;
hence dom F = X by A4;
now
let x;
assume
A5: x in X;
x in COMPLEX by XCMPLX_0:def 2;
then
A6: x in dom F by A2,A5;
then F.x = diff(f,x) by A2;
hence F/.x = diff(f,x) by A6,PARTFUN1:def 6;
end;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of COMPLEX,COMPLEX;
assume that
A7: dom F = X and
A8: for x st x in X holds F/.x = diff(f,x) and
A9: dom G = X and
A10: for x st x in X holds G/.x = diff(f,x);
now
let x be Element of COMPLEX;
assume
A11: x in dom F;
then F/.x = diff(f,x) by A7,A8;
hence F/.x = G/.x by A7,A10,A11;
end;
hence thesis by A7,A9,PARTFUN2:1;
end;
end;
theorem
for f,Z st Z c= dom f & ex a1 st rng f = {a1} holds f
is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 0c
proof
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX;
set R = cf;
now
let h;
now
let n be Nat;
A2: rng h c= dom R & n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h").n*((R/*h).n) by VALUED_1:5
.= (h").n*(R/.(h.n)) by A2,FUNCT_2:109
.= (h").n* 0c
.= 0c;
end;
then (h")(#)(R/*h) is constant & ((h")(#)(R/*h)).0 = 0c by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0c by CFCONT_1:26
,27;
end;
then reconsider R as C_RestFunc by Def3;
set L = cf;
for z holds L/.z = 0c*z
by XCMPLX_0:def 2,FUNCOP_1:7;
then reconsider L as C_LinearFunc by Def4;
let f, Z such that
A3: Z c= dom f;
given a1 such that
A4: rng f = {a1};
A5: now
let x0;
assume
A6: x0 in dom f;
then f.x0 in {a1} by A4,FUNCT_1:def 3;
then f/.x0 in {a1} by A6,PARTFUN1:def 6;
hence f/.x0 = a1 by TARSKI:def 1;
end;
A7: now
let x0;
assume
A8: x0 in Z;
then consider N being Neighbourhood of x0 such that
A9: N c= Z by Th9;
A10: N c= dom f by A3,A9;
A11: x - x0 in COMPLEX by XCMPLX_0:def 2;
for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
assume x in N;
hence f/.x-f/.x0 = a1-f/.x0 by A5,A10
.= a1-a1 by A3,A5,A8
.= L/.(x-x0)+0c by FUNCOP_1:7,A11
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A11;
end;
hence f is_differentiable_in x0 by A10;
end;
hence
A12: f is_differentiable_on Z by A3,Th15;
let x0;
assume
A13: x0 in Z;
then
A14: f is_differentiable_in x0 by A7;
then ex N being Neighbourhood of x0 st N c= dom f & ex L,R st for x st x in
N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0);
then consider N being Neighbourhood of x0 such that
A15: N c= dom f;
A16: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A17: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
hence f/.x-f/.x0 = a1-f/.x0 by A5,A15
.= a1-a1 by A3,A5,A13
.= L/.(x-x0)+0c by FUNCOP_1:7,A17
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A17;
end;
thus (f`|Z)/.x0 = diff(f,x0) by A12,A13,Def12
.= L/.1r by A14,A15,A16,Def7
.= 0c;
end;
registration
let seq be non-zero Complex_Sequence, k be Nat;
cluster seq ^\k -> non-zero;
coherence
proof
reconsider k as Element of NAT by ORDINAL1:def 12;
now
let n be Element of NAT;
(seq ^\k).n = seq.(n+k) by NAT_1:def 3;
hence (seq ^\k).n <> 0c by COMSEQ_1:4;
end;
hence thesis by COMSEQ_1:4;
end;
end;
registration
let h,n;
cluster h^\n -> 0-convergent for Complex_Sequence;
coherence
proof
lim h = 0 by Def1;
then
A1: lim (h^\n) = 0 by CFCONT_1:21;
h^\n is convergent by CFCONT_1:21;
hence thesis by A1;
end;
end;
theorem Th18:
(seq+seq1)^\k = (seq^\k)+(seq1^\k)
proof
now
let n be Element of NAT;
A1: n+k in NAT by ORDINAL1:def 12;
thus ((seq+seq1)^\k).n = (seq+seq1).(n+k) by NAT_1:def 3
.= seq.(n+k)+seq1.(n+k) by VALUED_1:1,A1
.= (seq^\k).n+seq1.(n+k) by NAT_1:def 3
.= (seq^\k).n+(seq1^\k).n by NAT_1:def 3
.= ((seq^\k)+(seq1^\k)).n by VALUED_1:1;
end;
hence thesis;
end;
theorem Th19:
(seq-seq1)^\k = (seq^\k)-(seq1^\k)
proof
now
let n be Element of NAT;
A1: n+k in NAT by ORDINAL1:def 12;
thus ((seq-seq1)^\k).n = (seq+-seq1).(n+k) by NAT_1:def 3
.= seq.(n+k)+(-seq1).(n+k) by VALUED_1:1,A1
.= seq.(n+k)+-seq1.(n+k) by VALUED_1:8
.= (seq^\k).n-seq1.(n+k) by NAT_1:def 3
.= (seq^\k).n+-(seq1^\k).n by NAT_1:def 3
.= (seq^\k).n+(-(seq1^\k)).n by VALUED_1:8
.= ((seq^\k)-(seq1^\k)).n by VALUED_1:1;
end;
hence thesis;
end;
theorem Th20:
(seq")^\k = (seq^\k)"
proof
now
let n be Element of NAT;
thus ((seq")^\k).n = (seq").(n+k) by NAT_1:def 3
.= (seq.(n+k))" by VALUED_1:10
.= ((seq^\k).n)" by NAT_1:def 3
.= ((seq^\k)").n by VALUED_1:10;
end;
hence thesis;
end;
theorem Th21:
(seq(#)seq1)^\k = (seq^\k)(#)(seq1^\k)
proof
now
let n be Element of NAT;
thus ((seq(#)seq1)^\k).n = (seq(#)seq1).(n+k) by NAT_1:def 3
.= seq.(n+k)*seq1.(n+k) by VALUED_1:5
.= (seq^\k).n*seq1.(n+k) by NAT_1:def 3
.= (seq^\k).n*(seq1^\k).n by NAT_1:def 3
.= ((seq^\k)(#)(seq1^\k)).n by VALUED_1:5;
end;
hence thesis;
end;
theorem Th22:
for x0 be Complex for N being Neighbourhood of x0 st f
is_differentiable_in x0 & N c= dom f holds for h,c st rng c = {x0} & rng (h+c)
c= N holds h"(#)(f/*(h+c)-f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h+c
)-f/*c))
proof
let x0 be Complex;
let N be Neighbourhood of x0;
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f;
consider N1 be Neighbourhood of x0 such that
N1 c= dom f and
A3: ex L,R st for x st x in N1 holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A1;
consider N2 be Neighbourhood of x0 such that
A4: N2 c= N and
A5: N2 c= N1 by Lm1;
A6: N2 c= dom f by A2,A4;
let h, c such that
A7: rng c = {x0} and
A8: rng (h+c) c= N;
consider g be Real such that
A9: 0 < g and
A10: {y where y is Complex : |.y-x0.| < g} c= N2 by Def5;
|.x0-x0.| = 0 by COMPLEX1:44;
then x0 in {y where y is Complex : |.y-x0.| < g} by A9;
then
A11: x0 in N2 by A10;
A12: rng c c= dom f
proof
let y be object;
assume y in rng c;
then y = x0 by A7,TARSKI:def 1;
then y in N by A4,A11;
hence thesis by A2;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
x0 in rng c by A7,TARSKI:def 1;
then
A13: lim c = x0 by CFCONT_1:27;
A14: c is convergent by CFCONT_1:26;
then
A15: h+c is convergent;
lim h = 0 by Def1;
then lim (h+c) = 0+x0 by A14,A13,COMSEQ_2:14
.= x0;
then consider n such that
A16: for m being Nat st n <= m holds |.(h+c).m-x0.| < g by A9,A15,
COMSEQ_2:def 6;
take n;
A17: rng (c^\n) = {x0} by A7,VALUED_0:26;
thus rng (c^\n) c= N2
by A11,A17,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m being Element of NAT such that
A18: y = ((h+c)^\n).m by FUNCT_2:113;
reconsider y1 = y as Complex by A18;
n+0 <= n+m by XREAL_1:7;
then |.(h+c).(n+m)-x0.| < g by A16;
then |.((h+c)^\n).m-x0.| < g by NAT_1:def 3;
then y1 in {z where z is Complex : |.z-x0.| < g} by A18;
hence thesis by A10;
end;
then consider n such that
rng (c^\n) c= N2 and
A19: rng ((h+c)^\n) c= N2;
consider L,R such that
A20: for x st x in N1 holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A3;
A21: rng (c^\n) c= dom f
proof
let y be object;
assume
A22: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = x0 by A7,A22,TARSKI:def 1;
then y in N by A4,A11;
hence thesis by A2;
end;
A23: (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent & lim ((L/*(h^\n)+R/*(h^\
n))(#)(h^\n)") = L/.1r
proof
deffunc F(Nat) = L/.1r+((R/*(h^\n))(#)(h^\n)").$1;
consider s1 such that
A24: for k holds s1.k = F(k) from COMSEQ_1:sch 1;
A25: now
A26: ((h^\n)")(#)(R/*(h^\n)) is convergent & lim (((h^\n)")(#)(R/*(h^\n)
)) = 0 by Def3;
let r be Real;
assume 0 < r;
then consider m being Nat such that
A27: for k being Nat st m <= k
holds |.(((h^\n)")(#)(R/*(h^\n))).k-0c.| < r
by A26,COMSEQ_2:def 6;
take n1 = m;
let k such that
A28: n1 <= k;
|.s1.k-L/.1r.| = |.L/.1r+((R/*(h^\n))(#)(h^\n)").k-L/.1r .| by A24
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0c.|;
hence |.s1.k-L/.1r.| < r by A27,A28;
end;
consider x such that
A29: for b1 holds L/.b1 = x*b1 by Def4;
A30: L/.1r = x*1r by A29
.= x;
now
let m be Element of NAT;
A31: (h^\n).m <> 0c by COMSEQ_1:4;
thus ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)").m = ((L/*(h^\n)+R/*(h^\n)).m)*((h
^\n)").m by VALUED_1:5
.= ((L/*(h^\n)).m+(R/*(h^\n)).m) *((h^\n)").m by VALUED_1:1
.= ((L/*(h^\n)).m)*((h^\n)").m+((R/*(h^\n)).m)*((h^\n)").m
.= ((L/*(h^\n)).m)*((h^\n)").m+((R/*(h^\n))(#)(h^\n)").m by VALUED_1:5
.= ((L/*(h^\n)).m)*((h^\n).m)"+((R/*(h^\n))(#)(h^\n)").m by VALUED_1:10
.= (L/.((h^\n).m))*((h^\n).m)"+((R/*(h^\n))(#)(h^\n)").m by FUNCT_2:115
.= (x*((h^\n).m))*((h^\n).m)"+((R/*(h^\n))(#)(h^\n)").m by A29
.= x*(((h^\n).m)*((h^\n).m)")+((R/*(h^\n))(#)(h^\n)").m
.= x*1r+((R/*(h^\n))(#)(h^\n)").m by A31,XCMPLX_0:def 7
.= s1.m by A24,A30;
end;
then
A32: (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" = s1;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A25;
hence thesis by A32,A25,COMSEQ_2:def 6;
end;
A33: for k holds f/.(((h+c)^\n).k)-f/.((c^\n).k) = L/.((h^\n).k)+R/.((h^\n). k)
proof
let k;
A34: k+n in NAT by ORDINAL1:def 12;
A35: k in NAT by ORDINAL1:def 12;
then ((h+c)^\n).k in rng ((h+c)^\n) by FUNCT_2:112;
then
A36: ((h+c)^\n).k in N2 by A19;
(c^\n).k in rng (c^\n) & rng (c^\n) = rng c
by FUNCT_2:112,VALUED_0:26,A35;
then
A37: (c^\n).k = x0 by A7,TARSKI:def 1;
((h+c)^\n).k-(c^\n).k = (h+c).(k+n)-(c^\n).k by NAT_1:def 3
.= h.(k+n)+c.(k+n)-(c^\n).k by VALUED_1:1,A34
.= (h^\n).k+c.(k+n)-(c^\n).k by NAT_1:def 3
.= (h^\n).k+(c^\n).k-(c^\n).k by NAT_1:def 3
.= (h^\n).k;
hence thesis by A20,A5,A36,A37;
end;
A38: rng (h+c) c= dom f
by A8,A2;
A39: rng ((h+c)^\n) c= dom f
by A19,A4,A2;
now
let k be Element of NAT;
thus (f/*((h+c)^\n)-f/*(c^\n)).k = (f/*((h+c)^\n)).k-(f/*(c^\n)).k by
CFCONT_1:1
.= f/.(((h+c)^\n).k)-(f/*(c^\n)).k by A39,FUNCT_2:109
.= f/.(((h+c)^\n).k)-f/.((c^\n).k) by A21,FUNCT_2:109
.= L/.((h^\n).k)+R/.((h^\n).k) by A33
.= (L/*(h^\n)).k+R/.((h^\n).k) by FUNCT_2:115
.= (L/*(h^\n)).k+(R/*(h^\n)).k by FUNCT_2:115
.= (L/*(h^\n)+R/*(h^\n)).k by VALUED_1:1;
end;
then
A40: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)") = ((f/*((h+c)^\n)-f/*(c^\n))(#)(h^\n)
") by FUNCT_2:def 7
.= ((((f/*(h+c))^\n)-f/*(c^\n))(#)(h^\n)") by A38,VALUED_0:27
.= ((((f/*(h+c))^\n)-((f/*c)^\n))(#)(h^\n)") by A12,VALUED_0:27
.= ((((f/*(h+c))-(f/*c))^\n)(#)(h^\n)") by Th19
.= ((((f/*(h+c))-(f/*c))^\n)(#)((h")^\n)) by Th20
.= ((((f/*(h+c))-(f/*c))(#) h")^\n) by Th21;
then
A41: L/.1r = lim ((h")(#)((f/*(h+c))-(f/*c))) by A23,CFCONT_1:23;
thus h" (#) (f/*(h+c)-f/*c) is convergent by A23,A40,CFCONT_1:22;
for x st x in N2 holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A20,A5;
hence thesis by A1,A6,A41,Def7;
end;
theorem Th23:
for f1,f2,x0 st f1 is_differentiable_in x0 & f2
is_differentiable_in x0 holds f1+f2 is_differentiable_in x0 & diff(f1+f2,x0) =
diff(f1,x0)+diff(f2,x0)
proof
let f1,f2,x0;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L, R st for x st x in N1 holds f1/.x-f1/.x0 = L/.(x-x0)+R/.(x-x0)
by A1;
consider L1, R1 such that
A5: for x st x in N1 holds f1/.x-f1/.x0 = L1/.(x-x0)+R1/.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x st x in N2 holds f2/.x-f2/.x0 = L/.(x-x0)+R/.(x-x0)
by A2;
consider L2,R2 such that
A8: for x st x in N2 holds f2/.x-f2/.x0 = L2/.(x-x0)+R2/.(x-x0) by A7;
reconsider R = R1+R2 as C_RestFunc;
reconsider L = L1+L2 as C_LinearFunc;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1/\ dom f2 by A11,XBOOLE_1:27;
then
A12: N c= dom (f1+f2) by VALUED_1:def 1;
A13: now
let x;
A14: x0 in N by Th7;
A15: x-x0 in COMPLEX by XCMPLX_0:def 2;
assume
A16: x in N;
hence (f1+f2)/.x-(f1+f2)/.x0 = (f1/.x+f2/.x)-(f1+f2)/.x0 by A12,CFUNCT_1:1
.= f1/.x+f2/.x-(f1/.x0+f2/.x0) by A12,A14,CFUNCT_1:1
.= (f1/.x-f1/.x0)+(f2/.x-f2/.x0)
.= L1/.(x-x0)+R1/.(x-x0)+(f2/.x-f2/.x0) by A5,A9,A16
.= L1/.(x-x0)+R1/.(x-x0)+(L2/.(x-x0)+R2/.(x-x0)) by A8,A10,A16
.= (L1/.(x-x0)+L2/.(x-x0))+(R1/.(x-x0)+R2/.(x-x0))
.= L/.(x-x0)+(R1/.(x-x0)+R2/.(x-x0)) by CFUNCT_1:64,A15
.= L/.(x-x0)+R/.(x-x0) by CFUNCT_1:64,A15;
end;
hence f1+f2 is_differentiable_in x0 by A12;
hence diff(f1+f2,x0) = L/.1r by A12,A13,Def7
.= L1/.1r+L2/.1r by CFUNCT_1:64
.= diff(f1,x0)+L2/.1r by A1,A3,A5,Def7
.= diff(f1,x0)+diff(f2,x0) by A2,A6,A8,Def7;
end;
theorem Th24:
for f1,f2,x0 st f1 is_differentiable_in x0 & f2
is_differentiable_in x0 holds f1-f2 is_differentiable_in x0 & diff(f1-f2,x0) =
diff(f1,x0)-diff(f2,x0)
proof
let f1,f2,x0;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x st x in N1 holds f1/.x-f1/.x0 = L/.(x-x0)+R/.(x-x0)
by A1;
consider L1,R1 such that
A5: for x st x in N1 holds f1/.x-f1/.x0 = L1/.(x-x0)+R1/.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x st x in N2 holds f2/.x-f2/.x0 = L/.(x-x0)+R/.(x-x0)
by A2;
consider L2,R2 such that
A8: for x st x in N2 holds f2/.x-f2/.x0 = L2/.(x-x0)+R2/.(x-x0) by A7;
reconsider R = R1-R2 as C_RestFunc;
reconsider L = L1-L2 as C_LinearFunc;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1/\ dom f2 by A11,XBOOLE_1:27;
then
A12: N c= dom (f1-f2) by CFUNCT_1:2;
A13: now
let x;
A14: x0 in N by Th7;
A15: x-x0 in COMPLEX by XCMPLX_0:def 2;
assume
A16: x in N;
hence (f1-f2)/.x-(f1-f2)/.x0 = (f1/.x-f2/.x)-(f1-f2)/.x0 by A12,CFUNCT_1:2
.= f1/.x-f2/.x-(f1/.x0-f2/.x0) by A12,A14,CFUNCT_1:2
.= f1/.x-f1/.x0-(f2/.x-f2/.x0)
.= L1/.(x-x0)+R1/.(x-x0)-(f2/.x-f2/.x0) by A5,A9,A16
.= L1/.(x-x0)+R1/.(x-x0)-(L2/.(x-x0)+R2/.(x-x0)) by A8,A10,A16
.= L1/.(x-x0)-L2/.(x-x0)+(R1/.(x-x0)-R2/.(x-x0))
.= L/.(x-x0)+(R1/.(x-x0)-R2/.(x-x0)) by CFUNCT_1:64,A15
.= L/.(x-x0)+R/.(x-x0) by CFUNCT_1:64,A15;
end;
hence f1-f2 is_differentiable_in x0 by A12;
hence diff(f1-f2,x0) = L/.1r by A12,A13,Def7
.= L1/.1r-L2/.1r by CFUNCT_1:64
.= diff(f1,x0)-L2/.1r by A1,A3,A5,Def7
.= diff(f1,x0)-diff(f2,x0) by A2,A6,A8,Def7;
end;
theorem Th25:
for a,f,x0 st f is_differentiable_in x0 holds a(#)f
is_differentiable_in x0 & diff((a(#)f),x0) = a*diff(f,x0)
proof
let a,f,x0;
assume
A1: f is_differentiable_in x0;
then consider N1 be Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L,R st for x st x in N1 holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0);
consider L1,R1 such that
A4: for x st x in N1 holds f/.x-f/.x0 = L1/.(x-x0)+R1/.(x-x0) by A3;
reconsider R = a(#)R1 as C_RestFunc;
reconsider L = a(#)L1 as C_LinearFunc;
A5: N1 c= dom(a(#)f) by A2,VALUED_1:def 5;
A6: now
let x;
A7: x0 in N1 by Th7;
A8: x-x0 in COMPLEX by XCMPLX_0:def 2;
assume
A9: x in N1;
hence (a(#)f)/.x-(a(#)f)/.x0 = a*(f/.x)-(a(#)f)/.x0 by A5,CFUNCT_1:4
.= a*f/.x-a*f/.x0 by A5,A7,CFUNCT_1:4
.= a*(f/.x-f/.x0)
.= a*(L1/.(x-x0)+R1/.(x-x0)) by A4,A9
.= a*L1/.(x-x0)+a*R1/.(x-x0)
.= L/.(x-x0)+a*R1/.(x-x0) by CFUNCT_1:65,A8
.= L/.(x-x0)+R/.(x-x0) by CFUNCT_1:65,A8;
end;
hence a(#)f is_differentiable_in x0 by A5;
hence diff((a(#)f),x0) = L/.1r by A5,A6,Def7
.= a*L1/.1r by CFUNCT_1:65
.= a*diff(f,x0) by A1,A2,A4,Def7;
end;
theorem Th26:
for f1,f2,x0 st f1 is_differentiable_in x0 & f2
is_differentiable_in x0 holds f1(#)f2 is_differentiable_in x0 & diff(f1(#)f2,x0
) = (f2/.x0)*diff(f1,x0)+(f1/.x0)*diff(f2,x0)
proof
let f1,f2,x0;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N2 be Neighbourhood of x0 such that
A3: N2 c= dom f2 and
A4: ex L,R st for x st x in N2 holds f2/.x-f2/.x0 = L/.(x-x0)+R/.(x-x0)
by A2;
consider L2,R2 such that
A5: for x st x in N2 holds f2/.x-f2/.x0 = L2/.(x-x0)+R2/.(x-x0) by A4;
reconsider R12 = (f1/.x0)(#)R2 as C_RestFunc;
reconsider L12 = (f1/.x0)(#)L2 as C_LinearFunc;
consider N1 be Neighbourhood of x0 such that
A6: N1 c= dom f1 and
A7: ex L,R st for x st x in N1 holds f1/.x-f1/.x0 = L/.(x-x0)+R/.(x-x0)
by A1;
consider L1,R1 such that
A8: for x st x in N1 holds f1/.x-f1/.x0 = L1/.(x-x0)+R1/.(x-x0) by A7;
reconsider R11 = (f2/.x0)(#)R1 as C_RestFunc;
reconsider L11 = (f2/.x0)(#)L1 as C_LinearFunc;
reconsider R18 = R2(#)L1 as C_RestFunc;
reconsider R17 = R1(#)R2 as C_RestFunc;
reconsider R16 = R1(#)L2 as C_RestFunc;
reconsider R14 = L1(#)L2 as C_RestFunc;
reconsider R13 = R11+R12 as C_RestFunc;
reconsider L = L11+L12 as C_LinearFunc;
reconsider R15 = R13+R14 as C_RestFunc;
reconsider R19 = R16+R17 as C_RestFunc;
reconsider R20 = R19+R18 as C_RestFunc;
reconsider R = R15+R20 as C_RestFunc;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A3,A10;
N c= dom f1 by A6,A9;
then N/\ N c= dom f1/\ dom f2 by A11,XBOOLE_1:27;
then
A12: N c= dom (f1(#)f2) by VALUED_1:def 4;
A13: now
let x;
A14: x0 in N by Th7;
A15: x-x0 in COMPLEX by XCMPLX_0:def 2;
assume
A16: x in N;
then
A17: f1/.x-f1/.x0+f1/.x0 = L1/.(x-x0)+R1/.(x-x0)+f1/.x0 by A8,A9;
thus (f1(#)f2)/.x-(f1(#)f2)/.x0 = (f1/.x)*(f2/.x)-(f1(#)f2)/.x0 by A12,A16,
CFUNCT_1:3
.= (f1/.x)*(f2/.x)+-(f1/.x)*(f2/.x0)+(f1/.x)*(f2/.x0)-(f1/.x0)*(f2/.x0
) by A12,A14,CFUNCT_1:3
.= (f1/.x)*((f2/.x)-(f2/.x0))+((f1/.x)-(f1/.x0))*(f2/.x0)
.= (f1/.x)*((f2/.x)-(f2/.x0))+(L1/.(x-x0)+R1/.(x-x0))*(f2/.x0) by A8,A9
,A16
.= (f1/.x)*((f2/.x)-(f2/.x0))+((f2/.x0)*L1/.(x-x0)+R1/.(x-x0)*(f2/.x0)
)
.= (f1/.x)*((f2/.x)-(f2/.x0))+(L11/.(x-x0)+(f2/.x0)*R1/.(x-x0)) by
CFUNCT_1:65,A15
.= (L1/.(x-x0)+R1/.(x-x0)+f1/.x0)*((f2/.x) -(f2/.x0))+(L11/.(x-x0)+R11
/.(x-x0)) by A17,CFUNCT_1:65,A15
.= (L1/.(x-x0)+R1/.(x-x0)+f1/.x0)*(L2/.(x-x0)+R2/.(x-x0)) +(L11/.(x-x0
)+R11/.(x-x0)) by A5,A10,A16
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +((f1/.x0)*L2/.(x-
x0)+(f1/.x0)*R2/.(x-x0))+(L11/.(x-x0)+R11/.(x-x0))
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +(L12/.(x-x0)+(f1/.
x0)*R2/.(x-x0))+(L11/.(x-x0)+R11/.(x-x0)) by CFUNCT_1:65,A15
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +(L12/.(x-x0)+R12/.
(x-x0))+(L11/.(x-x0)+R11/.(x-x0)) by CFUNCT_1:65,A15
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +(L12/.(x-x0)+(L11
/.(x-x0)+(R11/.(x-x0)+R12/.(x-x0))))
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +(L12/.(x-x0)+(L11
/.(x-x0)+R13/.(x-x0))) by CFUNCT_1:64,A15
.= (L1/.(x-x0)+R1/.(x-x0))*(L2/.(x-x0)+R2/.(x-x0)) +(L11/.(x-x0)+L12/.
(x-x0)+R13/.(x-x0))
.= (L1/.(x-x0)*L2/.(x-x0)+L1/.(x-x0)*R2/.(x-x0))+R1/.(x-x0)*(L2/.(x-x0
) +R2/.(x-x0))+(L/.(x-x0)+R13/.(x-x0)) by CFUNCT_1:64,A15
.= R14/.(x-x0)+R2/.(x-x0)*L1/.(x-x0)+R1/.(x-x0)*(L2/.(x-x0)+R2/.(x-x0)
) +(L/.(x-x0)+R13/.(x-x0)) by CFUNCT_1:64,A15
.= R14/.(x-x0)+R18/.(x-x0)+(R1/.(x-x0)*L2/.(x-x0)+R1/.(x-x0)*R2/.(x-x0
)) +(L/.(x-x0)+R13/.(x-x0)) by CFUNCT_1:64,A15
.= R14/.(x-x0)+R18/.(x-x0)+(R16/.(x-x0)+R1/.(x-x0)*R2/.(x-x0)) +(L/.(x
-x0)+R13/.(x-x0)) by CFUNCT_1:64,A15
.= R14/.(x-x0)+R18/.(x-x0)+(R16/.(x-x0)+R17/.(x-x0)) +(L/.(x-x0)+R13/.
(x-x0)) by CFUNCT_1:64,A15
.= R14/.(x-x0)+R18/.(x-x0)+R19/.(x-x0)+(L/.(x-x0)+R13/.(x-x0)) by
CFUNCT_1:64,A15
.= R14/.(x-x0)+(R19/.(x-x0)+R18/.(x-x0))+(L/.(x-x0)+R13/.(x-x0))
.= L/.(x-x0)+R13/.(x-x0)+(R14/.(x-x0)+R20/.(x-x0)) by CFUNCT_1:64,A15
.= L/.(x-x0)+(R13/.(x-x0)+R14/.(x-x0)+R20/.(x-x0))
.= L/.(x-x0)+(R15/.(x-x0)+R20/.(x-x0)) by CFUNCT_1:64,A15
.= L/.(x-x0)+R/.(x-x0) by CFUNCT_1:64,A15;
end;
hence f1(#)f2 is_differentiable_in x0 by A12;
hence diff(f1(#)f2,x0) = L/.1r by A12,A13,Def7
.= L11/.1r+L12/.1r by CFUNCT_1:64
.= f2/.x0*L1/.1r+L12/.1r by CFUNCT_1:65
.= f2/.x0*L1/.1r+f1/.x0 *L2/.1r by CFUNCT_1:65
.= f2/.x0*diff(f1,x0)+f1/.x0*L2/.1r by A1,A6,A8,Def7
.= f2/.x0*diff(f1,x0)+f1/.x0*diff(f2,x0) by A2,A3,A5,Def7;
end;
theorem
for f,Z st Z c= dom f & f|Z = id Z holds f is_differentiable_on Z &
for x st x in Z holds (f`|Z)/.x = 1r
proof
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX;
set R = cf;
reconsider L = id COMPLEX as PartFunc of COMPLEX,COMPLEX;
A1: COMPLEX c= COMPLEX;
for b holds L/.b = 1r*b
proof let b;
b in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1,PARTFUN2:6;
end;
then reconsider L as C_LinearFunc by Def4;
now
let h;
now
let n be Nat;
A3: n in NAT & rng h c= dom R by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by VALUED_1:5
.= (h").n*(R/.(h.n)) by A3,FUNCT_2:109
.= (h".n)*0c
.= 0c;
end;
then (h")(#)(R/*h) is constant & ((h")(#)(R/*h)).0 = 0c by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0c by CFCONT_1:26
,27;
end;
then reconsider R as C_RestFunc by Def3;
let f, Z;
assume that
A4: Z c= dom f and
A5: f|Z = id Z;
A6: now
let x be Complex;
assume
A7: x in Z;
then (f|Z).x = x by A5,FUNCT_1:18;
then f.x = x by A7,FUNCT_1:49;
hence f/.x = x by A4,A7,PARTFUN1:def 6;
end;
A8: now
let x0;
assume
A9: x0 in Z;
then consider N being Neighbourhood of x0 such that
A10: N c= Z by Th9;
A11: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A12: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
hence f/.x-f/.x0 = x-f/.x0 by A6,A10
.= x-x0 by A6,A9
.= L/.(x-x0)+0c by A1,PARTFUN2:6,A12
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A12;
end;
N c= dom f by A4,A10;
hence f is_differentiable_in x0 by A11;
end;
hence
A13: f is_differentiable_on Z by A4,Th15;
let x0;
assume
A14: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A15: N1 c= Z by Th9;
A16: f is_differentiable_in x0 by A8,A14;
then ex N being Neighbourhood of x0 st N c= dom f & ex L,R st for x st x in
N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0);
then consider N being Neighbourhood of x0 such that
A17: N c= dom f;
consider N2 being Neighbourhood of x0 such that
A18: N2 c= N1 and
A19: N2 c= N by Lm1;
A20: N2 c= dom f by A17,A19;
A21: for x st x in N2 holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A22: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N2;
then x in N1 by A18;
hence f/.x-f/.x0 = x-f/.x0 by A6,A15
.= x-x0 by A6,A14
.= L/.(x-x0)+0c by A1,PARTFUN2:6,A22
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A22;
end;
thus (f`|Z)/.x0 = diff(f,x0) by A13,A14,Def12
.= L/.1r by A16,A20,A21,Def7
.= 1r;
end;
theorem
for f1,f2,Z st Z c= dom (f1+f2) & f1 is_differentiable_on Z & f2
is_differentiable_on Z holds f1+f2 is_differentiable_on Z & for x st x in Z
holds ((f1+f2)`|Z)/.x = diff(f1,x)+diff(f2,x)
proof
let f1,f2,Z;
assume that
A1: Z c= dom (f1+f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th15;
hence f1+f2 is_differentiable_in x0 by Th23;
end;
hence
A3: f1+f2 is_differentiable_on Z by A1,Th15;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th15;
thus ((f1+f2)`|Z)/.x = diff((f1+f2),x) by A3,A4,Def12
.= diff(f1,x)+diff(f2,x) by A5,Th23;
end;
hence thesis;
end;
theorem
for f1,f2,Z st Z c= dom (f1-f2) & f1 is_differentiable_on Z & f2
is_differentiable_on Z holds f1-f2 is_differentiable_on Z & for x st x in Z
holds ((f1-f2)`|Z)/.x = diff(f1,x)-diff(f2,x)
proof
let f1,f2,Z;
assume that
A1: Z c= dom (f1-f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th15;
hence f1-f2 is_differentiable_in x0 by Th24;
end;
hence
A3: f1-f2 is_differentiable_on Z by A1,Th15;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th15;
thus ((f1-f2)`|Z)/.x = diff((f1-f2),x) by A3,A4,Def12
.= diff(f1,x)-diff(f2,x) by A5,Th24;
end;
hence thesis;
end;
theorem
for a,f,Z st Z c= dom (a(#)f) & f is_differentiable_on Z holds a(#)f
is_differentiable_on Z & for x st x in Z holds ((a(#)f)`|Z)/.x = a*diff(f,x)
proof
let a,f,Z;
assume that
A1: Z c= dom (a(#)f) and
A2: f is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f is_differentiable_in x0 by A2,Th15;
hence a(#)f is_differentiable_in x0 by Th25;
end;
hence
A3: a(#)f is_differentiable_on Z by A1,Th15;
now
let x;
assume
A4: x in Z;
then
A5: f is_differentiable_in x by A2,Th15;
thus ((a(#)f)`|Z)/.x = diff((a(#)f),x) by A3,A4,Def12
.= a*diff(f,x) by A5,Th25;
end;
hence thesis;
end;
theorem
for f1,f2,Z st Z c= dom (f1(#)f2) & f1 is_differentiable_on Z & f2
is_differentiable_on Z holds f1(#)f2 is_differentiable_on Z & for x st x in Z
holds ((f1(#)f2)`|Z)/.x = (f2/.x)*diff(f1,x)+(f1/.x)*diff(f2,x)
proof
let f1,f2,Z;
assume that
A1: Z c= dom (f1(#)f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th15;
hence f1(#)f2 is_differentiable_in x0 by Th26;
end;
hence
A3: f1(#)f2 is_differentiable_on Z by A1,Th15;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th15;
thus ((f1(#)f2)`|Z)/.x = diff((f1(#)f2),x) by A3,A4,Def12
.= f2/.x*diff(f1,x)+f1/.x*diff(f2,x) by A5,Th26;
end;
hence thesis;
end;
theorem
Z c= dom f & f|Z is constant implies f is_differentiable_on Z & for x
st x in Z holds (f`|Z)/.x = 0c
proof
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX;
set R = cf;
now
let h;
now
let n be Nat;
A2: n in NAT & rng h c= dom R by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by VALUED_1:5
.= (h".n)*(R/.(h.n)) by A2,FUNCT_2:109
.= (h".n)*0c
.= 0c;
end;
then (h")(#)(R/*h) is constant & ((h")(#)(R/*h)).0 = 0c by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0c by CFCONT_1:26
,27;
end;
then reconsider R as C_RestFunc by Def3;
set L = cf;
for x holds L/.x = 0c*x
by XCMPLX_0:def 2,FUNCOP_1:7;
then reconsider L as C_LinearFunc by Def4;
assume that
A3: Z c= dom f and
A4: f|Z is constant;
consider a1 being Element of COMPLEX such that
A5: for x being Element of COMPLEX st x in Z/\dom f holds f/.x = a1
by A4,PARTFUN2:35;
A6: now
let x0;
assume
A7: x0 in Z;
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: N c= dom f by A3,A8;
A10: x0 in Z/\dom f by A3,A7,XBOOLE_0:def 4;
for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A11: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
then x in Z/\dom f by A8,A9,XBOOLE_0:def 4;
hence f/.x-f/.x0 = a1-f/.x0 by A5
.= a1-a1 by A5,A10
.= L/.(x-x0)+0c by FUNCOP_1:7,A11
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A11;
end;
hence f is_differentiable_in x0 by A9;
end;
hence
A12: f is_differentiable_on Z by A3,Th15;
let x0;
assume
A13: x0 in Z;
then consider N being Neighbourhood of x0 such that
A14: N c= Z by Th9;
A15: N c= dom f by A3,A14;
A16: x0 in Z/\dom f by A3,A13,XBOOLE_0:def 4;
A17: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A18: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
then x in Z/\dom f by A14,A15,XBOOLE_0:def 4;
hence f/.x-f/.x0 = a1-f/.x0 by A5
.= a1-a1 by A5,A16
.= L/.(x-x0)+0c by FUNCOP_1:7,A18
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A18;
end;
A19: f is_differentiable_in x0 by A6,A13;
thus (f`|Z)/.x0 = diff(f,x0) by A12,A13,Def12
.= L/.1r by A19,A15,A17,Def7
.= 0c;
end;
theorem
Z c= dom f & (for x st x in Z holds f/.x = a*x+b) implies f
is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = a
proof
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX;
set R = cf;
now
let h;
now
let n be Nat;
A2: n in NAT & rng h c= dom R by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by VALUED_1:5
.= (h".n)*(R/.(h.n)) by A2,FUNCT_2:109
.= (h".n)*0c
.= 0c;
end;
then (h")(#)(R/*h) is constant & ((h")(#)(R/*h)).0 = 0c by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0c by CFCONT_1:26
,27;
end;
then reconsider R as C_RestFunc by Def3;
assume that
A3: Z c= dom f and
A4: for x st x in Z holds f/.x = a*x+b;
deffunc G(Complex) = In(a*$1,COMPLEX);
consider L being Function of COMPLEX,COMPLEX such that
A5: for x being Element of COMPLEX holds L.x = G(x) from FUNCT_2:sch 4;
for z holds L/.z = a*z
proof let z;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
L.z = G(z) by A5;
hence thesis;
end;
then reconsider L as C_LinearFunc by Def4;
A6: now
let x0;
assume
A7: x0 in Z;
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A10: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
hence f/.x-f/.x0 = a*x+b-f/.x0 by A4,A8
.= a*x+b-(a*x0+b) by A4,A7
.= G(x-x0)+0c
.= L/.(x-x0)+0c by A5,A10
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A10;
end;
N c= dom f by A3,A8;
hence f is_differentiable_in x0 by A9;
end;
hence
A11: f is_differentiable_on Z by A3,Th15;
let x0;
assume
A12: x0 in Z;
then consider N being Neighbourhood of x0 such that
A13: N c= Z by Th9;
A14: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0)
proof
let x;
A15: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N;
hence f/.x-f/.x0 = a*x+b-f/.x0 by A4,A13
.= a*x+b-(a*x0+b) by A4,A12
.= G(x-x0)+0c
.= L/.(x-x0)+0c by A5,A15
.= L/.(x-x0)+R/.(x-x0) by FUNCOP_1:7,A15;
end;
A16: N c= dom f by A3,A13;
A17: f is_differentiable_in x0 by A6,A12;
thus (f`|Z)/.x0 = diff(f,x0) by A11,A12,Def12
.= L/.1r by A17,A16,A14,Def7
.= G(1r) by A5
.= a;
end;
theorem Th34:
for x0 be Complex holds f is_differentiable_in x0 implies f
is_continuous_in x0
proof
let x0 be Complex;
assume
A1: f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L,R st for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R /.(x-x0);
A3: x0 in N by Th7;
now
consider g be 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 such that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n holds s1.n <> x0;
consider l be Nat such that
A10: for m be 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 G(Nat) = In(s1.$1-s2.$1,COMPLEX);
consider s3 such that
A12: for n being Element of NAT holds s3.n = G(n) from FUNCT_2:sch 4;
A13: for n holds s3.n = s1.n-s2.n
proof let n;
n in NAT by ORDINAL1:def 12;
then s3.n = G(n) by A12;
hence thesis;
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
given n being Element of NAT such that
A19: s3.n = 0c;
s1.n-s2.n = 0c by A13,A19;
hence contradiction by A9;
end;
A20: now
given n being Element of NAT such that
A21: (s3^\l).n = 0c;
A22: n+l in NAT by ORDINAL1:def 12;
s3.(n+l) = 0c by A21,NAT_1:def 3;
hence contradiction by A18,A22;
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 0-convergent non-zero Complex_Sequence
by A17,A23,Def1;
now
let n be Element of NAT;
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;
end;
then
A24: f/*(h+c)-f/*c+(f/*c) = f/*(h+c);
now
let n be Element of NAT;
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;
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}
proof
let y be object;
assume y in rng c;
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 thesis by TARSKI:def 1;
end;
let y be object;
assume y in {x0};
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 thesis by FUNCT_2:4;
end;
A32: now
let p be Real such that
A33: 0 < p;
reconsider n = 0 as Nat;
take n;
thus for m st n <= m holds |.(f/*c).m-f/.x0.| < p
proof
let m such that
n <= m;
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 thesis by A33;
end;
end;
then
A36: f/*c is convergent;
now
let n be Element of NAT;
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;
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;
assume
A39: y in rng(h+c);
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 thesis by A5;
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;
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;
end;
hence thesis by A2,A3,CFCONT_1:31;
end;
theorem
f is_differentiable_on X implies f is_continuous_on X
proof
assume
A1: f is_differentiable_on X;
hence
A2: X c= dom f;
let x be Complex;
assume x in X;
then
A3: x in dom (f|X) by A2,RELAT_1:57;
f|X is differentiable by A1;
then f|X is_differentiable_in x by A3;
hence thesis by Th34;
end;
theorem
f is_differentiable_on X & Z c= X implies f is_differentiable_on Z
proof
assume that
A1: f is_differentiable_on X and
A2: Z c= X;
A3: f|X is differentiable by A1;
X c= dom f by A1;
hence Z c= dom f by A2;
let x0;
assume
A4: x0 in dom (f|Z);
then
A5: x0 in dom f by RELAT_1:57;
A6: x0 in Z by A4,RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A7: N1 c= Z by Th9;
x0 in dom (f|X) by A2,A5,A6,RELAT_1:57;
then f|X is_differentiable_in x0 by A3;
then consider N being Neighbourhood of x0 such that
A8: N c= dom(f|X) and
A9: ex L,R st for x st x in N holds (f|X)/.x-(f|X)/.x0 = L/.(x-x0)+R/.(
x-x0);
consider N2 being Neighbourhood of x0 such that
A10: N2 c= N and
A11: N2 c= N1 by Lm1;
A12: N2 c= Z by A7,A11;
take N2;
dom(f|X) = dom f/\X by RELAT_1:61;
then dom(f|X) c= dom f by XBOOLE_1:17;
then N c= dom f by A8;
then N2 c= dom f by A10;
then N2 c= dom f/\Z by A12,XBOOLE_1:19;
hence
A13: N2 c= dom(f|Z) by RELAT_1:61;
consider L,R such that
A14: for x st x in N holds (f|X)/.x-(f|X)/.x0 = L/.(x-x0)+R/.(x-x0) by A9;
take L,R;
let x;
assume
A15: x in N2;
then (f|X)/.x-(f|X)/.x0 = L/.(x-x0)+R/.(x-x0) by A10,A14;
then
A16: (f|X)/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A2,A5,A6,PARTFUN2:17;
x in N by A10,A15;
then f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A8,A16,PARTFUN2:15;
then f/.x-(f|Z)/.x0 = L/.(x-x0)+R/.(x-x0) by A5,A6,PARTFUN2:17;
hence thesis by A13,A15,PARTFUN2:15;
end;
::$CT
theorem
f is_differentiable_in x0 implies ex R st R/.0c = 0c & R is_continuous_in 0c
proof
assume f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
N c= dom f and
A1: ex L,R st for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0);
consider L,R such that
A2: for x st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A1;
take R;
consider a such that
A3: for z holds L/.z = a*z by Def4;
f/.x0-f/.x0 = L/.(x0-x0)+R/.(x0-x0) by A2,Th7;
then
A4: 0c = a*0c+R/.0c by A3;
hence R/.0c = 0c;
A5: now
let h;
(h")(#)(R/*h) is bounded by Def3;
then consider M being Real such that
M > 0 and
A6: for n holds |.((h")(#)(R/*h)).n.| < M by COMSEQ_2:8;
lim h = 0 by Def1;
then lim |.h.| = |. 0 .| by SEQ_2:27;
then
A7: lim (M(#)|.h.|) = M * |. 0 .| by SEQ_2:8
.=M*0 by ABSVALUE:2
.=0;
A8: now
let p be Real;
assume 0 < p;
then consider m such that
A9: for n st m <= n holds |.(M(#)|.h.|).n-0 .| < p by A7,SEQ_2:def 7;
take m;
now
let n;
assume m <= n;
then
A10: |.(M(#)|.h.|).n-0 .| < p by A9;
|.((h")(#)(R/*h)).n.| = |.((h").n)*(R/*h).n.| by VALUED_1:5
.= |.(h.n)"*(R/*h).n.| by VALUED_1:10;
then
A11: |.(h.n)"*(R/*h).n.| <= M by A6;
A12: n in NAT by ORDINAL1:def 12;
|.(h.n).| >= 0 by COMPLEX1:46;
then |.(h.n).|*|.(h.n)"*(R/*h).n.| <= M*|.(h.n).| by A11,XREAL_1:64;
then |.(h.n)*((h.n)"*(R/*h).n).| <= M*|.(h.n).| by COMPLEX1:65;
then h.n <> 0c & |.(h.n)*(h.n)"*(R/*h).n.| <= M*|.(h.n).|
by COMSEQ_1:4,A12;
then |.1r*(R/*h).n.| <= M*|.(h.n).| by XCMPLX_0:def 7;
then |.(R/*h).n.| <= M*|.h.|.n by VALUED_1:18;
then
A13: |.(R/*h).n.| <= (M(#)|.h.|).n by SEQ_1:9;
0 <= |.(R/*h).n.| by COMPLEX1:46;
then 0 <= (M(#)|.h.|).n by A13;
then (M(#)|.h.|).n < p by A10,ABSVALUE:def 1;
hence |.(R/*h).n-0c.| < p by A13,XXREAL_0:2;
end;
hence for n st m <= n holds |.(R/*h).n-0c.| < p;
end;
hence R/*h is convergent;
hence lim (R/*h) = R/.0c by A4,A8,COMSEQ_2:def 6;
end;
A14: now
let s1;
assume that
rng s1 c= dom R and
A15: s1 is convergent & lim s1 = 0 and
A16: for n holds s1.n <> 0;
for n being Element of NAT holds s1.n <> 0 by A16;
then s1 is non-zero by COMSEQ_1:4;
then s1 is 0-convergent non-zero Complex_Sequence by A15,Def1;
hence R/*s1 is convergent & lim (R/*s1) = R/.0c by A5;
end;
dom R = COMPLEX by PARTFUN1:def 2;
hence thesis by A14,CFCONT_1:31;
end;