:: Cauchy-Riemann Differential Equations of Complex Functions :: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura :: :: Received April 7, 2009 :: Copyright (c) 2009-2021 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, PARTFUN1, REAL_1, SEQ_1, COMSEQ_1, SEQ_2, CARD_1, FUNCT_1, COMPLEX1, RELAT_1, NAT_1, ORDINAL2, ARYTM_3, XXREAL_0, ARYTM_1, FDIFF_1, VALUED_0, XCMPLX_0, VALUED_1, FINSEQ_1, PDIFF_1, AFINSQ_1, CARD_3, RCOMP_1, TARSKI, CFDIFF_1, FUNCT_2, XXREAL_1, PRE_TOPC, REAL_NS1, BINOP_2, NORMSP_1, EUCLID, MCART_1, RVSUM_1, SQUARE_1, SUPINF_2, STRUCT_0, LOPBAN_1, FUNCT_7; notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, BINOP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, BINOP_2, XREAL_0, COMPLEX1, REAL_1, VALUED_1, SEQ_1, SEQ_2, RLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, PRE_TOPC, STRUCT_0, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_7, SQUARE_1, EUCLID, NORMSP_0, NORMSP_1, REAL_NS1, LOPBAN_1, NFCONT_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, RCOMP_1; constructors REAL_1, SQUARE_1, RSSPACE3, SEQ_2, BINOP_2, FINSEQ_7, NFCONT_1, RCOMP_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, COMSEQ_2, COMSEQ_3, RVSUM_1, RELSET_1, BINOP_1, NUMBERS, EXTREAL1, FINSEQ_4; registrations RELSET_1, STRUCT_0, ORDINAL1, MEMBERED, NUMBERS, XBOOLE_0, XREAL_0, XXREAL_0, XCMPLX_0, FUNCT_2, REAL_NS1, COMSEQ_3, VALUED_0, VALUED_1, SEQ_4, FDIFF_1, CFDIFF_1, EUCLID, COMSEQ_2, SQUARE_1, RVSUM_1, CFUNCT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin reserve n, m for Element of NAT; reserve z for Complex; theorem :: CFDIFF_2:1 for f be PartFunc of COMPLEX,COMPLEX st f is total holds dom (Re f) = COMPLEX & dom (Im f) = COMPLEX; :: Cauchy-Riemann theorem :: CFDIFF_2:2 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); theorem :: CFDIFF_2:3 for seq be Real_Sequence holds seq is convergent & lim seq = 0 iff abs seq is convergent & lim abs seq = 0; theorem :: CFDIFF_2:4 for X be RealNormSpace, seq be sequence of X holds seq is convergent & lim seq = 0.X iff ||. seq .|| is convergent & lim ||. seq .|| = 0; theorem :: CFDIFF_2:5 for u be PartFunc of REAL 2, REAL, x0, y0 be Real, xy0 be 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 *>); theorem :: CFDIFF_2:6 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 v holds x+y* in dom f) & (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*> & <>*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);