:: Complex Numbers - Basic Definitions
:: by Library Committee
::
:: Copyright (c) 2003-2012 Association of Mizar Users

begin

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

:: deftheorem defines <i> XCMPLX_0:def 1 :
<i> = (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
coherence
proof end;
end;

registration
existence
ex b1 being number st b1 is complex
proof end;
end;

registration
complex number ex b1 being set st
for b2 being complex number holds b2 in b1
proof end;
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;
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 b1 being set ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] )
proof end;
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
proof end;
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))*] )
;
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 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))))*] )
proof end;
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
proof end;
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:
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 ;
cluster z + z9 -> complex ;
coherence
z + z9 is complex
proof end;
cluster z * z9 -> complex ;
coherence
z * z9 is complex
proof end;
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
proof end;
uniqueness
for b1, b2 being complex number st z + b1 = 0 & z + b2 = 0 holds
b1 = b2
proof end;
involutiveness
for b1, b2 being complex number st b2 + b1 = 0 holds
b1 + b2 = 0
;
func z " -> 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 ) )
proof end;
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 ) )
proof end;
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 ) )
proof end;
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 ;
func x - y -> set equals :: XCMPLX_0:def 8
x + (- y);
coherence
x + (- y) is set
;
func x / 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 ;
cluster x - y -> complex ;
coherence
x - y is complex
;
cluster x / y -> complex ;
coherence
x / y is complex
;
end;

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

registration
cluster non zero complex for set ;
existence
not for b1 being complex number holds b1 is zero
proof end;
end;

Lm4:
by ;

registration
let x be non zero complex number ;
cluster - x -> non zero complex ;
coherence
not - x is zero
proof end;
cluster x " -> non zero complex ;
coherence
not x " is zero
proof end;
let y be non zero complex number ;
cluster x * y -> non zero ;
coherence
not x * y is zero
proof end;
end;

registration
let x, y be non zero complex number ;
cluster x / 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
proof end;
end;

registration
cluster natural -> complex for set ;
coherence
for b1 being number st b1 is natural holds
b1 is complex
proof end;
end;

registration
cluster -> complex for Element of COMPLEX ;
coherence
for b1 being Element of COMPLEX holds b1 is complex
by Def2;
end;