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;
canceled;
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;
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))*] )
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
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:
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))))*] )
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
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 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
Lm5:
for x, y, z being Complex holds x * (y * z) = (x * y) * z
Lm:
1 is Complex
;
Lm6:
REAL c= COMPLEX
by NUMBERS:def 2, XBOOLE_1:7;