(#) seq holds seq is
non-zero iff cseq is non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = * (#) seq;
thus seq is non-zero implies cseq is non-zero by A1,COMSEQ_1:38;
A2: (#) seq is non-zero implies seq is non-zero
proof
assume
A3: (#) seq is non-zero;
now
let n;
( (#) seq).n <> 0c by A3,COMSEQ_1:4;
then * seq.n <> 0c by VALUED_1:6;
hence seq.n <> 0c;
end;
hence thesis by COMSEQ_1:4;
end;
assume cseq is non-zero;
hence seq is non-zero by A1,A2;
end;
Lm5: for seq, cseq be Complex_Sequence st cseq = (#) seq holds seq is
0-convergent non-zero iff cseq is 0-convergent non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = (#) seq;
thus seq is 0-convergent non-zero implies cseq is 0-convergent non-zero
proof
assume
A2: seq is 0-convergent non-zero;
then lim seq = 0 by CFDIFF_1:def 1;
then
A3: lim ( (#) seq) = * 0 by A2,COMSEQ_2:18
.= 0;
(#) seq is non-zero & (#) seq is convergent by A2,COMSEQ_1:38;
hence cseq is 0-convergent non-zero by A1,A3,CFDIFF_1:def 1;
end;
assume
A4: cseq is 0-convergent non-zero;
then
A5: seq is non-zero by A1,Lm4;
(-) (#) ( (#) seq ) is convergent by A1,A4;
then ((-) * ) (#) seq is convergent by CFUNCT_1:22;
then
A6: seq is convergent by CFUNCT_1:26;
lim ( (#) seq) = 0 by A1,A4,CFDIFF_1:def 1;
then * lim seq = 0 by A6,COMSEQ_2:18;
hence seq is 0-convergent non-zero by A6,A5,CFDIFF_1:def 1;
end;
:: Cauchy-Riemann
theorem Th2:
for f be PartFunc of COMPLEX, COMPLEX, u,v be PartFunc of REAL 2,
REAL, z0 be Complex, x0, y0 be Real,
xy0 be Element of REAL 2 st (for x, y be
Real st x+y* in dom f holds <*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*))
& (for x,y be Real st x+y* in dom f holds <*x,y*> in dom v & v.<*x,y*> = (Im
f).(x+y*)) & z0 = x0+y0* & xy0 = <*x0,y0*> & f is_differentiable_in z0
holds u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0
,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,
2 & Re diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) & Im
diff(f,z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1)
proof
let f be PartFunc of COMPLEX,COMPLEX, u,v be PartFunc of REAL 2,REAL, z0 be
Complex, x00,y00 be Real ,xy0 be Element of REAL 2 such that
A1: for x,y be Real st x+y* in dom f holds <*x,y*> in dom u & u.<*x,y
*> = (Re f).(x+y*) and
A2: for x,y be Real st x+y* in dom f holds <*x,y*> in dom v & v.<*x,y
*> = (Im f).(x+y*) and
A3: z0 = x00+y00* and
A4: xy0 = <*x00,y00*> and
A5: f is_differentiable_in z0;
reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;
A6: z0 = x0+y0* by A3;
A7: xy0 = <*x0,y0*> by A4;
deffunc LDF2(Real) = In((Im diff(f,z0))* $1,REAL);
consider LD2 be Function of REAL, REAL such that
A8: for x be Element of REAL holds LD2.x = LDF2(x) from FUNCT_2:sch 4;
A9: for x be Real holds LD2.x = (Im diff(f,z0))* x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD2.x = LDF2(x) by A8;
hence thesis;
end;
reconsider LD2 as LinearFunc by A9,FDIFF_1:def 3;
deffunc LDF1(Real) = In((Re diff(f,z0)) * $1,REAL);
consider LD1 be Function of REAL, REAL such that
A10: for x be Element of REAL holds LD1.x = LDF1(x) from FUNCT_2:sch 4;
A11: for x be Real holds LD1.x = (Re diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD1.x = LDF1(x) by A10;
hence thesis;
end;
A12: for y be Real holds (v*reproj(2,xy0)).y = v.<*x0,y*>
proof
let y be Real;
reconsider yy=y, dwa=2 as Element of REAL by XREAL_0:def 1;
yy in REAL;
then yy in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (v*reproj(2,xy0)).y = v.((reproj(2,xy0)).y) by FUNCT_1:13
.=v.(Replace(xy0,2,yy)) by PDIFF_1:def 5
.=v.<*x0,yy*> by A7,FINSEQ_7:14
.=v.<*x0,y*>;
end;
A13: for y be Real holds (u*reproj(2,xy0)).y=u.<*x0,y*>
proof
let y be Real;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
y in REAL by XREAL_0:def 1;
then y in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (u*reproj(2,xy0)).y = u.((reproj(2,xy0)).y) by FUNCT_1:13
.= u.(Replace(xy0,2,yy)) by PDIFF_1:def 5
.= u.<*x0,y*> by A7,FINSEQ_7:14;
end;
A14: proj(2,2).xy0 = xy0.2 by PDIFF_1:def 1
.= y0 by A7,FINSEQ_1:44;
reconsider LD1 as LinearFunc by A11,FDIFF_1:def 3;
deffunc LDF3(Real) = In(-(Im diff(f,z0)) * $1,REAL);
consider LD3 be Function of REAL,REAL such that
A15: for x be Element of REAL holds LD3.x = LDF3(x) from FUNCT_2:sch 4;
A16: for x be Real holds LD3.x = -(Im diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD3.x = LDF3(x) by A15;
hence thesis;
end;
for x be Real holds LD3.x = (-(Im diff(f,z0)))* x
proof
let x be Real;
thus LD3.x = -(Im diff(f,z0)) * x by A16
.= (-(Im diff(f,z0)))* x;
end;
then reconsider LD3 as LinearFunc by FDIFF_1:def 3;
reconsider z0 as Element of COMPLEX by XCMPLX_0:def 2;
consider N being Neighbourhood of z0 such that
A17: N c= dom f and
A18: ex L be C_LinearFunc, R be C_RestFunc st diff(f,z0) = L/.1r &
for z being Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A5,CFDIFF_1:def 7;
consider L be C_LinearFunc, R be C_RestFunc such that
A19: diff(f,z0) = L/.1r & for z be Complex st
z in N holds f/.z-f/.z0 = L/.(z-z0) +R/.(z-z0) by A18;
deffunc RF4(Real) = In((Im R).($1*),REAL);
consider R4 be Function of REAL, REAL such that
A20: for y be Element of REAL holds R4.y =RF4(y) from FUNCT_2:sch 4;
A21: for z be Complex st z in N holds f/.z-f/.z0 = diff(f,z0)*(z-z0)+R/.(z-z0)
proof
let z be Complex;
assume
A22: z in N;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
consider a0 be Complex such that
A23: for w be Complex holds L/.w = a0*w by CFDIFF_1:def 4;
L/.(1r*(z-z0)) = a0*1r*(z-z0) by A23
.= (L/.1r)*(z-z0) by A23;
hence thesis by A19,A22;
end;
A24: for x,y be Real st x+y* in N & x0+y0* in N holds
f.(x+y*)-f.(x0+y0*) =
diff(f,z0)*((x+y*)-(x0+y0*)) + R/.((x+y*)-(x0+y0*))
proof
let x,y be Real;
assume
A25: x+y* in N & x0+y0* in N;
then f.(x+y*) = f/.(x+y*) & f.(x0+y0*) = f/.(x0+y0*)
by A17,PARTFUN1:def 6;
hence thesis by A21,A25,A6;
end;
A26: dom R = COMPLEX by PARTFUN1:def 2;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R4/*h) is
convergent & lim ((h")(#)(R4/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=(#)hz0;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm5;
now
A27: rng hz c= dom R by A26;
dom R4=REAL by PARTFUN1:def 2;
then
A28: rng h c= dom R4;
let n be Nat;
A29: n in NAT by ORDINAL1:def 12;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A30: Im ((h.nn)" ) = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A31: hz.n = (h.n)* by VALUED_1:6;
reconsider hn = h.n as Real;
(h.n)* in COMPLEX by XCMPLX_0:def 2;
then
A32: (h.n)* in dom Im R by Th1;
thus ((h")(#)(R4/*h)).n = (h").n*((R4/*h).n) by SEQ_1:8
.= (h.n)"*((R4/*h).n) by VALUED_1:10
.= (h.n)"*(R4.hn) by A28,FUNCT_2:108,A29
.= (h.nn)"*RF4(hn) by A20
.= (h.n)"* (Im R).((h.n)*)
.= Re ((h.n)" )* Im (R.((h.n)*)) + Re (R.((h.n)*)) * Im ((h.
n)") by A32,A30,COMSEQ_3:def 4
.= Im (((hz.n)/) "* (R.(hz.n))) by A31,COMPLEX1:9
.= Im (( /(hz.n)) * (R.(hz.n))) by XCMPLX_1:213
.= Im ( *(hz").n * (R.(hz.n))) by VALUED_1:10
.= Im ( *((hz").n * (R.(hz.n))))
.= Re ( ) * Im ((hz").n * (R/.(hz.n))) + Re ((hz").n * (R/.(hz.n
)))*Im ( ) by COMPLEX1:9
.= Re ((hz").n * (R/*hz).n ) by A27,COMPLEX1:7,FUNCT_2:109,A29
.= Re (( (hz")(#)(R/*hz)).n ) by VALUED_1:5;
end;
then
A33: (h")(#)(R4/*h) = Re ((hz")(#)(R/*hz)) by COMSEQ_3:def 5;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3
;
hence thesis by A33,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider R4 as RestFunc by FDIFF_1:def 2;
deffunc RF2(Real) = In((Re R).($1*),REAL);
A34: dom R = COMPLEX by PARTFUN1:def 2;
consider R2 be Function of REAL,REAL such that
A35: for y be Element of REAL holds R2.y =RF2(y) from FUNCT_2:sch 4;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R2/*h) is
convergent & lim ((h")(#)(R2/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=(#)hz0;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm5;
A36: (hz")(#)(R/*hz) is convergent by CFDIFF_1:def 3;
dom R= COMPLEX by PARTFUN1:def 2;
then
A37: rng hz c= dom R;
now
dom R2=REAL by PARTFUN1:def 2;
then
A38: rng h c= dom R2;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A39: Im ((h.nn)" ) = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A40: hz.n=(h.n)* by VALUED_1:6;
dom Re R = COMPLEX by Th1;
then
A41: (h.n)* in dom Re R by XCMPLX_0:def 2;
A42: R.(hz.n) = R/.(hz.n);
reconsider hn = h.n as Real;
thus ((h")(#)(R2/*h)).n = (h").n*((R2/*h).n) by SEQ_1:8
.= (h.n)"*((R2/*h).n) by VALUED_1:10
.= (h.nn)"*(R2.(h.n)) by A38,FUNCT_2:108
.= (h.nn)"*(RF2(hn)) by A35
.= (h.n)"* (Re R).((h.n)*)
.= Re ((h.n)" )* Re (R.((h.n)*)) -Im ((h.n)") *Im (R.((h.n)*
)) by A41,A39,COMSEQ_3:def 3
.= Re (((hz.n)/) "* (R.(hz.n))) by A40,COMPLEX1:9
.= Re (( /(hz.n)) * (R.(hz.n))) by XCMPLX_1:213
.= Re ( *(hz").n * (R.(hz.n))) by VALUED_1:10
.= Re ( *((hz").n * (R.(hz.n))))
.= Re * Re ((hz").n * (R.(hz.n))) -
Im * Im ((hz").n * (R.(hz.n))) by COMPLEX1:9
.= -Im ((hz").nn * (R/*hz).nn ) by A42,A37,COMPLEX1:7,FUNCT_2:109
.= -Im (( (hz")(#)(R/*hz)).n ) by VALUED_1:5
.= - (Im ((hz")(#)(R/*hz))).n by COMSEQ_3:def 6;
end;
then
A43: (h")(#)(R2/*h) = - Im ((hz")(#)(R/*hz)) by SEQ_1:10;
lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3;
then lim Im ((hz")(#)(R/*hz)) = Im 0 by A36,COMSEQ_3:41;
then lim ((h")(#)(R2/*h)) = -Im 0 by A43,A36,SEQ_2:10
.= 0 by COMPLEX1:4;
hence thesis by A43,A36,SEQ_2:9;
end;
then reconsider R2 as RestFunc by FDIFF_1:def 2;
consider r0 be Real such that
A44: 0*