:: Complex Numbers - Basic Definitions :: by Library Committee :: :: Received March 7, 2003 :: Copyright (c) 2003-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 CARD_1, FUNCOP_1, ORDINAL1, NUMBERS, SUBSET_1, FUNCT_2, FUNCT_1, XBOOLE_0, ARYTM_0, ARYTM_3, RELAT_1, ARYTM_2, ZFMISC_1, ARYTM_1, TARSKI, XCMPLX_0, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0; constructors FUNCT_4, ARYTM_1, ARYTM_0, FUNCOP_1, RELSET_1, NUMBERS; registrations FUNCT_1, FUNCT_2, NUMBERS, XBOOLE_0, FUNCT_4, ORDINAL1, ARYTM_0; requirements BOOLE, SUBSET, NUMERALS; begin definition func -> Number 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; registration cluster -> complex; end; registration cluster complex for Number; cluster complex for number; end; definition mode Complex is complex Number; end; registration sethood of Complex; end; ::$CD definition let x,y be Complex; func x+y -> number 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 -> number 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; registration let z,z9 be Complex; cluster z+z9 -> complex; cluster z*z9 -> complex; end; definition let z be Complex; func -z -> Complex means :: XCMPLX_0:def 6 z + it = 0; involutiveness; func z" -> Complex means :: XCMPLX_0:def 7 z*it = 1 if z <> 0 otherwise it = 0; involutiveness; end; definition let x,y be Complex; func x-y -> number equals :: XCMPLX_0:def 8 x+(-y); func x/y -> number equals :: XCMPLX_0:def 9 x * y"; end; registration let x,y be Complex; cluster x-y -> complex; cluster x/y -> complex; end; registration cluster natural -> complex for object; end; registration cluster zero for Complex; cluster non zero for Complex; cluster non zero for Complex; end; registration let x be non zero Complex; cluster -x -> non zero; cluster x" -> non zero; let y be non zero Complex; cluster x*y -> non zero; end; registration let x,y be non zero Complex; cluster x/y -> non zero; end; registration cluster -> complex for Element of REAL; end; registration cluster -> complex for Element of COMPLEX; end; :: 26.05.2012, A.T. registration let i be Complex; reduce In(i,COMPLEX) to i; end;