:: XCMPLX_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: one = succ 0 by ORDINAL2:def 4
.= 1 ;

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 b1 being number st b1 is complex
proof end;
end;

notation
let x be complex number ;
synonym zero x for empty x;
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 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))*] ) );

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

reconsider j = one as Element of REAL by ARYTM_0:1, ARYTM_2:21;

Lm3: for x, y, z being Element of REAL st + x,y = 0 & + x,z = 0 holds
y = z
proof end;

registration
let z, z' be complex number ;
cluster z + z' -> complex ;
coherence
z + z' is complex
proof end;
cluster z * z' -> complex ;
coherence
z * z' 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 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;

Lm4: 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 b1 being complex number holds b1 is zero
proof end;
end;

Lm5: 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 complex ;
coherence
not x * y is zero
proof end;
end;

registration
let x, y be non zero complex number ;
cluster x / y -> non zero complex ;
coherence
not x / y is zero ;
end;

registration
cluster -> complex Element of REAL ;
coherence
for b1 being Element of REAL holds b1 is complex
proof end;
end;

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