:: by Library Committee

::

:: Received March 7, 2003

:: Copyright (c) 2003-2015 Association of Mizar Users

:: deftheorem Def2 defines complex XCMPLX_0:def 2 :

for c being object holds

( c is complex iff c in COMPLEX );

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

existence

ex b_{1} being object st b_{1} is complex

ex b_{1} being number st b_{1} is complex

end;
ex b

proof end;

existence ex b

proof end;

registration
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;

ex b_{1} being set ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] )

for b_{1}, b_{2} being set st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{2} = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds

b_{1} = b_{2}

for b_{1} being set

for x, y being Complex st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b_{1} = [*(+ (x1,y1)),(+ (x2,y2))*] )
;

ex b_{1} being set ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )

for b_{1}, b_{2} being set st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ ((* (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*] & b_{2} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds

b_{1} = b_{2}

for b_{1} being set

for x, y being Complex st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{1} = [*(+ ((* (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*] & b_{1} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )
;

end;
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 x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & it = [*(+ (x1,y1)),(+ (x2,y2))*] );

ex b

( x = [*x1,x2*] & y = [*y1,y2*] & b

proof end;

uniqueness for b

( x = [*x1,x2*] & y = [*y1,y2*] & b

( x = [*x1,x2*] & y = [*y1,y2*] & b

b

proof end;

commutativity for b

for x, y being Complex st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b

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 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))))*] );

ex b

( x = [*x1,x2*] & y = [*y1,y2*] & b

proof end;

uniqueness for b

( x = [*x1,x2*] & y = [*y1,y2*] & b

( x = [*x1,x2*] & y = [*y1,y2*] & b

b

proof end;

commutativity for b

for x, y being Complex st ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b

ex x1, x2, y1, y2 being Element of REAL st

( y = [*x1,x2*] & x = [*y1,y2*] & b

:: deftheorem Def3 defines + XCMPLX_0:def 3 :

for x, y being Complex

for b_{3} being set holds

( b_{3} = x + y iff ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{3} = [*(+ (x1,y1)),(+ (x2,y2))*] ) );

for x, y being Complex

for b

( b

( x = [*x1,x2*] & y = [*y1,y2*] & b

:: deftheorem Def4 defines * XCMPLX_0:def 4 :

for x, y being Complex

for b_{3} being set holds

( b_{3} = x * y iff ex x1, x2, y1, y2 being Element of REAL st

( x = [*x1,x2*] & y = [*y1,y2*] & b_{3} = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) );

for x, y being Complex

for b

( b

( x = [*x1,x2*] & y = [*y1,y2*] & b

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
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;

existence

ex b_{1} being Complex st z + b_{1} = 0

for b_{1}, b_{2} being Complex st z + b_{1} = 0 & z + b_{2} = 0 holds

b_{1} = b_{2}

for b_{1}, b_{2} being Complex st b_{2} + b_{1} = 0 holds

b_{1} + b_{2} = 0
;

existence

( ( z <> 0 implies ex b_{1} being Complex st z * b_{1} = 1 ) & ( not z <> 0 implies ex b_{1} being Complex st b_{1} = 0 ) )

for b_{1}, b_{2} being Complex holds

( ( z <> 0 & z * b_{1} = 1 & z * b_{2} = 1 implies b_{1} = b_{2} ) & ( not z <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Complex holds verum
;

involutiveness

for b_{1}, b_{2} being Complex st ( b_{2} <> 0 implies b_{2} * b_{1} = 1 ) & ( not b_{2} <> 0 implies b_{1} = 0 ) holds

( ( b_{1} <> 0 implies b_{1} * b_{2} = 1 ) & ( not b_{1} <> 0 implies b_{2} = 0 ) )

end;
z in COMPLEX by Def2;

then consider x, y being Element of REAL such that

A1: z = [*x,y*] by ARYTM_0:9;

existence

ex b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

b

existence

( ( z <> 0 implies ex b

proof end;

uniqueness for b

( ( z <> 0 & z * b

proof end;

consistency for b

involutiveness

for b

( ( b

proof end;

:: deftheorem Def5 defines - XCMPLX_0:def 5 :

for z, b_{2} being Complex holds

( b_{2} = - z iff z + b_{2} = 0 );

for z, b

( b

:: deftheorem Def6 defines " XCMPLX_0:def 6 :

for z, b_{2} being Complex holds

( ( z <> 0 implies ( b_{2} = z " iff z * b_{2} = 1 ) ) & ( not z <> 0 implies ( b_{2} = z " iff b_{2} = 0 ) ) );

for z, b

( ( z <> 0 implies ( b

Lm5: for x, y, z being Complex holds x * (y * z) = (x * y) * z

proof end;

registration
end;

Lm: 1 is Complex

;

registration

existence

ex b_{1} being Complex st b_{1} is zero

not for b_{1} being Complex holds b_{1} is zero
by Lm;

existence

not for b_{1} being Complex holds b_{1} is zero
by Lm;

end;
ex b

proof end;

existence not for b

existence

not for b

Lm6: REAL c= COMPLEX

by NUMBERS:def 2, XBOOLE_1:7;

registration

let x be non zero Complex;

coherence

not - x is zero

not x " is zero

coherence

not x * y is zero

end;
coherence

not - x is zero

proof end;

coherence not x " is zero

proof end;

let y be non zero Complex;coherence

not x * y is zero

proof end;

registration
end;

:: 26.05.2012, A.T.