:: XCMPLX_0 semantic presentation

E1: 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 c1 be number ;
attr a1 is complex means :Def2: :: XCMPLX_0:def 2
a1 in COMPLEX ;
end;

:: deftheorem Def1 defines <i> XCMPLX_0:def 1 :
<i> = 0,1 --> 0,1;

:: deftheorem Def2 defines complex XCMPLX_0:def 2 :
for b1 being number holds
( b1 is complex iff b1 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 c1 be complex number ;
synonym zero c1 for empty c1;
end;

definition
let c1 be complex number ;
redefine attr a1 is empty means :: XCMPLX_0:def 3
a1 = 0;
compatibility
( c1 is zero iff c1 = 0 ) ;
end;

:: deftheorem Def3 defines zero XCMPLX_0:def 3 :
for b1 being complex number holds
( b1 is zero iff b1 = 0 );

definition
let c1, c2 be complex number ;
c1 in COMPLEX by Def2;
then consider c3, c4 being Element of REAL such that
E3: c1 = [*c3,c4*] by ARYTM_0:11;
c2 in COMPLEX by Def2;
then consider c5, c6 being Element of REAL such that
E4: c2 = [*c5,c6*] by ARYTM_0:11;
func c1 + c2 -> set means :Def4: :: XCMPLX_0:def 4
ex b1, b2, b3, b4 being Element of REAL st
( a1 = [*b1,b2*] & a2 = [*b3,b4*] & a3 = [*(+ b1,b3),(+ b2,b4)*] );
existence
ex b1 being set ex b2, b3, b4, b5 being Element of REAL st
( c1 = [*b2,b3*] & c2 = [*b4,b5*] & b1 = [*(+ b2,b4),(+ b3,b5)*] )
proof end;
uniqueness
for b1, b2 being set st ex b3, b4, b5, b6 being Element of REAL st
( c1 = [*b3,b4*] & c2 = [*b5,b6*] & b1 = [*(+ b3,b5),(+ b4,b6)*] ) & ex b3, b4, b5, b6 being Element of REAL st
( c1 = [*b3,b4*] & c2 = [*b5,b6*] & b2 = [*(+ b3,b5),(+ b4,b6)*] ) holds
b1 = b2
proof end;
commutativity
for b1 being set
for b2, b3 being complex number st ex b4, b5, b6, b7 being Element of REAL st
( b2 = [*b4,b5*] & b3 = [*b6,b7*] & b1 = [*(+ b4,b6),(+ b5,b7)*] ) holds
ex b4, b5, b6, b7 being Element of REAL st
( b3 = [*b4,b5*] & b2 = [*b6,b7*] & b1 = [*(+ b4,b6),(+ b5,b7)*] ) ;
func c1 * c2 -> set means :Def5: :: XCMPLX_0:def 5
ex b1, b2, b3, b4 being Element of REAL st
( a1 = [*b1,b2*] & a2 = [*b3,b4*] & a3 = [*(+ (* b1,b3),(opp (* b2,b4))),(+ (* b1,b4),(* b2,b3))*] );
existence
ex b1 being set ex b2, b3, b4, b5 being Element of REAL st
( c1 = [*b2,b3*] & c2 = [*b4,b5*] & b1 = [*(+ (* b2,b4),(opp (* b3,b5))),(+ (* b2,b5),(* b3,b4))*] )
proof end;
uniqueness
for b1, b2 being set st ex b3, b4, b5, b6 being Element of REAL st
( c1 = [*b3,b4*] & c2 = [*b5,b6*] & b1 = [*(+ (* b3,b5),(opp (* b4,b6))),(+ (* b3,b6),(* b4,b5))*] ) & ex b3, b4, b5, b6 being Element of REAL st
( c1 = [*b3,b4*] & c2 = [*b5,b6*] & b2 = [*(+ (* b3,b5),(opp (* b4,b6))),(+ (* b3,b6),(* b4,b5))*] ) holds
b1 = b2
proof end;
commutativity
for b1 being set
for b2, b3 being complex number st ex b4, b5, b6, b7 being Element of REAL st
( b2 = [*b4,b5*] & b3 = [*b6,b7*] & b1 = [*(+ (* b4,b6),(opp (* b5,b7))),(+ (* b4,b7),(* b5,b6))*] ) holds
ex b4, b5, b6, b7 being Element of REAL st
( b3 = [*b4,b5*] & b2 = [*b6,b7*] & b1 = [*(+ (* b4,b6),(opp (* b5,b7))),(+ (* b4,b7),(* b5,b6))*] ) ;
end;

:: deftheorem Def4 defines + XCMPLX_0:def 4 :
for b1, b2 being complex number
for b3 being set holds
( b3 = b1 + b2 iff ex b4, b5, b6, b7 being Element of REAL st
( b1 = [*b4,b5*] & b2 = [*b6,b7*] & b3 = [*(+ b4,b6),(+ b5,b7)*] ) );

:: deftheorem Def5 defines * XCMPLX_0:def 5 :
for b1, b2 being complex number
for b3 being set holds
( b3 = b1 * b2 iff ex b4, b5, b6, b7 being Element of REAL st
( b1 = [*b4,b5*] & b2 = [*b6,b7*] & b3 = [*(+ (* b4,b6),(opp (* b5,b7))),(+ (* b4,b7),(* b5,b6))*] ) );

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

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

Lemma6: for b1, b2, b3 being Element of REAL st + b1,b2 = 0 & + b1,b3 = 0 holds
b2 = b3
proof end;

registration
let c2, c3 be complex number ;
cluster a1 + a2 -> complex ;
coherence
c2 + c3 is complex
proof end;
cluster a1 * a2 -> complex ;
coherence
c2 * c3 is complex
proof end;
end;

definition
let c2 be complex number ;
c2 in COMPLEX by Def2;
then consider c3, c4 being Element of REAL such that
E7: c2 = [*c3,c4*] by ARYTM_0:11;
func - c1 -> complex number means :Def6: :: XCMPLX_0:def 6
a1 + a2 = 0;
existence
ex b1 being complex number st c2 + b1 = 0
proof end;
uniqueness
for b1, b2 being complex number st c2 + b1 = 0 & c2 + b2 = 0 holds
b1 = b2
proof end;
involutiveness
for b1, b2 being complex number st b2 + b1 = 0 holds
b1 + b2 = 0 ;
func c1 " -> complex number means :Def7: :: XCMPLX_0:def 7
a1 * a2 = 1 if a1 <> 0
otherwise a2 = 0;
existence
( ( c2 <> 0 implies ex b1 being complex number st c2 * b1 = 1 ) & ( not c2 <> 0 implies ex b1 being complex number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being complex number holds
( ( c2 <> 0 & c2 * b1 = 1 & c2 * b2 = 1 implies b1 = b2 ) & ( not c2 <> 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 b1, b2 being complex number holds
( b2 = - b1 iff b1 + b2 = 0 );

:: deftheorem Def7 defines " XCMPLX_0:def 7 :
for b1, b2 being complex number holds
( ( b1 <> 0 implies ( b2 = b1 " iff b1 * b2 = 1 ) ) & ( not b1 <> 0 implies ( b2 = b1 " iff b2 = 0 ) ) );

definition
let c2, c3 be complex number ;
func c1 - c2 -> set equals :: XCMPLX_0:def 8
a1 + (- a2);
coherence
c2 + (- c3) is set ;
func c1 / c2 -> set equals :: XCMPLX_0:def 9
a1 * (a2 " );
coherence
c2 * (c3 " ) is set ;
end;

:: deftheorem Def8 defines - XCMPLX_0:def 8 :
for b1, b2 being complex number holds b1 - b2 = b1 + (- b2);

:: deftheorem Def9 defines / XCMPLX_0:def 9 :
for b1, b2 being complex number holds b1 / b2 = b1 * (b2 " );

registration
let c2, c3 be complex number ;
cluster a1 - a2 -> complex ;
coherence
c2 - c3 is complex ;
cluster a1 / a2 -> complex ;
coherence
c2 / c3 is complex ;
end;

Lemma9: for b1, b2, b3 being complex number holds b1 * (b2 * b3) = (b1 * b2) * b3
proof end;

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

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

registration
let c2 be non zero complex number ;
cluster - a1 -> non zero complex ;
coherence
not - c2 is zero
proof end;
cluster a1 " -> non zero complex ;
coherence
not c2 " is zero
proof end;
let c3 be non zero complex number ;
cluster a1 * a2 -> non zero complex ;
coherence
not c2 * c3 is zero
proof end;
end;

registration
let c2, c3 be non zero complex number ;
cluster a1 / a2 -> non zero complex ;
coherence
not c2 / c3 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;