:: by Library Committee

::

:: Received March 7, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

:: deftheorem Def2 defines complex XCMPLX_0:def 2 :

for c being number holds

( c is complex iff c in COMPLEX );

for c being number holds

( c is complex iff c in COMPLEX );

registration
end;

registration
end;

:: deftheorem defines zero XCMPLX_0:def 3 :

for x being complex number holds

( x is zero iff x = 0 );

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;

ex b_{1} being set ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] )

for b_{1}, b_{2} being set st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{2} = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds

b_{1} = b_{2}

for b_{1} 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*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] )
;

ex b_{1} being set ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )

for b_{1}, b_{2} being set st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ ((* (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*] & b_{2} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds

b_{1} = b_{2}

for b_{1} 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*] & b_{1} = [*(+ ((* (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*] & b_{1} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )
;

end;
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;

func x + 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 x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & it = [*(+ (x1,y1)),(+ (x2,y2))*] );

ex b

( x = [*x1,x2*] & y = [*y1,y2*] & b

proof end;

uniqueness for b

( x = [*x1,x2*] & y = [*y1,y2*] & b

( x = [*x1,x2*] & y = [*y1,y2*] & b

b

proof end;

commutativity for b

for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b

func x * 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 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))))*] );

ex b

( x = [*x1,x2*] & y = [*y1,y2*] & b

proof end;

uniqueness for b

( x = [*x1,x2*] & y = [*y1,y2*] & b

( x = [*x1,x2*] & y = [*y1,y2*] & b

b

proof end;

commutativity for b

for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b

:: deftheorem Def4 defines + XCMPLX_0:def 4 :

for x, y being complex number

for b_{3} being set holds

( b_{3} = x + y iff ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{3} = [*(+ (x1,y1)),(+ (x2,y2))*] ) );

for x, y being complex number

for b

( b

( x = [*x1,x2*] & y = [*y1,y2*] & b

:: deftheorem Def5 defines * XCMPLX_0:def 5 :

for x, y being complex number

for b_{3} being set holds

( b_{3} = x * y iff ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{3} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) );

for x, y being complex number

for b

( b

( x = [*x1,x2*] & y = [*y1,y2*] & b

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

proof end;

registration

let z, z9 be complex number ;

coherence

z + z9 is complex

z * z9 is complex

end;
coherence

z + z9 is complex

proof end;

coherence z * z9 is complex

proof 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;

existence

ex b_{1} being complex number st z + b_{1} = 0

for b_{1}, b_{2} being complex number st z + b_{1} = 0 & z + b_{2} = 0 holds

b_{1} = b_{2}

for b_{1}, b_{2} being complex number st b_{2} + b_{1} = 0 holds

b_{1} + b_{2} = 0
;

existence

( ( z <> 0 implies ex b_{1} being complex number st z * b_{1} = 1 ) & ( not z <> 0 implies ex b_{1} being complex number st b_{1} = 0 ) )

for b_{1}, b_{2} being complex number holds

( ( z <> 0 & z * b_{1} = 1 & z * b_{2} = 1 implies b_{1} = b_{2} ) & ( not z <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being complex number holds verum
;

involutiveness

for b_{1}, b_{2} being complex number st ( b_{2} <> 0 implies b_{2} * b_{1} = 1 ) & ( not b_{2} <> 0 implies b_{1} = 0 ) holds

( ( b_{1} <> 0 implies b_{1} * b_{2} = 1 ) & ( not b_{1} <> 0 implies b_{2} = 0 ) )

end;
z in COMPLEX by Def2;

then consider x, y being Element of REAL such that

A1: z = [*x,y*] by ARYTM_0:9;

existence

ex b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

b

existence

( ( z <> 0 implies ex b

proof end;

uniqueness for b

( ( z <> 0 & z * b

proof end;

consistency for b

involutiveness

for b

( ( b

proof end;

:: deftheorem Def6 defines - XCMPLX_0:def 6 :

for z, b_{2} being complex number holds

( b_{2} = - z iff z + b_{2} = 0 );

for z, b

( b

:: deftheorem Def7 defines " XCMPLX_0:def 7 :

for z, b_{2} being complex number holds

( ( z <> 0 implies ( b_{2} = z " iff z * b_{2} = 1 ) ) & ( not z <> 0 implies ( b_{2} = z " iff b_{2} = 0 ) ) );

for z, b

( ( z <> 0 implies ( b

definition
end;

registration
end;

Lm3: for x, y, z being complex number holds x * (y * z) = (x * y) * z

proof end;

Lm4: REAL c= COMPLEX

by NUMBERS:def 2, XBOOLE_1:7;

registration

let x be non zero complex number ;

coherence

not - x is zero

not x " is zero

coherence

not x * y is zero

end;
coherence

not - x is zero

proof end;

coherence not x " is zero

proof end;

let y be non zero complex number ;coherence

not x * y is zero

proof end;

registration
end;

registration
end;