Journal of Formalized Mathematics
EMM, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Complex Numbers --- Basic Definitions

by
Library Committee

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;

```