The abstract of the Mizar article:

Complex Numbers --- Basic Definitions

by

Library Committee

Received March 7, 2003

MML identifier: XCMPLX_0

[ Mizar article, MML identifier index ]

environ

 vocabulary XCMPLX_0, ARYTM_0, COMPLEX1, ARYTM, FUNCOP_1, BOOLE, FUNCT_1,
      FUNCT_2, ORDINAL2, ORDINAL1, RELAT_1, OPPCAT_1, ARYTM_1, ARYTM_2,
      ARYTM_3, XREAL_0;
 notation TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_4,
      ORDINAL1, ORDINAL2, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0;
 constructors ARYTM_1, FRAENKEL, FUNCT_4, ARYTM_0, XBOOLE_0;
 clusters NUMBERS, FRAENKEL, FUNCT_2, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET, NUMERALS;


begin

definition
 func <i> equals
:: XCMPLX_0:def 1
 (0,1) --> (0,1);
 let c be number;
 attr c is complex means
:: XCMPLX_0:def 2
 c in COMPLEX;
end;

definition
 cluster <i> -> complex;
end;

definition
 cluster complex number;
end;

definition let x be complex number;
  redefine attr x is empty means
:: XCMPLX_0:def 3
      x = 0;
  synonym x is zero;
end;

definition let x,y be complex number;
 func x+y means
:: XCMPLX_0:def 4
  ex x1,x2,y1,y2 being Element of REAL st
   x = [*x1,x2*] & y = [*y1,y2*] & it = [*+(x1,y1),+(x2,y2)*];
 commutativity;
 func x*y means
:: XCMPLX_0:def 5
  ex x1,x2,y1,y2 being Element of REAL st
   x = [*x1,x2*] & y = [*y1,y2*] &
    it = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *];
 commutativity;
end;

definition let z,z' be complex number;
 cluster z+z' -> complex;
 cluster z*z' -> complex;
end;

definition let z be complex number;
 func -z -> complex number means
:: XCMPLX_0:def 6
   z + it = 0;
 involutiveness;
 func z" -> complex number means
:: XCMPLX_0:def 7
   z*it = 1 if z <> 0
   otherwise it = 0;
  involutiveness;
end;

definition let x,y be complex number;
  func x-y equals
:: XCMPLX_0:def 8
    x+(-y);
  func x/y equals
:: XCMPLX_0:def 9
    x * y";
end;

definition let x,y be complex number;
  cluster x-y -> complex;
  cluster x/y -> complex;
end;

definition
 cluster non zero (complex number);
end;

definition let x be non zero (complex number);
  cluster -x -> non zero;
  cluster x" -> non zero;
 let y be non zero (complex number);
  cluster x*y -> non zero;
end;

definition let x,y be non zero (complex number);
  cluster x/y -> non zero;
end;

definition
  cluster -> complex Element of REAL;
end;

definition
  cluster natural -> complex number;
end;