:: Complex Numbers - Basic Definitions
:: by Library Committee
::
:: Received March 7, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition

func <i> -> Number equals :: XCMPLX_0:def 1
(0,1) --> (0,1);

coherence
(0,1) --> (0,1) is Number ;
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 );

0 in NAT
;

then 0 in REAL
by NUMBERS:19;

then Lm1: In (0,REAL) = 0
by SUBSET_1:def 8;

1 in NAT
;

then Lm2: 1 in REAL
by NUMBERS:19;

registration

cluster <i> -> complex ;

coherence
<i> is complex

proof end;

end;

registration

cluster complex for object ;

existence
ex b₁ being Number st b₁ is complex

proof end;

cluster complex for set ;

existence
ex b₁ being number st b₁ is complex

proof end;

end;

definition

mode Complex is complex Number ;

end;

registration

Complex ex b₁ being set st
for b₂ being Complex holds b₂ in b₁

proof end;

end;

canceled;

::$CD

definition

let x, y be Complex;
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 -> number means :Def3: :: XCMPLX_0:def 3
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 number 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 number 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 number
for x, y being Complex 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 -> number 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)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] );

existence
ex b₁ being number 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 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))))*] ) & 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 number
for x, y being Complex 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 Def3 defines + XCMPLX_0:def 3 :
for x, y being Complex
for b₃ being number 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 Def4 defines * XCMPLX_0:def 4 :
for x, y being Complex
for b₃ being number 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))))*] ) );

Lm4: 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;

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;
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 means :Def5: :: XCMPLX_0:def 5
z + it = 0 ;

existence
ex b₁ being Complex st z + b₁ = 0

proof end;

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

proof end;

involutiveness
for b₁, b₂ being Complex st b₂ + b₁ = 0 holds
b₁ + b₂ = 0 ;

func z " -> Complex means :Def6: :: XCMPLX_0:def 6
z * it = 1 if z <> 0
otherwise it = 0 ;

existence
( ( z <> 0 implies ex b₁ being Complex st z * b₁ = 1 ) & ( not z <> 0 implies ex b₁ being Complex st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Complex 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 holds verum ;
involutiveness
for b₁, b₂ being Complex 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 Def5 defines - XCMPLX_0:def 5 :
for z, b₂ being Complex holds
( b₂ = - z iff z + b₂ = 0 );

:: deftheorem Def6 defines " XCMPLX_0:def 6 :
for z, b₂ being Complex 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;

func x - y -> number equals :: XCMPLX_0:def 7
x + (- y);

coherence
x + (- y) is number ;

func x / y -> number equals :: XCMPLX_0:def 8
x * (y ");

coherence
x * (y ") is number ;

end;

:: deftheorem defines - XCMPLX_0:def 7 :
for x, y being Complex holds x - y = x + (- y);

:: deftheorem defines / XCMPLX_0:def 8 :
for x, y being Complex holds x / y = x * (y ");

registration

let x, y be Complex;

cluster x - y -> complex ;

coherence
x - y is complex ;

cluster x / y -> complex ;

coherence
x / y is complex ;

end;

Lm5: for x, y, z being Complex holds x * (y * z) = (x * y) * z

proof end;

registration

cluster natural -> complex for object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is complex by NUMBERS:20;

end;

Lm: 1 is Complex
;

registration

cluster zero complex for object ;

existence
ex b₁ being Complex st b₁ is zero

proof end;

cluster non zero complex for object ;

existence
not for b₁ being Complex holds b₁ is zero by Lm;

cluster non zero complex for object ;

existence
not for b₁ being Complex holds b₁ is zero by Lm;

end;

Lm6: REAL c= COMPLEX
by NUMBERS:def 2, XBOOLE_1:7;

registration

let x be non zero Complex;

cluster - x -> non zero ;

coherence
not - x is zero

proof end;

cluster x " -> non zero ;

coherence
not x " is zero

proof end;

let y be non zero Complex;

cluster x * y -> non zero ;

coherence
not x * y is zero

proof end;

end;

registration

let x, y be non zero Complex;

cluster x / y -> non zero ;

coherence
not x / y is zero ;

end;

registration

cluster -> complex for Element of REAL ;

coherence
for b₁ being Element of REAL holds b₁ is complex

proof end;

end;

registration

cluster -> complex for Element of COMPLEX ;

coherence
for b₁ being Element of COMPLEX holds b₁ is complex ;

end;

:: 26.05.2012, A.T.

registration

let i be Complex;

reduce In (i,COMPLEX) to i;

reducibility
In (i,COMPLEX) = i by Def2, SUBSET_1:def 8;

end;