:: XCMPLX_0 semantic presentation
begin
definition
func * -> set equals :: XCMPLX_0:def 1
(0,1) --> (0,1);
coherence
(0,1) --> (0,1) is set ;
let c be number ;
attrc is complex means :Def2: :: XCMPLX_0:def 2
c in COMPLEX ;
end;
:: deftheorem defines ** XCMPLX_0:def_1_:_
** = (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 ** -> complex ;
coherence
** is complex
proof
set X = { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ;
A1: now__::_thesis:_not_**_in__{__x_where_x_is_Element_of_Funcs_({0,1},REAL)_:_x_._1_=_0__}_
assume ** in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ; ::_thesis: contradiction
then ex x being Element of Funcs ({0,1},REAL) st
( ** = x & x . 1 = 0 ) ;
hence contradiction by FUNCT_4:63; ::_thesis: verum
end;
** in Funcs ({0,1},REAL) by FUNCT_2:8;
then ** in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, XBOOLE_0:def_5;
hence ** in COMPLEX by NUMBERS:def_2, XBOOLE_0:def_3; :: according to XCMPLX_0:def_2 ::_thesis: verum
end;
end;
registration
cluster complex for set ;
existence
ex b1 being number st b1 is complex
proof
take ** ; ::_thesis: ** is complex
thus ** is complex ; ::_thesis: verum
end;
end;
registration
complex number ex b1 being set st
for b2 being complex number holds b2 in b1
proof
take COMPLEX ; ::_thesis: for b1 being complex number holds b1 in COMPLEX
thus for b1 being complex number holds b1 in COMPLEX by Def2; ::_thesis: verum
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:9;
y in COMPLEX by Def2;
then consider y1, y2 being Element of REAL such that
A2: y = [*y1,y2*] by ARYTM_0:9;
funcx + 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
take [*(+ (x1,y1)),(+ (x2,y2))*] ; ::_thesis: ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ (x1,y1)),(+ (x2,y2))*] = [*(+ (x1,y1)),(+ (x2,y2))*] )
thus ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ (x1,y1)),(+ (x2,y2))*] = [*(+ (x1,y1)),(+ (x2,y2))*] ) by A1, A2; ::_thesis: verum
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
let c1, c2 be number ; ::_thesis: ( ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) implies c1 = c2 )
given x1, x2, y1, y2 being Element of REAL such that A3: x = [*x1,x2*] and
A4: y = [*y1,y2*] and
A5: c1 = [*(+ (x1,y1)),(+ (x2,y2))*] ; ::_thesis: ( for x1, x2, y1, y2 being Element of REAL holds
( not x = [*x1,x2*] or not y = [*y1,y2*] or not c2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) or c1 = c2 )
given x19, x29, y19, y29 being Element of REAL such that A6: x = [*x19,x29*] and
A7: y = [*y19,y29*] and
A8: c2 = [*(+ (x19,y19)),(+ (x29,y29))*] ; ::_thesis: c1 = c2
A9: ( x1 = x19 & x2 = x29 ) by A3, A6, ARYTM_0:10;
y1 = y19 by A4, A7, ARYTM_0:10;
hence c1 = c2 by A4, A5, A7, A8, A9, ARYTM_0:10; ::_thesis: verum
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))*] ) ;
funcx * 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
take [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ; ::_thesis: ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )
thus ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) by A1, A2; ::_thesis: verum
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
let c1, c2 be number ; ::_thesis: ( ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & c1 = [*(+ ((* (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*] & c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) implies c1 = c2 )
given x1, x2, y1, y2 being Element of REAL such that A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: c1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ; ::_thesis: ( for x1, x2, y1, y2 being Element of REAL holds
( not x = [*x1,x2*] or not y = [*y1,y2*] or not c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) or c1 = c2 )
given x19, x29, y19, y29 being Element of REAL such that A13: x = [*x19,x29*] and
A14: y = [*y19,y29*] and
A15: c2 = [*(+ ((* (x19,y19)),(opp (* (x29,y29))))),(+ ((* (x19,y29)),(* (x29,y19))))*] ; ::_thesis: c1 = c2
A16: ( x1 = x19 & x2 = x29 ) by A10, A13, ARYTM_0:10;
( y1 = y19 & y2 = y29 ) by A11, A14, ARYTM_0:10;
hence c1 = c2 by A12, A15, A16; ::_thesis: verum
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))))*] ) );
Lm1: 0 = [*0,0*]
by ARYTM_0:def_5;
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
let x, y, z be Element of REAL ; ::_thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z )
assume that
A1: + (x,y) = 0 and
A2: + (x,z) = 0 ; ::_thesis: y = z
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & z in REAL+ & y in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ) ;
suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z
then ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A1, A2, ARYTM_0:def_1;
hence y = z by ARYTM_2:11; ::_thesis: verum
end;
supposethat A3: x in REAL+ and
A4: y in REAL+ and
A5: z in [:{0},REAL+:] ; ::_thesis: y = z
A6: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A1, A3, A4, ARYTM_0:def_1;
consider x99, y99 being Element of REAL+ such that
A7: x = x99 and
A8: ( z = [0,y99] & 0 = x99 - y99 ) by A2, A3, A5, ARYTM_0:def_1;
A9: x99 = 0 by A6, A7, ARYTM_2:5;
[{},{}] in {[{},{}]} by TARSKI:def_1;
then A10: not [{},{}] in REAL by NUMBERS:def_1, XBOOLE_0:def_5;
z in REAL ;
hence y = z by A8, A9, A10, ARYTM_1:19; ::_thesis: verum
end;
supposethat A11: x in REAL+ and
A12: z in REAL+ and
A13: y in [:{0},REAL+:] ; ::_thesis: y = z
A14: ex x9, z9 being Element of REAL+ st
( x = x9 & z = z9 & 0 = x9 + z9 ) by A2, A11, A12, ARYTM_0:def_1;
consider x99, y9 being Element of REAL+ such that
A15: x = x99 and
A16: ( y = [0,y9] & 0 = x99 - y9 ) by A1, A11, A13, ARYTM_0:def_1;
A17: x99 = 0 by A14, A15, ARYTM_2:5;
[0,0] in {[0,0]} by TARSKI:def_1;
then A18: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5;
y in REAL ;
hence y = z by A16, A17, A18, ARYTM_1:19; ::_thesis: verum
end;
supposethat A19: x in REAL+ and
A20: y in [:{0},REAL+:] and
A21: z in [:{0},REAL+:] ; ::_thesis: y = z
consider x9, y9 being Element of REAL+ such that
A22: x = x9 and
A23: y = [0,y9] and
A24: 0 = x9 - y9 by A1, A19, A20, ARYTM_0:def_1;
consider x99, z9 being Element of REAL+ such that
A25: x = x99 and
A26: z = [0,z9] and
A27: 0 = x99 - z9 by A2, A19, A21, ARYTM_0:def_1;
y9 = x9 by A24, ARYTM_0:6
.= z9 by A22, A25, A27, ARYTM_0:6 ;
hence y = z by A23, A26; ::_thesis: verum
end;
supposethat A28: z in REAL+ and
A29: y in REAL+ and
A30: x in [:{0},REAL+:] ; ::_thesis: y = z
consider x9, y9 being Element of REAL+ such that
A31: x = [0,x9] and
A32: y = y9 and
A33: 0 = y9 - x9 by A1, A29, A30, ARYTM_0:def_1;
consider x99, z9 being Element of REAL+ such that
A34: x = [0,x99] and
A35: z = z9 and
A36: 0 = z9 - x99 by A2, A28, A30, ARYTM_0:def_1;
x9 = x99 by A31, A34, XTUPLE_0:1;
then z9 = x9 by A36, ARYTM_0:6
.= y9 by A33, ARYTM_0:6 ;
hence y = z by A32, A35; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z
then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A1, ARYTM_0:def_1;
hence y = z ; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z
then ex x9, z9 being Element of REAL+ st
( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A2, ARYTM_0:def_1;
hence y = z ; ::_thesis: verum
end;
end;
end;
registration
let z, z9 be complex number ;
clusterz + z9 -> complex ;
coherence
z + z9 is complex
proof
ex x1, x2, y1, y2 being Element of REAL st
( z = [*x1,x2*] & z9 = [*y1,y2*] & z + z9 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by Def4;
hence z + z9 in COMPLEX ; :: according to XCMPLX_0:def_2 ::_thesis: verum
end;
clusterz * z9 -> complex ;
coherence
z * z9 is complex
proof
ex x1, x2, y1, y2 being Element of REAL st
( z = [*x1,x2*] & z9 = [*y1,y2*] & z * z9 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) by Def5;
hence z * z9 in COMPLEX ; :: according to XCMPLX_0:def_2 ::_thesis: verum
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:9;
func - z -> complex number means :Def6: :: XCMPLX_0:def 6
z + it = 0 ;
existence
ex b1 being complex number st z + b1 = 0
proof
reconsider z9 = [*(opp x),(opp y)*] as complex number by Def2;
take z9 ; ::_thesis: z + z9 = 0
( 0 = + (x,(opp x)) & 0 = + (y,(opp y)) ) by ARYTM_0:def_3;
hence z + z9 = 0 by A1, Def4, Lm1; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex number st z + b1 = 0 & z + b2 = 0 holds
b1 = b2
proof
let c1, c2 be complex number ; ::_thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A2: z + c1 = 0 and
A3: z + c2 = 0 ; ::_thesis: c1 = c2
consider x1, x2, y1, y2 being Element of REAL such that
A4: z = [*x1,x2*] and
A5: c1 = [*y1,y2*] and
A6: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by A2, Def4;
consider x19, x29, y19, y29 being Element of REAL such that
A7: z = [*x19,x29*] and
A8: c2 = [*y19,y29*] and
A9: 0 = [*(+ (x19,y19)),(+ (x29,y29))*] by A3, Def4;
A10: x1 = x19 by A4, A7, ARYTM_0:10;
A11: x2 = x29 by A4, A7, ARYTM_0:10;
A12: + (x1,y1) = 0 by A6, Lm1, ARYTM_0:10;
+ (x1,y19) = 0 by A9, A10, Lm1, ARYTM_0:10;
then A13: y1 = y19 by A12, Lm2;
A14: + (x2,y2) = 0 by A6, Lm1, ARYTM_0:10;
+ (x2,y29) = 0 by A9, A11, Lm1, ARYTM_0:10;
hence c1 = c2 by A5, A8, A13, A14, Lm2; ::_thesis: verum
end;
involutiveness
for b1, b2 being complex number st b2 + b1 = 0 holds
b1 + b2 = 0 ;
funcz " -> 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
thus ( z <> 0 implies ex z9 being complex number st z * z9 = 1 ) ::_thesis: ( not z <> 0 implies ex b1 being complex number st b1 = 0 )
proof
set y1 = * (x,(inv (+ ((* (x,x)),(* (y,y))))));
set y2 = * ((opp y),(inv (+ ((* (x,x)),(* (y,y))))));
set z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*];
reconsider z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] as complex number by Def2;
assume A15: z <> 0 ; ::_thesis: ex z9 being complex number st z * z9 = 1
take z9 ; ::_thesis: z * z9 = 1
A16: opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))) = opp (* (y,(opp (* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15
.= opp (opp (* (y,(* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15
.= * ((* (y,y)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13 ;
A17: * (x,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((* (x,x)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13;
A18: now__::_thesis:_not_+_((*_(x,x)),(*_(y,y)))_=_0
assume + ((* (x,x)),(* (y,y))) = 0 ; ::_thesis: contradiction
then ( x = 0 & y = 0 ) by ARYTM_0:17;
hence contradiction by A1, A15, ARYTM_0:def_5; ::_thesis: verum
end;
* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((opp y),(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) by ARYTM_0:13
.= opp (* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))) by ARYTM_0:15 ;
then + ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))) = 0 by ARYTM_0:def_3;
then [*(+ ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))))))),(+ ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))))*] = + ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))))) by ARYTM_0:def_5
.= * ((+ ((* (x,x)),(* (y,y)))),(inv (+ ((* (x,x)),(* (y,y)))))) by A16, A17, ARYTM_0:14
.= 1 by A18, ARYTM_0:def_4 ;
hence z * z9 = 1 by A1, Def5; ::_thesis: verum
end;
assume z = 0 ; ::_thesis: ex b1 being complex number st b1 = 0
hence ex b1 being complex number st b1 = 0 ; ::_thesis: verum
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
let c1, c2 be complex number ; ::_thesis: ( ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) & ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) )
thus ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) ::_thesis: ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )
proof
assume that
A19: z <> 0 and
A20: z * c1 = 1 and
A21: z * c2 = 1 ; ::_thesis: c1 = c2
A22: for z9 being complex number st z * z9 = 1 holds
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
proof
let z9 be complex number ; ::_thesis: ( z * z9 = 1 implies z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] )
assume A23: z * z9 = 1 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
consider x1, x2, x9, y9 being Element of REAL such that
A24: z = [*x1,x2*] and
A25: z9 = [*x9,y9*] and
A26: 1 = [*(+ ((* (x1,x9)),(opp (* (x2,y9))))),(+ ((* (x1,y9)),(* (x2,x9))))*] by A23, Def5;
A27: ( x = x1 & y = x2 ) by A1, A24, ARYTM_0:10;
percases ( ( x = 0 & y <> 0 ) or ( opp y = 0 & x <> 0 ) or ( opp y <> 0 & x <> 0 ) ) by A1, A19, ARYTM_0:def_5;
supposethat A28: x = 0 and
A29: y <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (y,(opp y)) = 0 by ARYTM_0:def_3;
then A30: opp y <> 0 by A29, ARYTM_0:11;
( * (x,y9) = 0 & * (x,x9) = 0 ) by A28, ARYTM_0:12;
then A31: 1 = [*(opp (* (y,y9))),(+ (0,(* (y,x9))))*] by A26, A27, ARYTM_0:11
.= [*(opp (* (y,y9))),(* (y,x9))*] by ARYTM_0:11 ;
A32: 1 = [*j,0*] by ARYTM_0:def_5;
* ((opp y),y9) = opp (* (y,y9)) by ARYTM_0:15
.= 1 by A31, A32, ARYTM_0:10 ;
then A33: y9 = inv (opp y) by A30, ARYTM_0:def_4;
A34: * (x,x) = 0 by A28, ARYTM_0:12;
* ((opp y),(opp (inv y))) = opp (* (y,(opp (inv y)))) by ARYTM_0:15
.= opp (opp (* (y,(inv y)))) by ARYTM_0:15
.= 1 by A29, ARYTM_0:def_4 ;
then A35: inv (opp y) = opp (inv y) by A30, ARYTM_0:def_4;
* (y,x9) = 0 by A31, A32, ARYTM_0:10;
hence z9 = [*0,(inv (opp y))*] by A25, A29, A33, ARYTM_0:21
.= [*0,(opp (* (j,(inv y))))*] by A35, ARYTM_0:19
.= [*0,(opp (* ((* (y,(inv y))),(inv y))))*] by A29, ARYTM_0:def_4
.= [*0,(opp (* (y,(* ((inv y),(inv y))))))*] by ARYTM_0:13
.= [*0,(* ((opp y),(* ((inv y),(inv y)))))*] by ARYTM_0:15
.= [*0,(* ((opp y),(inv (* (y,y)))))*] by ARYTM_0:22
.= [*0,(* ((opp y),(inv (+ (0,(* (y,y)))))))*] by ARYTM_0:11
.= [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A28, A34, ARYTM_0:12 ;
::_thesis: verum
end;
supposethat A36: opp y = 0 and
A37: x <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (y,(opp y)) = 0 by ARYTM_0:def_3;
then A38: y = 0 by A36, ARYTM_0:11;
then A39: * (y,x9) = 0 by ARYTM_0:12;
opp (* (y,y9)) = * ((opp y),y9) by ARYTM_0:15
.= 0 by A36, ARYTM_0:12 ;
then A40: 1 = [*(* (x,x9)),(+ ((* (x,y9)),0))*] by A26, A27, A39, ARYTM_0:11
.= [*(* (x,x9)),(* (x,y9))*] by ARYTM_0:11 ;
A41: 1 = [*j,0*] by ARYTM_0:def_5;
then * (x,x9) = 1 by A40, ARYTM_0:10;
then A42: x9 = inv x by A37, ARYTM_0:def_4;
* (x,y9) = 0 by A40, A41, ARYTM_0:10;
then A43: y9 = 0 by A37, ARYTM_0:21;
A44: * (y,y) = 0 by A38, ARYTM_0:12;
x9 = * (j,(inv x)) by A42, ARYTM_0:19
.= * ((* (x,(inv x))),(inv x)) by A37, ARYTM_0:def_4
.= * (x,(* ((inv x),(inv x)))) by ARYTM_0:13
.= * (x,(inv (* (x,x)))) by ARYTM_0:22
.= * (x,(inv (+ ((* (x,x)),0)))) by ARYTM_0:11 ;
hence z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A25, A36, A43, A44, ARYTM_0:12; ::_thesis: verum
end;
supposethat A45: opp y <> 0 and
A46: x <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
A47: now__::_thesis:_not_+_((*_((*_(x,x)),(inv_(opp_y)))),(opp_y))_=_0
assume + ((* ((* (x,x)),(inv (opp y)))),(opp y)) = 0 ; ::_thesis: contradiction
then + ((* ((* (x,x)),(inv (opp y)))),(* ((opp y),j))) = 0 by ARYTM_0:19;
then + ((* ((* (x,x)),(inv (opp y)))),(* ((opp y),(* ((opp y),(inv (opp y))))))) = 0 by A45, ARYTM_0:def_4;
then + ((* ((* (x,x)),(inv (opp y)))),(* ((* ((opp y),(opp y))),(inv (opp y))))) = 0 by ARYTM_0:13;
then A48: * ((inv (opp y)),(+ ((* (x,x)),(* ((opp y),(opp y)))))) = 0 by ARYTM_0:14;
+ ((* (x,x)),(* ((opp y),(opp y)))) <> 0 by A46, ARYTM_0:17;
then A49: inv (opp y) = 0 by A48, ARYTM_0:21;
* ((opp y),(inv (opp y))) = 1 by A45, ARYTM_0:def_4;
hence contradiction by A49, ARYTM_0:12; ::_thesis: verum
end;
reconsider j = 1 as Element of REAL ;
A50: 1 = [*j,0*] by ARYTM_0:def_5;
then + ((* (x1,y9)),(* (x2,x9))) = 0 by A26, ARYTM_0:10;
then * (x,y9) = opp (* (y,x9)) by A27, ARYTM_0:def_3;
then * (x,y9) = * ((opp y),x9) by ARYTM_0:15;
then A51: x9 = * ((* (x,y9)),(inv (opp y))) by A45, ARYTM_0:20
.= * (x,(* (y9,(inv (opp y))))) by ARYTM_0:13 ;
then + ((* (x,(* (x,(* (y9,(inv (opp y)))))))),(opp (* (y,y9)))) = 1 by A26, A27, A50, ARYTM_0:10;
then + ((* ((* (x,x)),(* (y9,(inv (opp y)))))),(opp (* (y,y9)))) = 1 by ARYTM_0:13;
then + ((* ((* (x,x)),(* (y9,(inv (opp y)))))),(* ((opp y),y9))) = 1 by ARYTM_0:15;
then + ((* (y9,(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),y9))) = 1 by ARYTM_0:13;
then * (y9,(+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))) = 1 by ARYTM_0:14;
then A52: y9 = inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))) by A47, ARYTM_0:def_4;
then A53: x9 = * (x,(inv (* ((+ ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp y))))) by A51, ARYTM_0:22
.= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(* ((opp y),(opp y))))))) by ARYTM_0:14
.= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (* (y,(opp y)))))))) by ARYTM_0:15
.= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (opp (* (y,y)))))))) by ARYTM_0:15
.= * (x,(inv (+ ((* ((* (x,x)),(* ((inv (opp y)),(opp y))))),(* (y,y)))))) by ARYTM_0:13
.= * (x,(inv (+ ((* ((* (x,x)),j)),(* (y,y)))))) by A45, ARYTM_0:def_4
.= * (x,(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:19 ;
y9 = * (j,(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))) by A52, ARYTM_0:19
.= * ((* ((opp y),(inv (opp y)))),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))) by A45, ARYTM_0:def_4
.= * ((opp y),(* ((inv (opp y)),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))))) by ARYTM_0:13
.= * ((opp y),(inv (* ((opp y),(+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))))) by ARYTM_0:22
.= * ((opp y),(inv (+ ((* ((opp y),(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),(opp y))))))) by ARYTM_0:14
.= * ((opp y),(inv (+ ((* ((* (x,x)),(* ((opp y),(inv (opp y)))))),(* ((opp y),(opp y))))))) by ARYTM_0:13
.= * ((opp y),(inv (+ ((* ((* (x,x)),j)),(* ((opp y),(opp y))))))) by A45, ARYTM_0:def_4
.= * ((opp y),(inv (+ ((* (x,x)),(* ((opp y),(opp y))))))) by ARYTM_0:19
.= * ((opp y),(inv (+ ((* (x,x)),(opp (* (y,(opp y)))))))) by ARYTM_0:15
.= * ((opp y),(inv (+ ((* (x,x)),(opp (opp (* (y,y)))))))) by ARYTM_0:15
.= * ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))) ;
hence z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A25, A53; ::_thesis: verum
end;
end;
end;
hence c1 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A20
.= c2 by A21, A22 ;
::_thesis: verum
end;
thus ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) ; ::_thesis: verum
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
let z, z9 be complex number ; ::_thesis: ( ( z9 <> 0 implies z9 * z = 1 ) & ( not z9 <> 0 implies z = 0 ) implies ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) ) )
assume that
A54: ( z9 <> 0 implies z9 * z = 1 ) and
A55: ( z9 = 0 implies z = 0 ) ; ::_thesis: ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) )
thus ( z <> 0 implies z * z9 = 1 ) by A54, A55; ::_thesis: ( not z <> 0 implies z9 = 0 )
assume A56: z = 0 ; ::_thesis: z9 = 0
assume z9 <> 0 ; ::_thesis: contradiction
then consider x1, x2, y1, y2 being Element of REAL such that
A57: z = [*x1,x2*] and
z9 = [*y1,y2*] and
A58: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by A54, Def5;
A59: z = [*0,0*] by A56, ARYTM_0:def_5;
then A60: x1 = 0 by A57, ARYTM_0:10;
A61: x2 = 0 by A57, A59, ARYTM_0:10;
A62: * (x1,y1) = 0 by A60, ARYTM_0:12;
* (x2,y2) = 0 by A61, ARYTM_0:12;
then A63: + ((* (x1,y1)),(opp (* (x2,y2)))) = 0 by A62, ARYTM_0:def_3;
A64: * (x1,y2) = 0 by A60, ARYTM_0:12;
* (x2,y1) = 0 by A61, ARYTM_0:12;
then + ((* (x1,y2)),(* (x2,y1))) = 0 by A64, ARYTM_0:11;
hence contradiction by A58, A63, ARYTM_0:def_5; ::_thesis: verum
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 ;
funcx - y -> set equals :: XCMPLX_0:def 8
x + (- y);
coherence
x + (- y) is set ;
funcx / 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 ;
clusterx - y -> complex ;
coherence
x - y is complex ;
clusterx / y -> complex ;
coherence
x / y is complex ;
end;
Lm3: for x, y, z being complex number holds x * (y * z) = (x * y) * z
proof
let x, y, z be complex number ; ::_thesis: x * (y * z) = (x * y) * z
consider x1, x2, y1, y2 being Element of REAL such that
A1: x = [*x1,x2*] and
A2: y = [*y1,y2*] and
A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def5;
consider y3, y4, z1, z2 being Element of REAL such that
A4: y = [*y3,y4*] and
A5: z = [*z1,z2*] and
A6: y * z = [*(+ ((* (y3,z1)),(opp (* (y4,z2))))),(+ ((* (y3,z2)),(* (y4,z1))))*] by Def5;
A7: y1 = y3 by A2, A4, ARYTM_0:10;
A8: y2 = y4 by A2, A4, ARYTM_0:10;
consider x3, x4, yz1, yz2 being Element of REAL such that
A9: x = [*x3,x4*] and
A10: y * z = [*yz1,yz2*] and
A11: x * (y * z) = [*(+ ((* (x3,yz1)),(opp (* (x4,yz2))))),(+ ((* (x3,yz2)),(* (x4,yz1))))*] by Def5;
A12: x1 = x3 by A1, A9, ARYTM_0:10;
A13: x2 = x4 by A1, A9, ARYTM_0:10;
consider xy1, xy2, z3, z4 being Element of REAL such that
A14: x * y = [*xy1,xy2*] and
A15: z = [*z3,z4*] and
A16: (x * y) * z = [*(+ ((* (xy1,z3)),(opp (* (xy2,z4))))),(+ ((* (xy1,z4)),(* (xy2,z3))))*] by Def5;
A17: z1 = z3 by A5, A15, ARYTM_0:10;
A18: z2 = z4 by A5, A15, ARYTM_0:10;
A19: xy1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A3, A14, ARYTM_0:10;
A20: xy2 = + ((* (x1,y2)),(* (x2,y1))) by A3, A14, ARYTM_0:10;
A21: yz1 = + ((* (y3,z1)),(opp (* (y4,z2)))) by A6, A10, ARYTM_0:10;
A22: yz2 = + ((* (y3,z2)),(* (y4,z1))) by A6, A10, ARYTM_0:10;
+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))) = + ((* ((opp x4),(* (y4,z1)))),(* ((* ((opp x2),y1)),z4))) by A7, A13, A18, ARYTM_0:13
.= + ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))) by A8, A13, A17, ARYTM_0:13 ;
then A23: + ((* (x3,(* ((opp y4),z2)))),(+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))))) = + ((* ((* (x1,(opp y2))),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by A8, A12, A18, ARYTM_0:13
.= + ((* ((opp (* (x1,y2))),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15
.= + ((* ((* ((opp x1),y2)),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15
.= + ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23 ;
A24: + ((* (x3,yz1)),(opp (* (x4,yz2)))) = + ((* (x3,yz1)),(* ((opp x4),yz2))) by ARYTM_0:15
.= + ((* (x3,(+ ((* (y3,z1)),(* ((opp y4),z2)))))),(* ((opp x4),yz2))) by A21, ARYTM_0:15
.= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(* ((opp x4),(+ ((* (y3,z2)),(* (y4,z1))))))) by A22, ARYTM_0:14
.= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))))) by ARYTM_0:14
.= + ((* (x3,(* (y3,z1)))),(+ ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))))) by A23, ARYTM_0:23
.= + ((+ ((* (x3,(* (y3,z1)))),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23
.= + ((+ ((* ((* (x1,y1)),z3)),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by A7, A12, A17, ARYTM_0:13
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:14
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((opp (* (x2,y1))),z4))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((opp (* (x1,y2))),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((opp (* ((* (x1,y2)),z4))),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (+ ((* ((* (x1,y2)),z4)),(* ((* (x2,y1)),z4)))))) by ARYTM_0:25
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (* ((+ ((* (x1,y2)),(* (x2,y1)))),z4)))) by ARYTM_0:14
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(* ((opp xy2),z4))) by A20, ARYTM_0:15
.= + ((* (xy1,z3)),(* ((opp xy2),z4))) by A19, ARYTM_0:15
.= + ((* (xy1,z3)),(opp (* (xy2,z4)))) by ARYTM_0:15 ;
A25: + ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))) = + ((opp (* ((* (x2,y2)),z4))),(* ((* (x2,y1)),z3))) by ARYTM_0:15
.= + ((* (x4,(* (y3,z1)))),(opp (* ((* (x2,y2)),z4)))) by A7, A13, A17, ARYTM_0:13
.= + ((* (x4,(* (y3,z1)))),(opp (* (x4,(* (y4,z2)))))) by A8, A13, A18, ARYTM_0:13
.= + ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))) by ARYTM_0:15 ;
A26: + ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))) = + ((* ((opp (* (x2,y2))),z4)),(+ ((* ((* (x1,y2)),z3)),(* ((* (x2,y1)),z3))))) by A20, ARYTM_0:14
.= + ((* ((* (x1,y2)),z3)),(+ ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))))) by ARYTM_0:23
.= + ((* (x3,(* (y4,z1)))),(+ ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))))) by A8, A12, A17, A25, ARYTM_0:13
.= + ((* (x3,(* (y4,z1)))),(* (x4,yz1))) by A21, ARYTM_0:14 ;
+ ((* (xy1,z4)),(* (xy2,z3))) = + ((+ ((* ((* (x1,y1)),z4)),(* ((opp (* (x2,y2))),z4)))),(* (xy2,z3))) by A19, ARYTM_0:14
.= + ((* ((* (x1,y1)),z4)),(+ ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))))) by ARYTM_0:23
.= + ((* (x3,(* (y3,z2)))),(+ ((* (x3,(* (y4,z1)))),(* (x4,yz1))))) by A7, A12, A18, A26, ARYTM_0:13
.= + ((+ ((* (x3,(* (y3,z2)))),(* (x3,(* (y4,z1)))))),(* (x4,yz1))) by ARYTM_0:23
.= + ((* (x3,yz2)),(* (x4,yz1))) by A22, ARYTM_0:14 ;
hence x * (y * z) = (x * y) * z by A11, A16, A24; ::_thesis: verum
end;
registration
cluster non zero complex for set ;
existence
not for b1 being complex number holds b1 is zero
proof
( REAL c= COMPLEX & 1 in REAL ) by NUMBERS:def_2, XBOOLE_1:7;
then 1 is complex number by Def2;
hence not for b1 being complex number holds b1 is zero ; ::_thesis: verum
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
assume A1: - x = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction
x + (- x) = 0 by Def6;
then consider x1, x2, y1, y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: - x = [*y1,y2*] and
A4: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by Def4;
A5: + (x2,y2) = 0 by A4, ARYTM_0:24;
then A6: + (x1,y1) = 0 by A4, ARYTM_0:def_5;
y2 = 0 by A1, A3, ARYTM_0:24;
then A7: y1 = 0 by A1, A3, ARYTM_0:def_5;
x2 = 0 by A1, A3, A5, ARYTM_0:11, ARYTM_0:24;
then x = x1 by A2, ARYTM_0:def_5
.= 0 by A6, A7, ARYTM_0:11 ;
hence contradiction ; ::_thesis: verum
end;
clusterx " -> non zero complex ;
coherence
not x " is zero
proof
assume A8: x " = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction
x * (x ") = 1 by Def7;
then consider x1, x2, y1, y2 being Element of REAL such that
x = [*x1,x2*] and
A9: x " = [*y1,y2*] and
A10: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def5;
y2 = 0 by A8, A9, ARYTM_0:24;
then A11: y1 = 0 by A8, A9, ARYTM_0:def_5;
+ ((* (x1,y2)),(* (x2,y1))) = 0 by A10, ARYTM_0:24;
then 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A10, ARYTM_0:def_5
.= + ((* (x1,y1)),(* ((opp x2),y2))) by ARYTM_0:15
.= * ((opp x2),y2) by A11, ARYTM_0:11, ARYTM_0:12 ;
hence contradiction by A8, A9, ARYTM_0:12, ARYTM_0:24; ::_thesis: verum
end;
let y be non zero complex number ;
clusterx * y -> non zero ;
coherence
not x * y is zero
proof
1 in REAL ;
then reconsider j = 1 as complex number by Def2, Lm4;
consider u1, u2, v1, v2 being Element of REAL such that
A12: j = [*u1,u2*] and
A13: ( y = [*v1,v2*] & j * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] ) by Def5;
A14: u2 = 0 by A12, ARYTM_0:24;
then A15: + ((* (u1,v2)),(* (u2,v1))) = * (u1,v2) by ARYTM_0:11, ARYTM_0:12;
A16: u1 = 1 by A12, A14, ARYTM_0:def_5;
+ (0,(opp 0)) = 0 by ARYTM_0:def_3;
then A17: opp 0 = 0 by ARYTM_0:11;
A18: + ((* (u1,v1)),(opp (* (u2,v2)))) = + (v1,(opp (* (u2,v2)))) by A16, ARYTM_0:19
.= + (v1,(* ((opp u2),v2))) by ARYTM_0:15
.= + (v1,(* (0,v2))) by A12, A17, ARYTM_0:24
.= v1 by ARYTM_0:11, ARYTM_0:12 ;
0 in REAL ;
then reconsider z = 0 as complex number by Def2, Lm4;
consider u1, u2, v1, v2 being Element of REAL such that
x " = [*u1,u2*] and
A19: z = [*v1,v2*] and
A20: (x ") * z = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] by Def5;
v2 = 0 by A19, ARYTM_0:24;
then A21: v1 = 0 by A19, ARYTM_0:def_5;
then A22: + ((* (u1,v1)),(opp (* (u2,v2)))) = opp (* (u2,v2)) by ARYTM_0:11, ARYTM_0:12
.= 0 by A17, A19, ARYTM_0:12, ARYTM_0:24 ;
A23: + ((* (u1,v2)),(* (u2,v1))) = + (0,(* (u2,v1))) by A19, ARYTM_0:12, ARYTM_0:24
.= * (u2,v1) by ARYTM_0:11
.= 0 by A21, ARYTM_0:12 ;
assume A24: x * y = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction
A25: ((x ") * x) * y = (x ") * (x * y) by Lm3
.= 0 by A20, A22, A23, A24, ARYTM_0:def_5 ;
((x ") * x) * y = j * y by Def7
.= y by A13, A15, A16, A18, ARYTM_0:19 ;
hence contradiction by A25; ::_thesis: verum
end;
end;
registration
let x, y be non zero complex number ;
clusterx / 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
let n be Element of REAL ; ::_thesis: n is complex
n in REAL ;
hence n is complex by Def2, Lm4; ::_thesis: verum
end;
end;
registration
cluster natural -> complex for set ;
coherence
for b1 being number st b1 is natural holds
b1 is complex
proof
let n be set ; ::_thesis: ( n is natural implies n is complex )
assume n is natural ; ::_thesis: n is complex
then n in NAT by ORDINAL1:def_12;
hence n is complex ; ::_thesis: verum
end;
end;
registration
cluster -> complex for Element of COMPLEX ;
coherence
for b1 being Element of COMPLEX holds b1 is complex by Def2;
end;
*