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


definition
func <i> -> set equals :: XCMPLX_0:def 1
(0,1) --> (0,1);
coherence
(0,1) --> (0,1) is set
;
let c be object ;
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 object 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 b1 being object st b1 is complex
proof end;
cluster complex for set ;
existence
ex b1 being number st b1 is complex
proof end;
end;

definition
mode Complex is complex Number ;
end;

registration
Complex ex b1 being set st
for b2 being Complex holds b2 in b1
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 -> set 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 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 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 :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 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 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 Def3 defines + XCMPLX_0:def 3 :
for x, y being Complex
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 Def4 defines * XCMPLX_0:def 4 :
for x, y being Complex
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))))*] ) );

0 in NAT
;

then reconsider zz = 0 as Element of REAL by NUMBERS:19;

Lm3: 0 = [*zz,zz*]
by ARYTM_0:def 5;

reconsider j = 1 as Element of REAL by Lm2;

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 b1 being Complex st z + b1 = 0
proof end;
uniqueness
for b1, b2 being Complex st z + b1 = 0 & z + b2 = 0 holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Complex st b2 + b1 = 0 holds
b1 + b2 = 0
;
func z " -> Complex means :Def6: :: XCMPLX_0:def 6
z * it = 1 if z <> 0
otherwise it = 0 ;
existence
( ( z <> 0 implies ex b1 being Complex st z * b1 = 1 ) & ( not z <> 0 implies ex b1 being Complex st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Complex 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 holds verum
;
involutiveness
for b1, b2 being Complex 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 Def5 defines - XCMPLX_0:def 5 :
for z, b2 being Complex holds
( b2 = - z iff z + b2 = 0 );

:: deftheorem Def6 defines " XCMPLX_0:def 6 :
for z, b2 being Complex 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;
func x - y -> set equals :: XCMPLX_0:def 7
x + (- y);
coherence
x + (- y) is set
;
func x / y -> set equals :: XCMPLX_0:def 8
x * (y ");
coherence
x * (y ") is set
;
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 b1 being object st b1 is natural holds
b1 is complex
by NUMBERS:20;
end;

Lm: 1 is Complex
;

registration
cluster zero complex for object ;
existence
ex b1 being Complex st b1 is zero
proof end;
cluster non zero complex for object ;
existence
not for b1 being Complex holds b1 is zero
by Lm;
cluster non zero complex for object ;
existence
not for b1 being Complex holds b1 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 b1 being Element of REAL 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
;
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;