xcmplx_0.miz

begin

 definition

 :: XCMPLX_0:def1

 func -> Number equals (( 0 ,1) --> ( 0 ,1));

 coherence ;

 let c be Number;

 :: XCMPLX_0:def2

 attr c is complex means

 : Def2: c in COMPLEX ;

 end

 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

 cluster -> complex;

 coherence

 proof

 set X = { x where x be Element of ( Funcs ( { 0 , 1}, REAL )) : (x . 1) = 0 };

 A1:

 now

 assume in X;

 then ex x be Element of ( Funcs ( { 0 , 1}, REAL )) st = x & (x . 1) = 0 ;

 hence contradiction by FUNCT_4: 63;

 end;



 A2: {( In ( 0 , REAL )), 1} c= REAL by ZFMISC_1: 32, Lm2;

 ( rng (( 0 ,1) --> ( 0 ,1))) c= {( In ( 0 , REAL )), 1} by FUNCT_4: 62, Lm1;

 then ( rng (( 0 ,1) --> ( 0 ,1))) c= REAL by A2, XBOOLE_1: 1;

 then is Relation of { 0 , 1}, REAL by RELSET_1: 6;

 then in ( Funcs ( { 0 , 1}, REAL )) by FUNCT_2: 8;

 then in (( Funcs ( { 0 , 1}, REAL )) \ X) by A1, XBOOLE_0:def 5;

 hence in COMPLEX by NUMBERS:def 2, XBOOLE_0:def 3;

 end;

 end

 registration

 cluster complex for Number;

 existence

 proof

 take ;

 thus thesis;

 end;

 cluster complex for number;

 existence

 proof

 take ;

 thus thesis;

 end;

 end

 definition

 mode Complex is complex Number;

 end

 registration

 sethood of Complex

 proof

 take COMPLEX ;

 thus thesis by Def2;

 end;

 end

 ::$Canceled

 definition

 let x,y be Complex;

 x in COMPLEX by Def2;

 then

 consider x1,x2 be Element of REAL such that

 A1: x = [*x1, x2*] by ARYTM_0: 9;

 y in COMPLEX by Def2;

 then

 consider y1,y2 be Element of REAL such that

 A2: y = [*y1, y2*] by ARYTM_0: 9;

 :: XCMPLX_0:def3

 func x + y -> number means

 : Def3: ex x1,x2,y1,y2 be Element of REAL st x = [*x1, x2*] & y = [*y1, y2*] & it = [*( + (x1,y1)), ( + (x2,y2))*];

 existence

 proof

 take IT = [*( + (x1,y1)), ( + (x2,y2))*];

 thus thesis by A1, A2;

 end;

 uniqueness

 proof

 let c1,c2 be number;

 given x1,x2,y1,y2 be Element of REAL such that

 A3: x = [*x1, x2*] and

 A4: y = [*y1, y2*] and

 A5: c1 = [*( + (x1,y1)), ( + (x2,y2))*];

 given x19,x29,y19,y29 be Element of REAL such that

 A6: x = [*x19, x29*] and

 A7: y = [*y19, y29*] and

 A8: c2 = [*( + (x19,y19)), ( + (x29,y29))*];



 A9: x1 = x19 & x2 = x29 by A3, A6, ARYTM_0: 10;

 y1 = y19 by A4, A7, ARYTM_0: 10;

 hence thesis by A4, A5, A7, A8, A9, ARYTM_0: 10;

 end;

 commutativity ;

 :: XCMPLX_0:def4

 func x * y -> number means

 : Def4: ex x1,x2,y1,y2 be Element of REAL st x = [*x1, x2*] & y = [*y1, y2*] & it = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*];

 existence

 proof

 take IT = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*];

 thus thesis by A1, A2;

 end;

 uniqueness

 proof

 let c1,c2 be number;

 given x1,x2,y1,y2 be 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))))*];

 given x19,x29,y19,y29 be 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))))*];



 A16: x1 = x19 & x2 = x29 by A10, A13, ARYTM_0: 10;

 y1 = y19 & y2 = y29 by A11, A14, ARYTM_0: 10;

 hence thesis by A12, A15, A16;

 end;

 commutativity ;

 end



 Lm4: for x,y,z be Element of REAL st ( + (x,y)) = 0 & ( + (x,z)) = 0 holds y = z

 proof

 let x,y,z be Element of REAL such that

 A1: ( + (x,y)) = 0 and

 A2: ( + (x,z)) = 0 ;

 per cases ;

 suppose x in REAL+ & y in REAL+ & z in REAL+ ;

 then (ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & 0 = (x9 + y9)) & ex x9,y9 be Element of REAL+ st x = x9 & z = y9 & 0 = (x9 + y9) by A1, A2, ARYTM_0:def 1;

 hence thesis by ARYTM_2: 11;

 end;

 suppose that

 A3: x in REAL+ and

 A4: y in REAL+ and

 A5: z in [: { 0 }, REAL+ :];



 A6: ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & 0 = (x9 + y9) by A1, A3, A4, ARYTM_0:def 1;

 consider x99,y99 be 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 thesis by A8, A9, A10, ARYTM_1: 19;

 end;

 suppose that

 A11: x in REAL+ and

 A12: z in REAL+ and

 A13: y in [: { 0 }, REAL+ :];



 A14: ex x9,z9 be Element of REAL+ st x = x9 & z = z9 & 0 = (x9 + z9) by A2, A11, A12, ARYTM_0:def 1;

 consider x99,y9 be 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 thesis by A16, A17, A18, ARYTM_1: 19;

 end;

 suppose that

 A19: x in REAL+ and

 A20: y in [: { 0 }, REAL+ :] and

 A21: z in [: { 0 }, REAL+ :];

 consider x9,y9 be 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 be 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 thesis by A23, A26;

 end;

 suppose that

 A28: z in REAL+ and

 A29: y in REAL+ and

 A30: x in [: { 0 }, REAL+ :];

 consider x9,y9 be 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 be 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 thesis by A32, A35;

 end;

 suppose not (x in REAL+ & y in REAL+ ) & not (x in REAL+ & y in [: { 0 }, REAL+ :]) & not (y in REAL+ & x in [: { 0 }, REAL+ :]);

 then ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & y = [ 0 , y9] & 0 = [ 0 , (x9 + y9)] by A1, ARYTM_0:def 1;

 hence thesis;

 end;

 suppose not (x in REAL+ & z in REAL+ ) & not (x in REAL+ & z in [: { 0 }, REAL+ :]) & not (z in REAL+ & x in [: { 0 }, REAL+ :]);

 then ex x9,z9 be Element of REAL+ st x = [ 0 , x9] & z = [ 0 , z9] & 0 = [ 0 , (x9 + z9)] by A2, ARYTM_0:def 1;

 hence thesis;

 end;

 end;

 registration

 let z,z9 be Complex;

 cluster (z + z9) -> complex;

 coherence

 proof

 ex x1,x2,y1,y2 be Element of REAL st z = [*x1, x2*] & z9 = [*y1, y2*] & (z + z9) = [*( + (x1,y1)), ( + (x2,y2))*] by Def3;

 hence (z + z9) in COMPLEX ;

 end;

 cluster (z * z9) -> complex;

 coherence

 proof

 ex x1,x2,y1,y2 be Element of REAL st z = [*x1, x2*] & z9 = [*y1, y2*] & (z * z9) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by Def4;

 hence (z * z9) in COMPLEX ;

 end;

 end

 definition

 let z be Complex;

 z in COMPLEX by Def2;

 then

 consider x,y be Element of REAL such that

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

 :: XCMPLX_0:def5

 func - z -> Complex means

 : Def5: (z + it ) = 0 ;

 existence

 proof

 reconsider z9 = [*( opp x), ( opp y)*] as Complex by Def2;

 take z9;



 A2: 0 = ( + (x,( opp x))) & 0 = ( + (y,( opp y))) by ARYTM_0:def 3;

 0 in NAT ;

 then

 reconsider zz = 0 as Element of REAL by NUMBERS: 19;

 0 = [*zz, zz*] by ARYTM_0:def 5;

 hence thesis by A1, Def3, A2;

 end;

 uniqueness

 proof

 let c1,c2 be Complex such that

 A2: (z + c1) = 0 and

 A3: (z + c2) = 0 ;

 consider x1,x2,y1,y2 be Element of REAL such that

 A4: z = [*x1, x2*] and

 A5: c1 = [*y1, y2*] and

 A6: 0 = [*( + (x1,y1)), ( + (x2,y2))*] by A2, Def3;

 consider x19,x29,y19,y29 be Element of REAL such that

 A7: z = [*x19, x29*] and

 A8: c2 = [*y19, y29*] and

 A9: 0 = [*( + (x19,y19)), ( + (x29,y29))*] by A3, Def3;



 A10: x1 = x19 by A4, A7, ARYTM_0: 10;



 A11: x2 = x29 by A4, A7, ARYTM_0: 10;

 0 in NAT ;

 then

 reconsider zz = 0 as Element of REAL by NUMBERS: 19;



 Lm3: 0 = [*zz, zz*] by ARYTM_0:def 5;



 A12: ( + (x1,y1)) = 0 by A6, Lm3, ARYTM_0: 10;

 ( + (x1,y19)) = 0 by A9, A10, Lm3, ARYTM_0: 10;

 then

 A13: y1 = y19 by A12, Lm4;



 A14: ( + (x2,y2)) = 0 by A6, Lm3, ARYTM_0: 10;

 ( + (x2,y29)) = 0 by A9, A11, Lm3, ARYTM_0: 10;

 hence thesis by A5, A8, A13, A14, Lm4;

 end;

 involutiveness ;

 :: XCMPLX_0:def6

 func z " -> Complex means

 : Def6: (z * it ) = 1 if z <> 0

 otherwise it = 0 ;

 existence

 proof

 thus z <> 0 implies ex z9 be Complex st (z * z9) = 1

 proof

 set y1 = ( * (x,( inv ( + (( * (x,x)),( * (y,y))))))), y2 = ( * (( opp y),( inv ( + (( * (x,x)),( * (y,y)))))));

 set z9 = [*y1, y2*];

 reconsider z9 as Complex by Def2;

 assume

 A15: z <> 0 ;

 take z9;



 A16: ( opp ( * (y,y2))) = ( 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,y1)) = ( * (( * (x,x)),( inv ( + (( * (x,x)),( * (y,y))))))) by ARYTM_0: 13;

 A18:

 now

 assume ( + (( * (x,x)),( * (y,y)))) = 0 ;

 then x = 0 & y = 0 by ARYTM_0: 17;

 hence contradiction by A1, A15, ARYTM_0:def 5;

 end;

 ( * (x,y2)) = ( * (( opp y),y1)) by ARYTM_0: 13

 .= ( opp ( * (y,y1))) by ARYTM_0: 15;

 then ( + (( * (x,y2)),( * (y,y1)))) = 0 by ARYTM_0:def 3;



 then [*( + (( * (x,y1)),( opp ( * (y,y2))))), ( + (( * (x,y2)),( * (y,y1))))*] = ( + (( * (x,y1)),( opp ( * (y,y2))))) 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 thesis by A1, Def4;

 end;

 assume z = 0 ;

 hence thesis;

 end;

 uniqueness

 proof

 let c1,c2 be Complex;

 0 in NAT ;

 then

 reconsider zz = 0 , j = 1 as Element of REAL by Lm2, NUMBERS: 19;

 thus z <> 0 & (z * c1) = 1 & (z * c2) = 1 implies c1 = c2

 proof

 assume that

 A19: z <> 0 and

 A20: (z * c1) = 1 and

 A21: (z * c2) = 1;



 A22: for z9 be Complex st (z * z9) = 1 holds z9 = [*( * (x,( inv ( + (( * (x,x)),( * (y,y))))))), ( * (( opp y),( inv ( + (( * (x,x)),( * (y,y)))))))*]

 proof

 let z9 be Complex such that

 A23: (z * z9) = 1;

 consider x1,x2,x9,y9 be 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, Def4;



 A27: x = x1 & y = x2 by A1, A24, ARYTM_0: 10;

 per cases by A1, A19, ARYTM_0:def 5;

 suppose that

 A28: x = 0 and

 A29: y <> 0 ;

 ( + (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))), ( + (zz,( * (y,x9))))*] by A26, A27, ARYTM_0: 11

 .= [*( opp ( * (y,y9))), ( * (y,x9))*] by ARYTM_0: 11;



 A32: 1 = [*j, zz*] 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 = [*zz, ( inv ( opp y))*] by A25, A29, A33, ARYTM_0: 21

 .= [*zz, ( opp ( * (j,( inv y))))*] by A35, ARYTM_0: 19

 .= [*zz, ( opp ( * (( * (y,( inv y))),( inv y))))*] by A29, ARYTM_0:def 4

 .= [*zz, ( opp ( * (y,( * (( inv y),( inv y))))))*] by ARYTM_0: 13

 .= [*zz, ( * (( opp y),( * (( inv y),( inv y)))))*] by ARYTM_0: 15

 .= [*zz, ( * (( opp y),( inv ( * (y,y)))))*] by ARYTM_0: 22

 .= [*zz, ( * (( opp y),( inv ( + (zz,( * (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;

 end;

 suppose that

 A36: ( opp y) = 0 and

 A37: x <> 0 ;

 ( + (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)),zz))*] by A26, A27, A39, ARYTM_0: 11

 .= [*( * (x,x9)), ( * (x,y9))*] by ARYTM_0: 11;



 A41: 1 = [*j, zz*] 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)),zz))))) by ARYTM_0: 11;

 hence thesis by A25, A36, A43, A44, ARYTM_0: 12;

 end;

 suppose that

 A45: ( opp y) <> 0 and

 A46: x <> 0 ;

 A47:

 now

 assume ( + (( * (( * (x,x)),( inv ( opp y)))),( opp y))) = 0 ;

 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;

 end;



 A50: 1 = [*j, zz*] 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 thesis by A25, A53;

 end;

 end;



 hence c1 = [*( * (x,( inv ( + (( * (x,x)),( * (y,y))))))), ( * (( opp y),( inv ( + (( * (x,x)),( * (y,y)))))))*] by A20

 .= c2 by A21, A22;

 end;

 thus thesis;

 end;

 consistency ;

 involutiveness

 proof

 let z,z9 be Complex;

 0 in NAT ;

 then

 reconsider zz = 0 as Element of REAL by NUMBERS: 19;

 assume that

 A54: z9 <> 0 implies (z9 * z) = 1 and

 A55: z9 = 0 implies z = 0 ;

 thus z <> 0 implies (z * z9) = 1 by A54, A55;

 assume

 A56: z = 0 ;

 assume z9 <> 0 ;

 then

 consider x1,x2,y1,y2 be 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, Def4;



 A59: z = [*zz, zz*] 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;

 end;

 end

 definition

 let x,y be Complex;

 :: XCMPLX_0:def7

 func x - y -> number equals (x + ( - y));

 coherence ;

 :: XCMPLX_0:def8

 func x / y -> number equals (x * (y " ));

 coherence ;

 end

 registration

 let x,y be Complex;

 cluster (x - y) -> complex;

 coherence ;

 cluster (x / y) -> complex;

 coherence ;

 end



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

 proof

 let x,y,z be Complex;

 consider x1,x2,y1,y2 be 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 Def4;

 consider y3,y4,z1,z2 be 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 Def4;



 A7: y1 = y3 by A2, A4, ARYTM_0: 10;



 A8: y2 = y4 by A2, A4, ARYTM_0: 10;

 consider x3,x4,yz1,yz2 be 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 Def4;



 A12: x1 = x3 by A1, A9, ARYTM_0: 10;



 A13: x2 = x4 by A1, A9, ARYTM_0: 10;

 consider xy1,xy2,z3,z4 be 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 Def4;



 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 thesis by A11, A16, A24;

 end;

 registration

 cluster natural -> complex for object;

 coherence by NUMBERS: 20;

 end



 Lm: 1 is Complex;

 registration

 cluster zero for Complex;

 existence

 proof

 take 0 ;

 thus thesis;

 end;

 cluster non zero for Complex;

 existence by Lm;

 cluster non zero for Complex;

 existence by Lm;

 end



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

 registration

 let x be non zero Complex;

 cluster ( - x) -> non zero;

 coherence

 proof

 assume

 A1: ( - x) = 0 ;

 (x + ( - x)) = 0 by Def5;

 then

 consider x1,x2,y1,y2 be Element of REAL such that

 A2: x = [*x1, x2*] and

 A3: ( - x) = [*y1, y2*] and

 A4: ( In ( 0 , REAL )) = [*( + (x1,y1)), ( + (x2,y2))*] by Def3, Lm1;



 A5: ( + (x2,y2)) = 0 by A4, ARYTM_0: 24;

 then

 A6: ( + (x1,y1)) = 0 by A4, ARYTM_0:def 5, Lm1;

 y2 = ( In ( 0 , REAL )) by A1, A3, ARYTM_0: 24, Lm1;

 then

 A7: y1 = 0 by A1, A3, ARYTM_0:def 5, Lm1;

 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;

 end;

 cluster (x " ) -> non zero;

 coherence

 proof

 assume

 A8: (x " ) = 0 ;

 then

 A9: (x " ) = ( In ( 0 , REAL )) by Lm1;

 (x * (x " )) = 1 by Def6;

 then

 consider x1,x2,y1,y2 be Element of REAL such that x = [*x1, x2*] and

 A10: (x " ) = [*y1, y2*] and

 A11: 1 = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by Def4;

 y2 = ( In ( 0 , REAL )) by A8, A10, ARYTM_0: 24, Lm1;

 then

 A12: y1 = 0 by A8, A10, ARYTM_0:def 5, Lm1;

 ( + (( * (x1,y2)),( * (x2,y1)))) = 0 by A11, ARYTM_0: 24, Lm2;



 then 1 = ( + (( * (x1,y1)),( opp ( * (x2,y2))))) by A11, ARYTM_0:def 5

 .= ( + (( * (x1,y1)),( * (( opp x2),y2)))) by ARYTM_0: 15

 .= ( * (( opp x2),y2)) by A12, ARYTM_0: 11, ARYTM_0: 12;

 hence contradiction by A10, ARYTM_0: 12, ARYTM_0: 24, A9;

 end;

 let y be non zero Complex;

 cluster (x * y) -> non zero;

 coherence

 proof

 set j = 1;

 0 in NAT ;

 then

 reconsider zz = 0 as Element of REAL by NUMBERS: 19;

 consider u1,u2,v1,v2 be Element of REAL such that

 A13: j = [*u1, u2*] and

 A14: y = [*v1, v2*] & (j * y) = [*( + (( * (u1,v1)),( opp ( * (u2,v2))))), ( + (( * (u1,v2)),( * (u2,v1))))*] by Def4;



 A15: u2 = 0 by A13, ARYTM_0: 24, Lm2;

 then

 A16: ( + (( * (u1,v2)),( * (u2,v1)))) = ( * (u1,v2)) by ARYTM_0: 11, ARYTM_0: 12;



 A17: u1 = 1 by A13, A15, ARYTM_0:def 5;

 ( + (zz,( opp zz))) = 0 by ARYTM_0:def 3;

 then

 A18: ( opp zz) = 0 by ARYTM_0: 11;



 A19: ( + (( * (u1,v1)),( opp ( * (u2,v2))))) = ( + (v1,( opp ( * (u2,v2))))) by A17, ARYTM_0: 19

 .= ( + (v1,( * (( opp u2),v2)))) by ARYTM_0: 15

 .= ( + (v1,( * (zz,v2)))) by A13, A18, ARYTM_0: 24, Lm2

 .= v1 by ARYTM_0: 11, ARYTM_0: 12;

 set z = 0 ;

 consider u1,u2,v1,v2 be Element of REAL such that (x " ) = [*u1, u2*] and

 A20: z = [*v1, v2*] and

 A21: ((x " ) * z) = [*( + (( * (u1,v1)),( opp ( * (u2,v2))))), ( + (( * (u1,v2)),( * (u2,v1))))*] by Def4;

 v2 = zz by A20, ARYTM_0: 24;

 then

 A22: v1 = 0 by A20, ARYTM_0:def 5;



 then

 A23: ( + (( * (u1,v1)),( opp ( * (u2,v2))))) = ( opp ( * (u2,v2))) by ARYTM_0: 11, ARYTM_0: 12

 .= 0 by A18, A20, ARYTM_0: 12, ARYTM_0: 24;



 A24: ( + (( * (u1,v2)),( * (u2,v1)))) = ( + (zz,( * (u2,v1)))) by A20, ARYTM_0: 12, ARYTM_0: 24

 .= ( * (u2,v1)) by ARYTM_0: 11

 .= 0 by A22, ARYTM_0: 12;

 assume

 A25: (x * y) = 0 ;



 A26: (((x " ) * x) * y) = ((x " ) * (x * y)) by Lm5

 .= 0 by A21, A23, A24, A25, ARYTM_0:def 5;

 (((x " ) * x) * y) = (j * y) by Def6

 .= y by A14, A16, A17, A19, ARYTM_0: 19;

 hence contradiction by A26;

 end;

 end

 registration

 let x,y be non zero Complex;

 cluster (x / y) -> non zero;

 coherence ;

 end

 registration

 cluster -> complex for Element of REAL ;

 coherence

 proof

 let n be Element of REAL ;

 n in REAL ;

 hence thesis by Lm6;

 end;

 end

 registration

 cluster -> complex for Element of COMPLEX ;

 coherence ;

 end

 registration

 let i be Complex;

 reduce ( In (i, COMPLEX )) to i;

 reducibility by Def2, SUBSET_1:def 8;

 end