:: Complex Numbers - Basic Definitions
:: by Library Committee
::
:: Received March 7, 2003
:: Copyright (c) 2003-2011 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

cluster <i> -> complex ;
coherence
<i> is complex

proof end;

end;

registration

cluster complex set ;
existence
ex b₁ being number st b₁ is complex

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:11;
y in COMPLEX by Def2;
then consider y1, y2 being Element of REAL such that
A2: y = [*y1,y2*] by ARYTM_0:11;
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 b₁ being set ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₁ = [*(+ (x1,y1)),(+ (x2,y2))*] )

proof end;

uniqueness
for b₁, b₂ being set st ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₁ = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₂ = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds
b₁ = b₂

proof end;

commutativity
for b₁ 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₁ = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds
ex x1, x2, y1, y2 being Element of REAL st
( y = [*x1,x2*] & x = [*y1,y2*] & b₁ = [*(+ (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 b₁ being set ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₁ = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )

proof end;

uniqueness
for b₁, b₂ being set st ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₁ = [*(+ ((* (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₂ = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds
b₁ = b₂

proof end;

commutativity
for b₁ 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₁ = [*(+ ((* (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₁ = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) ;

end;

:: deftheorem Def4 defines + XCMPLX_0:def 4 :
for x, y being complex number
for b₃ being set holds
( b₃ = x + y iff ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₃ = [*(+ (x1,y1)),(+ (x2,y2))*] ) );

:: deftheorem Def5 defines * XCMPLX_0:def 5 :
for x, y being complex number
for b₃ being set holds
( b₃ = x * y iff ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₃ = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) );

Lm1: 0 = [*0,0*]
by ARYTM_0:def 7;

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:11;
func - z -> complex number means :Def6: :: XCMPLX_0:def 6
z + it = 0 ;
existence
ex b₁ being complex number st z + b₁ = 0

proof end;

uniqueness
for b₁, b₂ being complex number st z + b₁ = 0 & z + b₂ = 0 holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being complex number st b₂ + b₁ = 0 holds
b₁ + b₂ = 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 b₁ being complex number st z * b₁ = 1 ) & ( not z <> 0 implies ex b₁ being complex number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being complex number holds
( ( z <> 0 & z * b₁ = 1 & z * b₂ = 1 implies b₁ = b₂ ) & ( not z <> 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being complex number holds verum ;
involutiveness
for b₁, b₂ being complex number st ( b₂ <> 0 implies b₂ * b₁ = 1 ) & ( not b₂ <> 0 implies b₁ = 0 ) holds
( ( b₁ <> 0 implies b₁ * b₂ = 1 ) & ( not b₁ <> 0 implies b₂ = 0 ) )

proof end;

end;

:: deftheorem Def6 defines - XCMPLX_0:def 6 :
for z, b₂ being complex number holds
( b₂ = - z iff z + b₂ = 0 );

:: deftheorem Def7 defines " XCMPLX_0:def 7 :
for z, b₂ being complex number holds
( ( z <> 0 implies ( b₂ = z " iff z * b₂ = 1 ) ) & ( not z <> 0 implies ( b₂ = z " iff b₂ = 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 set ;
existence
not for b₁ being complex number holds b₁ is zero

proof end;

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

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 Element of REAL ;
coherence
for b₁ being Element of REAL holds b₁ is complex

proof end;

end;

registration

cluster natural -> complex set ;
coherence
for b₁ being number st b₁ is natural holds
b₁ is complex

proof end;

end;

registration

cluster -> complex Element of COMPLEX ;
coherence
for b₁ being Element of COMPLEX holds b₁ is complex by Def2;

end;