:: Complex Numbers - Basic Definitions :: by Library Committee :: :: Received March 7, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin definition func -> set equals :: XCMPLX_0:def 1 (0,1) --> (0,1); coherence (0,1) --> (0,1) is set ; let c be number ; attrc is complex means :Def2: :: XCMPLX_0:def 2 c in COMPLEX ; end; :: deftheorem defines XCMPLX_0:def_1_:_ = (0,1) --> (0,1); :: deftheorem Def2 defines complex XCMPLX_0:def_2_:_ for c being number holds ( c is complex iff c in COMPLEX ); registration cluster -> complex ; coherence is complex proofend; end; registration cluster complex for set ; existence ex b1 being number st b1 is complex proofend; end; registration complex number ex b1 being set st for b2 being complex number holds b2 in b1 proofend; end; notation let x be complex number ; synonym zero x for empty ; end; definition let x be complex number ; redefine attr x is empty means :: XCMPLX_0:def 3 x = 0 ; compatibility ( x is zero iff x = 0 ) ; end; :: deftheorem defines zero XCMPLX_0:def_3_:_ for x being complex number holds ( x is zero iff x = 0 ); definition let x, y be complex number ; x in COMPLEX by Def2; then consider x1, x2 being Element of REAL such that A1: x = [*x1,x2*] by ARYTM_0:9; y in COMPLEX by Def2; then consider y1, y2 being Element of REAL such that A2: y = [*y1,y2*] by ARYTM_0:9; funcx + y -> set means :Def4: :: 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))*] ); existence ex b1 being set ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) proofend; uniqueness for b1, b2 being set st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds b1 = b2 proofend; commutativity for b1 being set for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds ex x1, x2, y1, y2 being Element of REAL st ( y = [*x1,x2*] & x = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) ; funcx * y -> set means :Def5: :: 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))))*] ); existence ex b1 being set ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) proofend; uniqueness for b1, b2 being set st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds b1 = b2 proofend; commutativity for b1 being set for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds ex x1, x2, y1, y2 being Element of REAL st ( y = [*x1,x2*] & x = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) ; end; :: deftheorem Def4 defines + XCMPLX_0:def_4_:_ for x, y being complex number for b3 being set holds ( b3 = x + y iff ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b3 = [*(+ (x1,y1)),(+ (x2,y2))*] ) ); :: deftheorem Def5 defines * XCMPLX_0:def_5_:_ for x, y being complex number for b3 being set holds ( b3 = x * y iff ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b3 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) ); Lm1: 0 = [*0,0*] by ARYTM_0:def_5; reconsider j = 1 as Element of REAL ; Lm2: for x, y, z being Element of REAL st + (x,y) = 0 & + (x,z) = 0 holds y = z proofend; registration let z, z9 be complex number ; clusterz + z9 -> complex ; coherence z + z9 is complex proofend; clusterz * z9 -> complex ; coherence z * z9 is complex proofend; end; definition let z be complex number ; z in COMPLEX by Def2; then consider x, y being Element of REAL such that A1: z = [*x,y*] by ARYTM_0:9; func - z -> complex number means :Def6: :: XCMPLX_0:def 6 z + it = 0 ; existence ex b1 being complex number st z + b1 = 0 proofend; uniqueness for b1, b2 being complex number st z + b1 = 0 & z + b2 = 0 holds b1 = b2 proofend; involutiveness for b1, b2 being complex number st b2 + b1 = 0 holds b1 + b2 = 0 ; funcz " -> complex number means :Def7: :: XCMPLX_0:def 7 z * it = 1 if z <> 0 otherwise it = 0 ; existence ( ( z <> 0 implies ex b1 being complex number st z * b1 = 1 ) & ( not z <> 0 implies ex b1 being complex number st b1 = 0 ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( z <> 0 & z * b1 = 1 & z * b2 = 1 implies b1 = b2 ) & ( not z <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; consistency for b1 being complex number holds verum ; involutiveness for b1, b2 being complex number st ( b2 <> 0 implies b2 * b1 = 1 ) & ( not b2 <> 0 implies b1 = 0 ) holds ( ( b1 <> 0 implies b1 * b2 = 1 ) & ( not b1 <> 0 implies b2 = 0 ) ) proofend; end; :: deftheorem Def6 defines - XCMPLX_0:def_6_:_ for z, b2 being complex number holds ( b2 = - z iff z + b2 = 0 ); :: deftheorem Def7 defines " XCMPLX_0:def_7_:_ for z, b2 being complex number holds ( ( z <> 0 implies ( b2 = z " iff z * b2 = 1 ) ) & ( not z <> 0 implies ( b2 = z " iff b2 = 0 ) ) ); definition let x, y be complex number ; funcx - y -> set equals :: XCMPLX_0:def 8 x + (- y); coherence x + (- y) is set ; funcx / y -> set equals :: XCMPLX_0:def 9 x * (y "); coherence x * (y ") is set ; end; :: deftheorem defines - XCMPLX_0:def_8_:_ for x, y being complex number holds x - y = x + (- y); :: deftheorem defines / XCMPLX_0:def_9_:_ for x, y being complex number holds x / y = x * (y "); registration let x, y be complex number ; clusterx - y -> complex ; coherence x - y is complex ; clusterx / y -> complex ; coherence x / y is complex ; end; Lm3: for x, y, z being complex number holds x * (y * z) = (x * y) * z proofend; registration cluster non zero complex for set ; existence not for b1 being complex number holds b1 is zero proofend; end; Lm4: REAL c= COMPLEX by NUMBERS:def_2, XBOOLE_1:7; registration let x be non zero complex number ; cluster - x -> non zero complex ; coherence not - x is zero proofend; clusterx " -> non zero complex ; coherence not x " is zero proofend; let y be non zero complex number ; clusterx * y -> non zero ; coherence not x * y is zero proofend; end; registration let x, y be non zero complex number ; clusterx / y -> non zero ; coherence not x / y is zero ; end; registration cluster -> complex for Element of REAL ; coherence for b1 being Element of REAL holds b1 is complex proofend; end; registration cluster natural -> complex for set ; coherence for b1 being number st b1 is natural holds b1 is complex proofend; end; registration cluster -> complex for Element of COMPLEX ; coherence for b1 being Element of COMPLEX holds b1 is complex by Def2; end;