:: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura

::

:: Received April 7, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

Lm1: for seq being Real_Sequence

for cseq being Complex_Sequence

for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds

lim cseq = rlim

proof end;

Lm2: 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;

Lm3: for seq being Real_Sequence

for cseq being Complex_Sequence st seq = cseq holds

( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )

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 )

( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )

proof end;

Lm4: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds

( seq is non-zero iff cseq is non-zero )

proof end;

Lm5: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds

( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )

proof end;

:: Cauchy-Riemann

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) )

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;

Lm6: 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;

Lm7: 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;

Lm8: 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;

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

proof end;

Lm10: 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;

Lm11: 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;

Lm12: 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;

Lm13: 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;

Lm14: 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;

Lm15: for x, y being Real

for z being Complex st z = x + (y * <i>) holds

|.z.| <= |.x.| + |.y.|

proof end;

Lm16: for x, y being Real holds

( |.x.| <= |.(x + (y * <i>)).| & |.y.| <= |.(x + (y * <i>)).| )

proof end;

Lm17: for x, y being Real

for v being Element of (REAL-NS 2) st v = <*x,y*> holds

||.v.|| <= |.x.| + |.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 ) )

( 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 ) )

for seq being sequence of X holds

( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) )

proof end;

Lm18: for x being Real

for vx being Element of (REAL-NS 2) st vx = <*x,0*> holds

||.vx.|| = |.x.|

proof end;

Lm19: for x being Real

for vx being Element of (REAL-NS 2) st vx = <*0,x*> holds

||.vx.|| = |.x.|

proof end;

Lm20: for x being Real

for vx being Element of (REAL-NS 1) st vx = <*x*> holds

||.vx.|| = |.x.|

proof end;

Lm21: for v being Element of (REAL-NS 1) holds |.((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*> )

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;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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) )

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;