:: Cauchy-Riemann Differential Equations of Complex Functions
:: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura
::
:: Received April 7, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users

begin

Lm1: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent iff cseq is convergent )

proof end;

Lm2: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim

proof end;

Lm3: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim

proof end;

Lm4: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent_to_0 iff cseq is convergent_to_0 )

proof end;

theorem Th1: :: CFDIFF_2:1

for f being PartFunc of COMPLEX,COMPLEX st f is total holds
( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )

proof end;

Lm5: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds
( seq is non-empty iff cseq is non-empty )

proof end;

Lm6: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds
( seq is convergent_to_0 iff cseq is convergent_to_0 )

proof end;

theorem Th2: :: CFDIFF_2:2

for f being PartFunc of COMPLEX,COMPLEX
for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 end;

Lm7: for x, y being Real
for vx, vy being Point of (REAL-NS 1) st vx = <*x*> & vy = <*y*> holds
( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> )

proof end;

Lm8: for x, y, z, w being Real
for vx, vy being Element of REAL 2 st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )

proof end;

Lm9: for x, y, a being Real
for vx being Element of REAL 2 st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>

proof end;

Lm10: for x, y being Real holds <*x,y*> is Point of (REAL-NS 2)

proof end;

Lm11: for x, y, z, w being Real
for vx, vy being Point of (REAL-NS 2) st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )

proof end;

Lm12: for x, y, a being Real
for vx being Point of (REAL-NS 2) st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>

proof end;

Lm13: for u being PartFunc of (REAL 2),REAL
for xy being Element of REAL 2 st xy in dom u holds
(<>* u) . xy = <*(u . xy)*>

proof end;

Lm14: for u being PartFunc of (REAL 2),REAL
for x, y being Real st <*x,y*> in dom u holds
(<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*>

proof end;

Lm15: for x, y being Real
for z being Complex
for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds
|.z.| = ||.v.||

proof end;

Lm16: for x, y being Real
for z being Complex st z = x + (y * <i>) holds
|.z.| <= (abs x) + (abs y)

proof end;

Lm17: for x, y being Real holds
( abs x <= |.(x + (y * <i>)).| & abs y <= |.(x + (y * <i>)).| )

proof end;

Lm18: for x, y being Real
for v being Element of (REAL-NS 2) st v = <*x,y*> holds
||.v.|| <= (abs x) + (abs y)

proof end;

theorem Th3: :: CFDIFF_2:3

for seq being Real_Sequence holds
( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) )

proof end;

theorem Th4: :: CFDIFF_2:4

for X being RealNormSpace
for seq being sequence of X holds
( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) )

proof end;

Lm19: for x being Real
for vx being Element of (REAL-NS 2) st vx = <*x,0*> holds
||.vx.|| = abs x

proof end;

Lm20: for x being Real
for vx being Element of (REAL-NS 2) st vx = <*0,x*> holds
||.vx.|| = abs x

proof end;

Lm21: for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x

proof end;

Lm22: for v being Element of (REAL-NS 1) holds abs ((proj (1,1)) . v) = ||.v.||

proof end;

theorem Th5: :: CFDIFF_2:5

for u being PartFunc of (REAL 2),REAL
for x0, y0 being Real
for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> )

proof end;

theorem :: CFDIFF_2:6

for f being PartFunc of COMPLEX,COMPLEX
for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds
( f is_differentiable_in z0 & 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 end;