complex1.miz

begin

 reserve a,b,c,d for Real;

 theorem :: COMPLEX1:1



 Th1: ((a ^2 ) + (b ^2 )) = 0 implies a = 0

 proof

 0 <= (a ^2 ) & 0 <= (b ^2 ) by XREAL_1: 63;

 hence thesis;

 end;



 Lm1: 0 <= ((a ^2 ) + (b ^2 ))

 proof

 0 <= (a ^2 ) & 0 <= (b ^2 ) by XREAL_1: 63;

 hence thesis;

 end;

 definition

 let z be Complex;

 :: COMPLEX1:def1

 func Re z -> number means

 : Def1: it = z if z is real

 otherwise ex f be Function of 2, REAL st z = f & it = (f . 0 );

 existence

 proof

 thus z is real implies ex IT be set st IT = z

 proof

 assume z is real;

 then z in REAL by XREAL_0:def 1;

 hence thesis;

 end;



 A1: z in COMPLEX by XCMPLX_0:def 2;

 assume not z is real;

 then not z in REAL ;

 then z in (( Funcs (2, REAL )) \ { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 }) by A1, CARD_1: 50, NUMBERS:def 2, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 2, REAL by FUNCT_2: 66;

 take (f . 0 ), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 :: COMPLEX1:def2

 func Im z -> number means

 : Def2: it = 0 if z is real

 otherwise ex f be Function of 2, REAL st z = f & it = (f . 1);

 existence

 proof

 thus z is real implies ex IT be set st IT = 0 ;



 A2: z in COMPLEX by XCMPLX_0:def 2;

 assume not z is real;

 then not z in REAL ;

 then z in (( Funcs (2, REAL )) \ { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 }) by A2, CARD_1: 50, NUMBERS:def 2, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 2, REAL by FUNCT_2: 66;

 take (f . 1), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 end

 registration

 let z be Complex;

 cluster ( Re z) -> real;

 coherence

 proof

 per cases ;

 suppose z is real;

 hence thesis by Def1;

 end;

 suppose not z is real;

 then

 consider f be Function of 2, REAL such that z = f and

 A1: ( Re z) = (f . 0 ) by Def1;

 0 in 2 by CARD_1: 50, TARSKI:def 2;

 then (f . 0 ) in REAL by FUNCT_2: 5;

 hence thesis by A1;

 end;

 end;

 cluster ( Im z) -> real;

 coherence

 proof

 per cases ;

 suppose z is real;

 hence thesis by Def2;

 end;

 suppose not z is real;

 then

 consider f be Function of 2, REAL such that z = f and

 A2: ( Im z) = (f . 1) by Def2;

 1 in 2 by CARD_1: 50, TARSKI:def 2;

 then (f . 1) in REAL by FUNCT_2: 5;

 hence thesis by A2;

 end;

 end;

 end

 definition

 let z be Complex;

 :: original: Re

 redefine

 func Re z -> Element of REAL ;

 coherence by XREAL_0:def 1;

 :: original: Im

 redefine

 func Im z -> Element of REAL ;

 coherence by XREAL_0:def 1;

 end

 registration

 let r be Real;

 cluster ( Im r) -> zero;

 coherence by Def2;

 end

 theorem :: COMPLEX1:2



 Th2: for f be Function of 2, REAL holds ex a,b be Element of REAL st f = (( 0 ,1) --> (a,b))

 proof

 let f be Function of 2, REAL ;

 0 in 2 & 1 in 2 by CARD_1: 50, TARSKI:def 2;

 then

 reconsider a = (f . 0 ), b = (f . 1) as Element of REAL by FUNCT_2: 5;

 take a, b;

 ( dom f) = { 0 , 1} by CARD_1: 50, FUNCT_2:def 1;

 hence thesis by FUNCT_4: 66;

 end;



 Lm2: for a,b be Element of REAL holds ( Re [*a, b*]) = a & ( Im [*a, b*]) = b

 proof

 let a,b be Element of REAL ;

 reconsider a9 = a, b9 = b as Element of REAL ;

 thus ( Re [*a, b*]) = a

 proof

 per cases ;

 suppose b = 0 ;

 then [*a, b*] = a by ARYTM_0:def 5;

 hence thesis by Def1;

 end;

 suppose b <> 0 ;

 then

 A1: [*a, b*] = (( 0 ,1) --> (a9,b9)) by ARYTM_0:def 5;

 then

 reconsider f = [*a, b*] as Function of 2, REAL by CARD_1: 50;



 A2: not [*a, b*] in REAL & (f . 0 ) = a by A1, ARYTM_0: 8, FUNCT_4: 63;

 then not [*a, b*] is real by XREAL_0:def 1;

 hence thesis by Def1, A2;

 end;

 end;

 per cases ;

 suppose

 A2: b = 0 ;

 then [*a, b*] = a by ARYTM_0:def 5;

 hence thesis by A2;

 end;

 suppose b <> 0 ;

 then

 A3: [*a, b*] = (( 0 ,1) --> (a9,b9)) by ARYTM_0:def 5;

 then

 reconsider f = [*a, b*] as Function of 2, REAL by CARD_1: 50;



 A4: not [*a, b*] in REAL & (f . 1) = b by A3, ARYTM_0: 8, FUNCT_4: 63;

 then not [*a, b*] is real by XREAL_0:def 1;

 hence thesis by Def2, A4;

 end;

 end;

 reserve z,z1,z2 for Complex;



 Lm3: [*( Re z), ( Im z)*] = z

 proof



 A1: z in COMPLEX by XCMPLX_0:def 2;

 per cases ;

 suppose

 A2: z is real;

 then ( Im z) = 0 ;



 hence [*( Re z), ( Im z)*] = ( Re z) by ARYTM_0:def 5

 .= z by A2, Def1;

 end;

 suppose

 A3: not z is real;

 then

 a3: not z in REAL ;



 A4: ex f be Function of 2, REAL st z = f & ( Im z) = (f . 1) by Def2, A3;

 then

 consider a,b be Element of REAL such that

 A5: z = (( 0 ,1) --> (a,b)) by Th2;

 reconsider f = z as Element of ( Funcs (2, REAL )) by A5, CARD_1: 50, FUNCT_2: 8;

 z in (( Funcs (2, REAL )) \ { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 }) by A1, a3, CARD_1: 50, NUMBERS:def 2, XBOOLE_0:def 3;

 then not z in { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 } by XBOOLE_0:def 5;

 then (f . 1) <> 0 ;

 then

 A6: b <> 0 by A5, FUNCT_4: 63;

 ex f be Function of 2, REAL st z = f & ( Re z) = (f . 0 ) by A3, Def1;

 then

 A7: ( Re z) = a by A5, FUNCT_4: 63;

 ( Im z) = b by A4, A5, FUNCT_4: 63;

 hence thesis by A5, A7, A6, ARYTM_0:def 5;

 end;

 end;

 theorem :: COMPLEX1:3



 Th3: ( Re z1) = ( Re z2) & ( Im z1) = ( Im z2) implies z1 = z2

 proof

 assume ( Re z1) = ( Re z2) & ( Im z1) = ( Im z2);



 hence z1 = [*( Re z2), ( Im z2)*] by Lm3

 .= z2 by Lm3;

 end;

 definition

 let z1,z2 be Complex;

 :: original: =

 redefine

 :: COMPLEX1:def3

 pred z1 = z2 means ( Re z1) = ( Re z2) & ( Im z1) = ( Im z2);

 compatibility by Th3;

 end

 notation

 synonym 0c for 0 ;

 end

 definition

 :: original: 0c

 redefine

 func 0c -> Element of COMPLEX ;

 correctness by XCMPLX_0:def 2;

 end

 definition

 :: COMPLEX1:def4

 func 1r -> Element of COMPLEX equals 1;

 correctness by XCMPLX_0:def 2;

 :: original: 

 redefine

 func -> Element of COMPLEX ;

 coherence by XCMPLX_0:def 2;

 end

 theorem :: COMPLEX1:4



 Th4: ( Re 0 ) = 0 & ( Im 0 ) = 0

 proof

 reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

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

 hence thesis by Lm2;

 end;

 theorem :: COMPLEX1:5



 Th5: z = 0 iff ((( Re z) ^2 ) + (( Im z) ^2 )) = 0 by Th4, Th1;

 theorem :: COMPLEX1:6



 Th6: ( Re 1r ) = 1 & ( Im 1r ) = 0

 proof

 reconsider zz = 0 , j = 1 as Element of REAL by XREAL_0:def 1;

 1r = [*j, zz*] by ARYTM_0:def 5;

 hence thesis by Lm2;

 end;

 theorem :: COMPLEX1:7



 Th7: ( Re ) = 0 & ( Im ) = 1

 proof

 reconsider zz = 0 , j = 1 as Element of REAL by XREAL_0:def 1;

 = [*zz, j*] by ARYTM_0:def 5, XCMPLX_0:def 1;

 hence thesis by Lm2;

 end;



 Lm7: for x be Real, x1,x2 be Element of REAL st x = [*x1, x2*] holds x2 = 0 & x = x1

 proof

 let x be Real, x1,x2 be Element of REAL ;

 assume

 A1: x = [*x1, x2*];



 A2: x in REAL by XREAL_0:def 1;

 hereby

 assume x2 <> 0 ;

 then x = (( 0 ,1) --> (x1,x2)) by A1, ARYTM_0:def 5;

 hence contradiction by A2, ARYTM_0: 8;

 end;

 hence thesis by A1, ARYTM_0:def 5;

 end;



 Lm8: for x9,y9 be Element of REAL , x,y be Real st x9 = x & y9 = y holds ( + (x9,y9)) = (x + y)

 proof

 let x9,y9 be Element of REAL , x,y be Real such that

 A1: x9 = x & y9 = y;

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

 A2: x = [*x1, x2*] & y = [*y1, y2*] and

 A3: (x + y) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

 x2 = 0 & y2 = 0 by A2, Lm7;

 then

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

 x = x1 & y = y1 by A2, Lm7;

 hence thesis by A1, A3, A4, ARYTM_0:def 5;

 end;



 Lm9: for x be Element of REAL holds ( opp x) = ( - x)

 proof

 let x be Element of REAL ;

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

 then (x + ( opp x)) = 0 by Lm8;

 hence thesis;

 end;



 Lm10: for x9,y9 be Element of REAL , x,y be Real st x9 = x & y9 = y holds ( * (x9,y9)) = (x * y)

 proof

 let x9,y9 be Element of REAL , x,y be Real such that

 A1: x9 = x & y9 = y;

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

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

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

 A4: (x * y) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;

 x2 = 0 by A2, Lm7;

 then

 A5: ( * (x2,y1)) = 0 by ARYTM_0: 12;



 A6: y2 = 0 by A3, Lm7;

 then ( * (x1,y2)) = 0 by ARYTM_0: 12;

 then

 A7: ( + (( * (x1,y2)),( * (x2,y1)))) = 0 by A5, ARYTM_0: 11;

 x = x1 & y = y1 by A2, A3, Lm7;



 hence ( * (x9,y9)) = ( + (( * (x1,y1)),( * (( opp x2),y2)))) by A1, A6, ARYTM_0: 11, ARYTM_0: 12

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

 .= (x * y) by A4, A7, ARYTM_0:def 5;

 end;



 Lm11: for x,y,z be Complex st z = (x + y) holds ( Re z) = (( Re x) + ( Re y))

 proof

 let x,y,z be Complex such that

 A1: z = (x + y);

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

 A2: x = [*x1, x2*] & y = [*y1, y2*] and

 A3: (x + y) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;



 A4: ( Re x) = x1 & ( Re y) = y1 by A2, Lm2;



 thus ( Re z) = ( + (x1,y1)) by A1, A3, Lm2

 .= (( Re x) + ( Re y)) by A4, Lm8;

 end;



 Lm12: for x,y,z be Complex st z = (x + y) holds ( Im z) = (( Im x) + ( Im y))

 proof

 let x,y,z be Complex such that

 A1: z = (x + y);

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

 A2: x = [*x1, x2*] & y = [*y1, y2*] and

 A3: (x + y) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;



 A4: ( Im x) = x2 & ( Im y) = y2 by A2, Lm2;



 thus ( Im z) = ( + (x2,y2)) by A1, A3, Lm2

 .= (( Im x) + ( Im y)) by A4, Lm8;

 end;



 Lm13: for x,y,z be Complex st z = (x * y) holds ( Re z) = ((( Re x) * ( Re y)) - (( Im x) * ( Im y)))

 proof

 let x,y,z be Complex such that

 A1: z = (x * y);

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

 A2: x = [*x1, x2*] & y = [*y1, y2*] and

 A3: (x * y) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;



 A4: ( Re x) = x1 & ( Re y) = y1 by A2, Lm2;



 A5: ( Im x) = x2 & ( Im y) = y2 by A2, Lm2;



 thus ( Re z) = ( + (( * (x1,y1)),( opp ( * (x2,y2))))) by A1, A3, Lm2

 .= (( * (x1,y1)) + ( opp ( * (x2,y2)))) by Lm8

 .= ((x1 * y1) + ( opp ( * (x2,y2)))) by Lm10

 .= ((x1 * y1) + ( - ( * (x2,y2)))) by Lm9

 .= ((x1 * y1) - ( * (x2,y2)))

 .= ((( Re x) * ( Re y)) - (( Im x) * ( Im y))) by A4, A5, Lm10;

 end;



 Lm14: for x,y,z be Complex st z = (x * y) holds ( Im z) = ((( Re x) * ( Im y)) + (( Im x) * ( Re y)))

 proof

 let x,y,z be Complex such that

 A1: z = (x * y);

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

 A2: x = [*x1, x2*] & y = [*y1, y2*] and

 A3: (x * y) = [*( + (( * (x1,y1)),( opp ( * (x2,y2))))), ( + (( * (x1,y2)),( * (x2,y1))))*] by XCMPLX_0:def 5;



 A4: ( Im x) = x2 & ( Im y) = y2 by A2, Lm2;



 A5: ( Re x) = x1 & ( Re y) = y1 by A2, Lm2;



 thus ( Im z) = ( + (( * (x1,y2)),( * (x2,y1)))) by A1, A3, Lm2

 .= (( * (x1,y2)) + ( * (x2,y1))) by Lm8

 .= ((x1 * y2) + ( * (x2,y1))) by Lm10

 .= ((( Re x) * ( Im y)) + (( Im x) * ( Re y))) by A4, A5, Lm10;

 end;



 Lm15: (z1 + z2) = [*(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))*]

 proof

 set z = [*(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))*];

 reconsider z9 = (z1 + z2) as Element of COMPLEX by XCMPLX_0:def 2;



 A1: ( Im z) = (( Im z1) + ( Im z2)) by Lm2

 .= ( Im z9) by Lm12;

 ( Re z) = (( Re z1) + ( Re z2)) by Lm2

 .= ( Re z9) by Lm11;

 hence thesis by A1;

 end;



 Lm16: (z1 * z2) = [*((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))), ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))*]

 proof

 set z = [*((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))), ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))*];

 reconsider z9 = (z1 * z2) as Element of COMPLEX by XCMPLX_0:def 2;



 A1: ( Im z) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) by Lm2

 .= ( Im z9) by Lm14;

 ( Re z) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) by Lm2

 .= ( Re z9) by Lm13;

 hence thesis by A1;

 end;



 Lm17: ( Re (z1 * z2)) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) & ( Im (z1 * z2)) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))

 proof

 (z1 * z2) = [*((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))), ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))*] by Lm16;

 hence thesis by Lm2;

 end;



 Lm18: ( Re (z1 + z2)) = (( Re z1) + ( Re z2)) & ( Im (z1 + z2)) = (( Im z1) + ( Im z2))

 proof

 (z1 + z2) = [*(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))*] by Lm15;

 hence thesis by Lm2;

 end;



 Lm19: for x be Element of REAL holds ( Re (x * )) = 0

 proof

 let x be Element of REAL ;



 thus ( Re (x * )) = ((( Re x) * ( Re )) - (( Im x) * ( Im ))) by Lm17

 .= ((( Re x) * 0 ) - ( 0 * ( Im ))) by Th7

 .= 0 ;

 end;



 Lm20: for x be Element of REAL holds ( Im (x * )) = x

 proof

 let x be Element of REAL ;



 thus ( Im (x * )) = ((( Re x) * ( Im )) + (( Im x) * ( Re ))) by Lm17

 .= x by Def1, Th7;

 end;



 Lm21: for x,y be Element of REAL holds [*x, y*] = (x + (y * ))

 proof

 let x,y be Element of REAL ;



 A1: ( Im (x + (y * ))) = (( Im x) + ( Im (y * ))) by Lm18

 .= ( 0 + ( Im (y * )))

 .= y by Lm20;

 ( Re (x + (y * ))) = (( Re x) + ( Re (y * ))) by Lm18

 .= (( Re x) + 0 ) by Lm19

 .= x by Def1;

 hence thesis by A1, Lm3;

 end;

 definition

 ::$Canceled

 end

 theorem :: COMPLEX1:8



 Th8: ( Re (z1 + z2)) = (( Re z1) + ( Re z2)) & ( Im (z1 + z2)) = (( Im z1) + ( Im z2))

 proof

 (z1 + z2) = [*(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))*] by Lm15;

 hence thesis by Lm2;

 end;

 definition

 ::$Canceled

 end

 theorem :: COMPLEX1:9



 Th9: ( Re (z1 * z2)) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) & ( Im (z1 * z2)) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))

 proof

 (z1 * z2) = [*((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))), ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))*] by Lm16;

 hence thesis by Lm2;

 end;

 theorem :: COMPLEX1:10

 ( Re (a * )) = 0

 proof



 thus ( Re (a * )) = ((( Re a) * ( Re )) - (( Im a) * ( Im ))) by Th9

 .= ((( Re a) * 0 ) - ( 0 * ( Im ))) by Th7

 .= 0 ;

 end;

 theorem :: COMPLEX1:11

 ( Im (a * )) = a

 proof



 thus ( Im (a * )) = ((( Re a) * ( Im )) + (( Im a) * ( Re ))) by Th9

 .= a by Def1, Th7;

 end;

 theorem :: COMPLEX1:12



 Th12: ( Re (a + (b * ))) = a & ( Im (a + (b * ))) = b

 proof

 reconsider a, b as Element of REAL by XREAL_0:def 1;

 (a + (b * )) = [*a, b*] by Lm21;

 hence thesis by Lm2;

 end;

 theorem :: COMPLEX1:13



 Th13: (( Re z) + (( Im z) * )) = z

 proof

 [*( Re z), ( Im z)*] = z by Lm3;

 hence thesis by Lm21;

 end;

 theorem :: COMPLEX1:14



 Th14: ( Im z1) = 0 & ( Im z2) = 0 implies ( Re (z1 * z2)) = (( Re z1) * ( Re z2)) & ( Im (z1 * z2)) = 0

 proof

 assume that

 A1: ( Im z1) = 0 and

 A2: ( Im z2) = 0 ;



 thus ( Re (z1 * z2)) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) by Th9

 .= (( Re z1) * ( Re z2)) by A1;



 thus ( Im (z1 * z2)) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) by Th9

 .= 0 by A1, A2;

 end;

 theorem :: COMPLEX1:15



 Th15: ( Re z1) = 0 & ( Re z2) = 0 implies ( Re (z1 * z2)) = ( - (( Im z1) * ( Im z2))) & ( Im (z1 * z2)) = 0

 proof

 assume that

 A1: ( Re z1) = 0 and

 A2: ( Re z2) = 0 ;



 thus ( Re (z1 * z2)) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) by Th9

 .= ( - (( Im z1) * ( Im z2))) by A1;



 thus ( Im (z1 * z2)) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) by Th9

 .= 0 by A1, A2;

 end;

 theorem :: COMPLEX1:16

 ( Re (z * z)) = ((( Re z) ^2 ) - (( Im z) ^2 )) & ( Im (z * z)) = (2 * (( Re z) * ( Im z)))

 proof

 thus ( Re (z * z)) = ((( Re z) ^2 ) - (( Im z) ^2 )) by Th9;



 thus ( Im (z * z)) = ((( Re z) * ( Im z)) + (( Re z) * ( Im z))) by Th9

 .= (2 * (( Re z) * ( Im z)));

 end;

 definition

 ::$Canceled

 end



 Lm22: for z be Complex holds ( - z) = (( - ( Re z)) + (( - ( Im z)) * ))

 proof

 let z be Complex;

 reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

 set z9 = [*( - ( Re z)), ( - ( Im z))*];

 (z9 + z) = [*(( Re z9) + ( Re z)), (( Im z9) + ( Im z))*] by Lm15

 .= [*(( - ( Re z)) + ( Re z)), (( Im z9) + ( Im z))*] by Lm2

 .= [*zz, (( - ( Im z)) + ( Im z))*] by Lm2

 .= 0 by ARYTM_0:def 5;

 hence thesis by Lm21;

 end;

 theorem :: COMPLEX1:17



 Th17: ( Re ( - z)) = ( - ( Re z)) & ( Im ( - z)) = ( - ( Im z))

 proof

 ( - z) = (( - ( Re z)) + (( - ( Im z)) * )) by Lm22;

 hence thesis by Th12;

 end;

 theorem :: COMPLEX1:18

 ( * ) = ( - 1r );

 definition

 ::$Canceled

 end



 Lm23: for z1,z2 be Complex holds (z1 - z2) = ((( Re z1) - ( Re z2)) + ((( Im z1) - ( Im z2)) * ))

 proof

 let z1,z2 be Complex;



 A1: z1 = (( Re z1) + (( Im z1) * )) by Th13;

 (z1 - z2) = (z1 + ( - z2))

 .= (z1 + (( - ( Re z2)) + (( - ( Im z2)) * ))) by Lm22

 .= ((( Re z1) - ( Re z2)) + ((( Im z1) - ( Im z2)) * )) by A1;

 hence thesis;

 end;

 theorem :: COMPLEX1:19



 Th19: ( Re (z1 - z2)) = (( Re z1) - ( Re z2)) & ( Im (z1 - z2)) = (( Im z1) - ( Im z2))

 proof



 thus ( Re (z1 - z2)) = ( Re ((( Re z1) - ( Re z2)) + ((( Im z1) - ( Im z2)) * ))) by Lm23

 .= (( Re z1) - ( Re z2)) by Th12;



 thus ( Im (z1 - z2)) = ( Im ((( Re z1) - ( Re z2)) + ((( Im z1) - ( Im z2)) * ))) by Lm23

 .= (( Im z1) - ( Im z2)) by Th12;

 end;

 definition

 ::$Canceled

 end



 Lm24: for z be Complex holds (z " ) = ((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) + ((( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * ))

 proof

 let z be Complex;

 reconsider z9 = ((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) + ((( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * )) as Element of COMPLEX by XCMPLX_0:def 2;

 per cases ;

 suppose z = 0 ;

 hence thesis by Th4;

 end;

 suppose

 A1: z <> 0 ;

 then

 A2: ((( Re z) ^2 ) + (( Im z) ^2 )) <> 0 by Th5;



 A3: ( Im z9) = (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th12;



 then

 A4: ((( Re z) * ( Im z9)) + (( Re z9) * ( Im z))) = (((( Re z) / 1) * (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 )))) + ((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * ( Im z))) by Th12

 .= (((( Re z) * ( - ( Im z))) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 )))) + (((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * ( Im z)) / 1)) by XCMPLX_1: 76

 .= (((( Re z) * ( - ( Im z))) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 )))) + (((( Im z) / 1) * ( Re z)) / ((( Re z) ^2 ) + (( Im z) ^2 )))) by XCMPLX_1: 76

 .= ((( - (( Re z) * ( Im z))) + (( Re z) * ( Im z))) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by XCMPLX_1: 62

 .= 0 ;



 A5: ((( Re z) * ( Re z9)) - (( Im z) * ( Im z9))) = (((( Re z) / 1) * (( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 )))) - (( Im z) * (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))))) by A3, Th12

 .= (((( Re z) * ( Re z)) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 )))) - ((( Im z) / 1) * (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))))) by XCMPLX_1: 76

 .= (((( Re z) ^2 ) / ((( Re z) ^2 ) + (( Im z) ^2 ))) - ((( Im z) * ( - ( Im z))) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 ))))) by XCMPLX_1: 76

 .= (((( Re z) ^2 ) / ((( Re z) ^2 ) + (( Im z) ^2 ))) - (( - (( Im z) ^2 )) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 )))))

 .= (((( Re z) ^2 ) / ((( Re z) ^2 ) + (( Im z) ^2 ))) - ( - ((( Im z) ^2 ) / ((( Re z) ^2 ) + (( Im z) ^2 ))))) by XCMPLX_1: 187

 .= (((( Re z) ^2 ) / ((( Re z) ^2 ) + (( Im z) ^2 ))) + ((( Im z) ^2 ) / (1 * ((( Re z) ^2 ) + (( Im z) ^2 )))))

 .= (((( Re z) ^2 ) + (( Im z) ^2 )) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by XCMPLX_1: 62

 .= 1 by A2, XCMPLX_1: 60;

 (z * z9) = [*((( Re z) * ( Re z9)) - (( Im z) * ( Im z9))), ((( Re z) * ( Im z9)) + (( Re z9) * ( Im z)))*] by Lm16

 .= 1 by A5, A4, ARYTM_0:def 5;

 hence thesis by A1, XCMPLX_0:def 7;

 end;

 end;

 theorem :: COMPLEX1:20



 Th20: ( Re (z " )) = (( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) & ( Im (z " )) = (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 )))

 proof

 (z " ) = ((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) + ((( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * )) by Lm24;

 hence thesis by Th12;

 end;

 theorem :: COMPLEX1:21

 ( " ) = ( - );

 theorem :: COMPLEX1:22



 Th22: ( Re z) <> 0 & ( Im z) = 0 implies ( Re (z " )) = (( Re z) " ) & ( Im (z " )) = 0

 proof

 assume that

 A1: ( Re z) <> 0 and

 A2: ( Im z) = 0 ;

 ( Re (z " )) = (( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th20;



 hence ( Re (z " )) = ((1 * ( Re z)) / (( Re z) * ( Re z))) by A2

 .= (1 / ( Re z)) by A1, XCMPLX_1: 91

 .= (( Re z) " ) by XCMPLX_1: 215;

 ( Im (z " )) = (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th20;

 hence thesis by A2;

 end;

 theorem :: COMPLEX1:23



 Th23: ( Re z) = 0 & ( Im z) <> 0 implies ( Re (z " )) = 0 & ( Im (z " )) = ( - (( Im z) " ))

 proof

 assume that

 A1: ( Re z) = 0 and

 A2: ( Im z) <> 0 ;

 ( Re (z " )) = (( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th20;

 hence ( Re (z " )) = 0 by A1;

 ( Im (z " )) = (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th20;



 hence ( Im (z " )) = ( - ((1 * ( Im z)) / (( Im z) * ( Im z)))) by A1, XCMPLX_1: 187

 .= ( - (1 / ( Im z))) by A2, XCMPLX_1: 91

 .= ( - (( Im z) " )) by XCMPLX_1: 215;

 end;

 definition

 ::$Canceled

 end



 Lm25: for z1,z2 be Complex holds (z1 / z2) = ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) + ((((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) * ))

 proof

 let z1,z2 be Complex;

 reconsider z1, z2 as Element of COMPLEX by XCMPLX_0:def 2;

 reconsider k = ((( Re z2) ^2 ) + (( Im z2) ^2 )) as Element of REAL by XREAL_0:def 1;

 reconsider r = (( Re z2) / k), i = (( - ( Im z2)) / k) as Element of REAL ;



 A1: ( Re [*r, i*]) = ( Re ((( Re z2) / k) + ((( - ( Im z2)) / k) * ))) by Lm21

 .= (( Re z2) / k) by Th12;



 A2: ( Im [*r, i*]) = ( Im ((( Re z2) / k) + ((( - ( Im z2)) / k) * ))) by Lm21

 .= (( - ( Im z2)) / k) by Th12;

 reconsider r1 = (((( Re z1) / 1) * (( Re z2) / k)) - (( Im z1) * (( - ( Im z2)) / k))), i1 = ((( Re z1) * (( - ( Im z2)) / k)) + ((( Re z2) / k) * ( Im z1))) as Element of REAL by XREAL_0:def 1;

 (z1 / z2) = (z1 * (z2 " )) by XCMPLX_0:def 9

 .= (z1 * (r + (i * ))) by Lm24

 .= (z1 * [*r, i*]) by Lm21

 .= [*r1, i1*] by A1, A2, Lm16

 .= ((((( Re z1) / 1) * (( Re z2) / k)) - (( Im z1) * (( - ( Im z2)) / k))) + (((( Re z1) * (( - ( Im z2)) / k)) + ((( Re z2) / k) * ( Im z1))) * )) by Lm21

 .= ((((( Re z1) * ( Re z2)) / (1 * k)) - ((( Im z1) / 1) * (( - ( Im z2)) / k))) + (((( Re z1) * (( - ( Im z2)) / k)) + ((( Re z2) / k) * ( Im z1))) * )) by XCMPLX_1: 76

 .= ((((( Re z1) * ( Re z2)) / k) - ((( Im z1) * ( - ( Im z2))) / (1 * k))) + ((((( Re z1) / 1) * (( - ( Im z2)) / k)) + ((( Re z2) / k) * ( Im z1))) * )) by XCMPLX_1: 76

 .= ((((( Re z1) * ( Re z2)) / k) - ((( Im z1) * ( - ( Im z2))) / k)) + ((((( Re z1) * ( - ( Im z2))) / (1 * k)) + ((( Re z2) / k) * (( Im z1) / 1))) * )) by XCMPLX_1: 76

 .= ((((( Re z1) * ( Re z2)) / k) - ((( Im z1) * ( - ( Im z2))) / k)) + ((((( Re z1) * ( - ( Im z2))) / k) + ((( Im z1) * ( Re z2)) / (1 * k))) * )) by XCMPLX_1: 76

 .= ((((( Re z1) * ( Re z2)) - (( Im z1) * ( - ( Im z2)))) / k) + ((((( Re z1) * ( - ( Im z2))) / k) + ((( Im z1) * ( Re z2)) / (1 * k))) * )) by XCMPLX_1: 120

 .= ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / k) + (((( - (( Re z1) * ( Im z2))) + (( Im z1) * ( Re z2))) / k) * )) by XCMPLX_1: 62

 .= ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) + ((((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) * ));

 hence thesis;

 end;

 theorem :: COMPLEX1:24

 ( Re (z1 / z2)) = (((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) & ( Im (z1 / z2)) = (((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 )))

 proof



 thus ( Re (z1 / z2)) = ( Re ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) + ((((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) * ))) by Lm25

 .= (((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) by Th12;



 thus ( Im (z1 / z2)) = ( Im ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) + ((((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) * ))) by Lm25

 .= (((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) by Th12;

 end;

 theorem :: COMPLEX1:25

 ( Im z1) = 0 & ( Im z2) = 0 & ( Re z2) <> 0 implies ( Re (z1 / z2)) = (( Re z1) / ( Re z2)) & ( Im (z1 / z2)) = 0

 proof

 assume that

 A1: ( Im z1) = 0 and

 A2: ( Im z2) = 0 & ( Re z2) <> 0 ;



 A3: (z1 / z2) = (z1 * (z2 " )) & ( Im (z2 " )) = 0 by A2, Th22, XCMPLX_0:def 9;



 hence ( Re (z1 / z2)) = (( Re z1) * ( Re (z2 " ))) by A1, Th14

 .= (( Re z1) * (( Re z2) " )) by A2, Th22

 .= (( Re z1) / ( Re z2)) by XCMPLX_0:def 9;

 thus thesis by A1, A3, Th14;

 end;

 theorem :: COMPLEX1:26

 ( Re z1) = 0 & ( Re z2) = 0 & ( Im z2) <> 0 implies ( Re (z1 / z2)) = (( Im z1) / ( Im z2)) & ( Im (z1 / z2)) = 0

 proof

 assume that

 A1: ( Re z1) = 0 and

 A2: ( Re z2) = 0 & ( Im z2) <> 0 ;



 A3: (z1 / z2) = (z1 * (z2 " )) & ( Re (z2 " )) = 0 by A2, Th23, XCMPLX_0:def 9;



 hence ( Re (z1 / z2)) = ( - (( Im z1) * ( Im (z2 " )))) by A1, Th15

 .= ( - (( Im z1) * ( - (( Im z2) " )))) by A2, Th23

 .= ( - ( - (( Im z1) * (( Im z2) " ))))

 .= (( Im z1) / ( Im z2)) by XCMPLX_0:def 9;

 thus thesis by A1, A3, Th15;

 end;

 definition

 let z be Complex;

 :: COMPLEX1:def11

 func z *' -> Complex equals (( Re z) - (( Im z) * ));

 correctness ;

 involutiveness

 proof

 let z,z9 be Complex;

 assume z = (( Re z9) - (( Im z9) * ));

 then z = (( Re z9) + (( - ( Im z9)) * ));

 then ( Re z) = ( Re z9) & ( - ( Im z)) = ( - ( - ( Im z9))) by Th12;



 hence z9 = (( Re z) + (( - ( Im z)) * )) by Th13

 .= (( Re z) - (( Im z) * ));

 end;

 end

 theorem :: COMPLEX1:27



 Th27: ( Re (z *' )) = ( Re z) & ( Im (z *' )) = ( - ( Im z))

 proof

 (z *' ) = (( Re z) + (( - ( Im z)) * ));

 hence thesis by Th12;

 end;

 theorem :: COMPLEX1:28

 ( 0 *' ) = 0 by Th4;

 theorem :: COMPLEX1:29

 (z *' ) = 0 implies z = 0

 proof

 assume (z *' ) = 0 ;

 then 0 = (( Re z) + (( - ( Im z)) * ));

 hence ( Re z) = ( Re 0 ) & ( Im z) = ( Im 0 ) by Th12;

 end;

 theorem :: COMPLEX1:30

 ( 1r *' ) = 1r by Th6;

 theorem :: COMPLEX1:31

 ( *' ) = ( - ) by Th7;

 theorem :: COMPLEX1:32



 Th32: ((z1 + z2) *' ) = ((z1 *' ) + (z2 *' ))

 proof



 thus ( Re ((z1 + z2) *' )) = ( Re (z1 + z2)) by Th27

 .= (( Re z1) + ( Re z2)) by Th8

 .= (( Re (z1 *' )) + ( Re z2)) by Th27

 .= (( Re (z1 *' )) + ( Re (z2 *' ))) by Th27

 .= ( Re ((z1 *' ) + (z2 *' ))) by Th8;



 thus ( Im ((z1 + z2) *' )) = ( - ( Im (z1 + z2))) by Th27

 .= ( - (( Im z1) + ( - ( - ( Im z2))))) by Th8

 .= (( - ( Im z1)) + ( - ( Im z2)))

 .= (( Im (z1 *' )) + ( - ( Im z2))) by Th27

 .= (( Im (z1 *' )) + ( Im (z2 *' ))) by Th27

 .= ( Im ((z1 *' ) + (z2 *' ))) by Th8;

 end;

 theorem :: COMPLEX1:33



 Th33: (( - z) *' ) = ( - (z *' ))

 proof



 thus ( Re (( - z) *' )) = ( Re ( - z)) by Th27

 .= ( - ( Re z)) by Th17

 .= ( - ( Re (z *' ))) by Th27

 .= ( Re ( - (z *' ))) by Th17;



 thus ( Im (( - z) *' )) = ( - ( Im ( - z))) by Th27

 .= ( - ( - ( Im z))) by Th17

 .= ( - ( Im (z *' ))) by Th27

 .= ( Im ( - (z *' ))) by Th17;

 end;

 theorem :: COMPLEX1:34

 ((z1 - z2) *' ) = ((z1 *' ) - (z2 *' ))

 proof



 thus ((z1 - z2) *' ) = ((z1 + ( - z2)) *' )

 .= ((z1 *' ) + (( - z2) *' )) by Th32

 .= ((z1 *' ) + ( - (z2 *' ))) by Th33

 .= ((z1 *' ) - (z2 *' ));

 end;

 theorem :: COMPLEX1:35



 Th35: ((z1 * z2) *' ) = ((z1 *' ) * (z2 *' ))

 proof



 A1: ( Re (z1 *' )) = ( Re z1) & ( Re (z2 *' )) = ( Re z2) by Th27;



 A2: ( Im (z1 *' )) = ( - ( Im z1)) & ( Im (z2 *' )) = ( - ( Im z2)) by Th27;



 thus ( Re ((z1 * z2) *' )) = ( Re (z1 * z2)) by Th27

 .= ((( Re (z1 *' )) * ( Re (z2 *' ))) - (( - ( Im (z1 *' ))) * ( - ( Im (z2 *' ))))) by A1, A2, Th9

 .= ((( Re (z1 *' )) * ( Re (z2 *' ))) - ( - ( - (( Im (z1 *' )) * ( Im (z2 *' ))))))

 .= ( Re ((z1 *' ) * (z2 *' ))) by Th9;



 thus ( Im ((z1 * z2) *' )) = ( - ( Im (z1 * z2))) by Th27

 .= ( - ((( Re (z1 *' )) * ( - ( Im (z2 *' )))) + (( Re (z2 *' )) * ( - ( Im (z1 *' )))))) by A1, A2, Th9

 .= ((( Re (z2 *' )) * ( Im (z1 *' ))) + ( - ( - (( Re (z1 *' )) * ( Im (z2 *' ))))))

 .= ( Im ((z1 *' ) * (z2 *' ))) by Th9;

 end;

 theorem :: COMPLEX1:36



 Th36: ((z " ) *' ) = ((z *' ) " )

 proof



 A1: ( Re z) = ( Re (z *' )) & ( - ( Im z)) = ( Im (z *' )) by Th27;



 thus ( Re ((z " ) *' )) = ( Re (z " )) by Th27

 .= (( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) by Th20

 .= (( Re (z *' )) / ((( Re (z *' )) ^2 ) + (( Im (z *' )) ^2 ))) by A1

 .= ( Re ((z *' ) " )) by Th20;



 thus ( Im ((z " ) *' )) = ( - ( Im (z " ))) by Th27

 .= ( - (( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 )))) by Th20

 .= (( - ( Im (z *' ))) / ((( Re (z *' )) ^2 ) + (( Im (z *' )) ^2 ))) by A1, XCMPLX_1: 187

 .= ( Im ((z *' ) " )) by Th20;

 end;

 theorem :: COMPLEX1:37

 ((z1 / z2) *' ) = ((z1 *' ) / (z2 *' ))

 proof



 thus ((z1 / z2) *' ) = ((z1 * (z2 " )) *' ) by XCMPLX_0:def 9

 .= ((z1 *' ) * ((z2 " ) *' )) by Th35

 .= ((z1 *' ) * ((z2 *' ) " )) by Th36

 .= ((z1 *' ) / (z2 *' )) by XCMPLX_0:def 9;

 end;

 theorem :: COMPLEX1:38



 Th38: ( Im z) = 0 implies (z *' ) = z by Th27;

 registration

 let r be Real;

 reduce (r *' ) to r;

 reducibility by Th38;

 end

 theorem :: COMPLEX1:39

 ( Re z) = 0 implies (z *' ) = ( - z)

 proof

 assume

 A1: ( Re z) = 0 ;



 hence (z *' ) = (( - 0 ) + (( - ( Im z)) * ))

 .= ( - z) by A1, Lm22;

 end;

 theorem :: COMPLEX1:40

 ( Re (z * (z *' ))) = ((( Re z) ^2 ) + (( Im z) ^2 )) & ( Im (z * (z *' ))) = 0

 proof



 thus ( Re (z * (z *' ))) = ((( Re z) * ( Re (z *' ))) - (( Im z) * ( Im (z *' )))) by Th9

 .= ((( Re z) * ( Re z)) - (( Im z) * ( Im (z *' )))) by Th27

 .= ((( Re z) * ( Re z)) - (( Im z) * ( - ( Im z)))) by Th27

 .= ((( Re z) ^2 ) + (( Im z) ^2 ));



 thus ( Im (z * (z *' ))) = ((( Re z) * ( Im (z *' ))) + (( Re (z *' )) * ( Im z))) by Th9

 .= ((( Re z) * ( - ( Im z))) + (( Re (z *' )) * ( Im z))) by Th27

 .= (( - (( Re z) * ( Im z))) + (( Re z) * ( Im z))) by Th27

 .= 0 ;

 end;

 theorem :: COMPLEX1:41

 ( Re (z + (z *' ))) = (2 * ( Re z)) & ( Im (z + (z *' ))) = 0

 proof



 thus ( Re (z + (z *' ))) = (( Re z) + ( Re (z *' ))) by Th8

 .= (( Re z) + ( Re z)) by Th27

 .= (2 * ( Re z));



 thus ( Im (z + (z *' ))) = (( Im z) + ( Im (z *' ))) by Th8

 .= (( Im z) + ( - ( Im z))) by Th27

 .= 0 ;

 end;

 theorem :: COMPLEX1:42

 ( Re (z - (z *' ))) = 0 & ( Im (z - (z *' ))) = (2 * ( Im z))

 proof



 thus ( Re (z - (z *' ))) = (( Re z) - ( Re (z *' ))) by Th19

 .= (( Re z) - ( Re z)) by Th27

 .= 0 ;



 thus ( Im (z - (z *' ))) = (( Im z) - ( Im (z *' ))) by Th19

 .= (( Im z) - ( - ( Im z))) by Th27

 .= (2 * ( Im z));

 end;

 definition

 let z be Complex;

 :: COMPLEX1:def12

 func |.z.| -> Real equals ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 )));

 coherence ;

 projectivity

 proof

 let r be Real;

 reconsider rr = r as Element of REAL by XREAL_0:def 1;

 let z be Complex;

 assume

 A1: r = ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 )));

 (( Re z) ^2 ) >= 0 & (( Im z) ^2 ) >= 0 by XREAL_1: 63;

 then r >= 0 by A1, SQUARE_1:def 2;

 then

 A2: ( Re rr) >= 0 by Def1;



 thus r = ( Re rr) by Def1

 .= ( sqrt ((( Re r) ^2 ) + (( Im r) ^2 ))) by A2, SQUARE_1: 22;

 end;

 end

 theorem :: COMPLEX1:43



 Th43: a >= 0 implies |.a.| = a

 proof

 assume a >= 0 ;

 then ( Re a) >= 0 by Def1;



 hence |.a.| = ( Re a) by SQUARE_1: 22

 .= a by Def1;

 end;

 registration

 let z be zero Complex;

 cluster |.z.| -> zero;

 coherence by Th4, SQUARE_1: 17;

 end

 theorem :: COMPLEX1:44

 |. 0 .| = 0 ;

 registration

 let z be non zero Complex;

 cluster |.z.| -> non zero;

 coherence

 proof

 assume |.z.| is zero;

 then ((( Re z) ^2 ) + (( Im z) ^2 )) = 0 by Lm1, SQUARE_1: 24;

 hence thesis by Th5;

 end;

 end

 theorem :: COMPLEX1:45

 |.z.| = 0 implies z = 0 ;

 registration

 let z;

 cluster |.z.| -> non negative;

 coherence

 proof

 0 <= ((( Re z) ^2 ) + (( Im z) ^2 )) by Lm1;

 hence thesis by SQUARE_1:def 2;

 end;

 end

 theorem :: COMPLEX1:46

 0 <= |.z.|;

 theorem :: COMPLEX1:47

 z <> 0 iff 0 < |.z.|;

 theorem :: COMPLEX1:48



 Th48: |. 1r .| = 1 by Th6, SQUARE_1: 18;

 theorem :: COMPLEX1:49

 |. .| = 1 by Th7, SQUARE_1: 18;



 Lm26: |.( - z).| = |.z.|

 proof



 thus |.( - z).| = ( sqrt ((( - ( Re z)) ^2 ) + (( Im ( - z)) ^2 ))) by Th17

 .= ( sqrt ((( - ( Re z)) ^2 ) + (( - ( Im z)) ^2 ))) by Th17

 .= |.z.|;

 end;



 Lm27: a <= 0 implies |.a.| = ( - a)

 proof

 assume a <= 0 ;

 then |.( - a).| = ( - a) by Th43;

 hence thesis by Lm26;

 end;



 Lm28: ( sqrt (a ^2 )) = |.a.|

 proof

 per cases ;

 suppose

 A1: 0 <= a;

 then ( sqrt (a ^2 )) = a by SQUARE_1: 22;

 hence thesis by A1, Th43;

 end;

 suppose

 A2: not 0 <= a;

 then |.a.| = ( - a) by Lm27;

 hence thesis by A2, SQUARE_1: 23;

 end;

 end;

 theorem :: COMPLEX1:50

 ( Im z) = 0 implies |.z.| = |.( Re z).| by Lm28;

 theorem :: COMPLEX1:51

 ( Re z) = 0 implies |.z.| = |.( Im z).| by Lm28;

 theorem :: COMPLEX1:52

 |.( - z).| = |.z.| by Lm26;

 theorem :: COMPLEX1:53



 Th53: |.(z *' ).| = |.z.|

 proof



 thus |.(z *' ).| = ( sqrt ((( Re z) ^2 ) + (( Im (z *' )) ^2 ))) by Th27

 .= ( sqrt ((( Re z) ^2 ) + (( - ( Im z)) ^2 ))) by Th27

 .= |.z.|;

 end;



 Lm29: ( - |.a.|) <= a & a <= |.a.|

 proof

 a < 0 implies ( - |.a.|) <= a & a <= |.a.|

 proof

 assume a < 0 ;

 then |.a.| = ( - a) by Lm27;

 hence thesis;

 end;

 hence thesis by Th43;

 end;

 theorem :: COMPLEX1:54

 ( Re z) <= |.z.|

 proof

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then

 A1: ((( Re z) ^2 ) + 0 ) <= ((( Re z) ^2 ) + (( Im z) ^2 )) by XREAL_1: 7;

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then ( sqrt (( Re z) ^2 )) <= |.z.| by A1, SQUARE_1: 26;

 then

 A2: |.( Re z).| <= |.z.| by Lm28;

 ( Re z) <= |.( Re z).| by Lm29;

 hence thesis by A2, XXREAL_0: 2;

 end;

 theorem :: COMPLEX1:55

 ( Im z) <= |.z.|

 proof

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then

 A1: ((( Im z) ^2 ) + 0 ) <= ((( Re z) ^2 ) + (( Im z) ^2 )) by XREAL_1: 7;

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then ( sqrt (( Im z) ^2 )) <= |.z.| by A1, SQUARE_1: 26;

 then

 A2: |.( Im z).| <= |.z.| by Lm28;

 ( Im z) <= |.( Im z).| by Lm29;

 hence thesis by A2, XXREAL_0: 2;

 end;

 theorem :: COMPLEX1:56



 Th56: |.(z1 + z2).| <= ( |.z1.| + |.z2.|)

 proof

 set r1 = ( Re z1), r2 = ( Re z2), i1 = ( Im z1), i2 = ( Im z2);



 A1: (( Im (z1 + z2)) ^2 ) = ((i1 + i2) ^2 ) by Th8

 .= (((i1 ^2 ) + ((2 * i1) * i2)) + (i2 ^2 ));



 A2: 0 <= ((r1 ^2 ) + (i1 ^2 )) by Lm1;

 ((((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 ))) - (((r1 * r2) + (i1 * i2)) ^2 )) = (((r1 * i2) - (i1 * r2)) ^2 );

 then 0 <= ((((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 ))) - (((r1 * r2) + (i1 * i2)) ^2 )) by XREAL_1: 63;

 then

 A3: ((((r1 * r2) + (i1 * i2)) ^2 ) + 0 ) <= (((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 ))) by XREAL_1: 19;

 ((r1 * r2) + (i1 * i2)) <= |.((r1 * r2) + (i1 * i2)).| by Lm29;

 then

 A4: ((r1 * r2) + (i1 * i2)) <= ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) by Lm28;



 A5: 0 <= ((r2 ^2 ) + (i2 ^2 )) by Lm1;

 then

 A6: (( sqrt ((r2 ^2 ) + (i2 ^2 ))) ^2 ) = ((r2 ^2 ) + (i2 ^2 )) by SQUARE_1:def 2;

 0 <= (((r1 * r2) + (i1 * i2)) ^2 ) by XREAL_1: 63;

 then ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) <= ( sqrt (((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 )))) by A3, SQUARE_1: 26;

 then ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) <= (( sqrt ((r1 ^2 ) + (i1 ^2 ))) * ( sqrt ((r2 ^2 ) + (i2 ^2 )))) by A2, A5, SQUARE_1: 29;

 then

 A7: ((r1 * r2) + (i1 * i2)) <= (( sqrt ((r1 ^2 ) + (i1 ^2 ))) * ( sqrt ((r2 ^2 ) + (i2 ^2 )))) by A4, XXREAL_0: 2;

 (((2 * r1) * r2) + ((2 * i1) * i2)) = (2 * ((r1 * r2) + (i1 * i2)));

 then (((2 * r1) * r2) + ((2 * i1) * i2)) <= (2 * (( sqrt ((r1 ^2 ) + (i1 ^2 ))) * ( sqrt ((r2 ^2 ) + (i2 ^2 ))))) by A7, XREAL_1: 64;

 then

 A8: (((r1 ^2 ) + (i1 ^2 )) + (((2 * r1) * r2) + ((2 * i1) * i2))) <= (((r1 ^2 ) + (i1 ^2 )) + ((2 * ( sqrt ((r1 ^2 ) + (i1 ^2 )))) * ( sqrt ((r2 ^2 ) + (i2 ^2 ))))) by XREAL_1: 7;

 (( Re (z1 + z2)) ^2 ) = ((r1 + r2) ^2 ) by Th8

 .= (((r1 ^2 ) + ((2 * r1) * r2)) + (r2 ^2 ));

 then ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 )) = ((((r1 ^2 ) + (i1 ^2 )) + (((2 * r1) * r2) + ((2 * i1) * i2))) + ((r2 ^2 ) + (i2 ^2 ))) by A1;

 then

 A9: ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 )) <= ((((r1 ^2 ) + (i1 ^2 )) + ((2 * ( sqrt ((r1 ^2 ) + (i1 ^2 )))) * ( sqrt ((r2 ^2 ) + (i2 ^2 ))))) + ((r2 ^2 ) + (i2 ^2 ))) by A8, XREAL_1: 7;



 A10: 0 <= ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 )) by Lm1;

 (( sqrt ((r1 ^2 ) + (i1 ^2 ))) ^2 ) = ((r1 ^2 ) + (i1 ^2 )) by A2, SQUARE_1:def 2;

 then ( sqrt ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 ))) <= ( sqrt ((( sqrt ((r1 ^2 ) + (i1 ^2 ))) + ( sqrt ((r2 ^2 ) + (i2 ^2 )))) ^2 )) by A6, A9, A10, SQUARE_1: 26;

 hence thesis by SQUARE_1: 22;

 end;

 theorem :: COMPLEX1:57



 Th57: |.(z1 - z2).| <= ( |.z1.| + |.z2.|)

 proof

 |.(z1 - z2).| = |.(z1 + ( - z2)).|;

 then |.(z1 - z2).| <= ( |.z1.| + |.( - z2).|) by Th56;

 hence thesis by Lm26;

 end;

 theorem :: COMPLEX1:58

 ( |.z1.| - |.z2.|) <= |.(z1 + z2).|

 proof

 z1 = ((z1 + z2) - z2);

 then |.z1.| <= ( |.(z1 + z2).| + |.z2.|) by Th57;

 hence thesis by XREAL_1: 20;

 end;

 theorem :: COMPLEX1:59



 Th59: ( |.z1.| - |.z2.|) <= |.(z1 - z2).|

 proof

 z1 = ((z1 - z2) + z2);

 then |.z1.| <= ( |.(z1 - z2).| + |.z2.|) by Th56;

 hence thesis by XREAL_1: 20;

 end;

 theorem :: COMPLEX1:60



 Th60: |.(z1 - z2).| = |.(z2 - z1).|

 proof



 thus |.(z1 - z2).| = |.( - (z2 - z1)).|

 .= |.(z2 - z1).| by Lm26;

 end;

 theorem :: COMPLEX1:61



 Th61: |.(z1 - z2).| = 0 iff z1 = z2

 proof

 thus |.(z1 - z2).| = 0 implies z1 = z2

 proof

 assume |.(z1 - z2).| = 0 ;

 then (z1 - z2) = 0 ;

 hence thesis;

 end;

 thus thesis;

 end;

 theorem :: COMPLEX1:62

 z1 <> z2 iff 0 < |.(z1 - z2).|

 proof

 thus z1 <> z2 implies 0 < |.(z1 - z2).|

 proof

 assume z1 <> z2;

 then |.(z1 - z2).| <> 0 by Th61;

 hence thesis;

 end;

 thus thesis;

 end;

 theorem :: COMPLEX1:63

 |.(z1 - z2).| <= ( |.(z1 - z).| + |.(z - z2).|)

 proof

 |.(z1 - z2).| = |.((z1 - z) + (z - z2)).|;

 hence thesis by Th56;

 end;



 Lm30: ( - b) <= a & a <= b iff |.a.| <= b

 proof



 A1: |.a.| <= b implies ( - b) <= a & a <= b

 proof

 assume

 A2: |.a.| <= b;

 a < ( - 0 ) implies ( - b) <= a & a <= b

 proof

 assume

 A3: a < ( - 0 );

 then ( - a) <= b by A2, Lm27;

 then ( - b) <= ( - ( - a)) by XREAL_1: 24;

 hence thesis by A3;

 end;

 hence thesis by A2, Th43;

 end;

 ( - b) <= a & a <= b implies |.a.| <= b

 proof

 assume that

 A4: ( - b) <= a and

 A5: a <= b;

 ( - a) <= ( - ( - b)) by A4, XREAL_1: 24;

 then a < 0 implies |.a.| <= b by Lm27;

 hence thesis by A5, Th43;

 end;

 hence thesis by A1;

 end;

 theorem :: COMPLEX1:64

 |.( |.z1.| - |.z2.|).| <= |.(z1 - z2).|

 proof

 ( |.z2.| - |.z1.|) <= |.(z2 - z1).| by Th59;

 then ( - ( |.z1.| - |.z2.|)) <= |.(z1 - z2).| by Th60;

 then

 A1: ( - |.(z1 - z2).|) <= ( - ( - ( |.z1.| - |.z2.|))) by XREAL_1: 24;

 ( |.z1.| - |.z2.|) <= |.(z1 - z2).| by Th59;

 hence thesis by A1, Lm30;

 end;

 theorem :: COMPLEX1:65



 Th65: |.(z1 * z2).| = ( |.z1.| * |.z2.|)

 proof

 set r1 = ( Re z1), r2 = ( Re z2), i1 = ( Im z1), i2 = ( Im z2);



 A1: 0 <= ((r1 ^2 ) + (i1 ^2 )) & 0 <= ((r2 ^2 ) + (i2 ^2 )) by Lm1;



 A2: (( Im (z1 * z2)) ^2 ) = (((r1 * i2) + (r2 * i1)) ^2 ) by Th9

 .= (((2 * (r1 * r2)) * (i1 * i2)) + (((r1 * i2) ^2 ) + ((r2 * i1) ^2 )));

 (( Re (z1 * z2)) ^2 ) = (((r1 * r2) - (i1 * i2)) ^2 ) by Th9

 .= ((((r1 * r2) ^2 ) + ((i1 * i2) ^2 )) + ( - ((2 * (r1 * r2)) * (i1 * i2))));

 then ((( Re (z1 * z2)) ^2 ) + (( Im (z1 * z2)) ^2 )) = (((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 ))) by A2;

 hence thesis by A1, SQUARE_1: 29;

 end;

 theorem :: COMPLEX1:66



 Th66: |.(z " ).| = ( |.z.| " )

 proof

 per cases ;

 suppose

 A1: z <> 0 ;

 set r2i2 = ((( Re z) ^2 ) + (( Im z) ^2 ));



 A2: r2i2 <> 0 by A1, Th5;



 A3: 0 <= r2i2 by Lm1;



 thus |.(z " ).| = ( sqrt (((( Re z) / r2i2) ^2 ) + (( Im (z " )) ^2 ))) by Th20

 .= ( sqrt (((( Re z) / r2i2) ^2 ) + ((( - ( Im z)) / r2i2) ^2 ))) by Th20

 .= ( sqrt (((( Re z) ^2 ) / (r2i2 ^2 )) + ((( - ( Im z)) / r2i2) ^2 ))) by XCMPLX_1: 76

 .= ( sqrt (((( Re z) ^2 ) / (r2i2 ^2 )) + ((( - ( Im z)) ^2 ) / (r2i2 ^2 )))) by XCMPLX_1: 76

 .= ( sqrt ((1 * r2i2) / (r2i2 * r2i2))) by XCMPLX_1: 62

 .= ( sqrt (1 / r2i2)) by A2, XCMPLX_1: 91

 .= (1 / |.z.|) by A3, SQUARE_1: 18, SQUARE_1: 30

 .= ( |.z.| " ) by XCMPLX_1: 215;

 end;

 suppose

 A4: z = 0 ;



 hence |.(z " ).| = ( 0 " )

 .= ( |.z.| " ) by A4;

 end;

 end;

 theorem :: COMPLEX1:67



 Th67: ( |.z1.| / |.z2.|) = |.(z1 / z2).|

 proof



 thus ( |.z1.| / |.z2.|) = ( |.z1.| * ( |.z2.| " )) by XCMPLX_0:def 9

 .= ( |.z1.| * |.(z2 " ).|) by Th66

 .= |.(z1 * (z2 " )).| by Th65

 .= |.(z1 / z2).| by XCMPLX_0:def 9;

 end;

 theorem :: COMPLEX1:68

 |.(z * z).| = ((( Re z) ^2 ) + (( Im z) ^2 ))

 proof

 0 <= ((( Re z) ^2 ) + (( Im z) ^2 )) & |.(z * z).| = ( |.z.| * |.z.|) by Lm1, Th65;

 then |.(z * z).| = ( sqrt (((( Re z) ^2 ) + (( Im z) ^2 )) ^2 )) by SQUARE_1: 29;

 hence thesis by Lm1, SQUARE_1: 22;

 end;

 theorem :: COMPLEX1:69

 |.(z * z).| = |.(z * (z *' )).|

 proof



 thus |.(z * z).| = ( |.z.| * |.z.|) by Th65

 .= ( |.z.| * |.(z *' ).|) by Th53

 .= |.(z * (z *' )).| by Th65;

 end;

 theorem :: COMPLEX1:70

 a <= 0 implies |.a.| = ( - a) by Lm27;

 theorem :: COMPLEX1:71



 Th71: |.a.| = a or |.a.| = ( - a)

 proof

 a >= 0 or a < 0 ;

 hence thesis by Lm27, Th43;

 end;

 theorem :: COMPLEX1:72

 ( sqrt (a ^2 )) = |.a.| by Lm28;

 theorem :: COMPLEX1:73

 ( min (a,b)) = (((a + b) - |.(a - b).|) / 2)

 proof

 per cases ;

 suppose

 A1: a <= b;

 |.(a - b).| = |.( - (b - a)).|

 .= |.(b - a).| by Lm26

 .= (b - a) by A1, Th43, XREAL_1: 48;

 hence thesis by A1, XXREAL_0:def 9;

 end;

 suppose

 A2: b <= a;



 hence ( min (a,b)) = (((a + b) - (a - b)) / 2) by XXREAL_0:def 9

 .= (((a + b) - |.(a - b).|) / 2) by A2, Th43, XREAL_1: 48;

 end;

 end;

 theorem :: COMPLEX1:74

 ( max (a,b)) = (((a + b) + |.(a - b).|) / 2)

 proof

 per cases ;

 suppose

 A1: b <= a;



 hence ( max (a,b)) = (((a + b) + (a - b)) / 2) by XXREAL_0:def 10

 .= (((a + b) + |.(a - b).|) / 2) by A1, Th43, XREAL_1: 48;

 end;

 suppose

 A2: a <= b;

 then

 A3: 0 <= (b - a) by XREAL_1: 48;



 thus ( max (a,b)) = (((a + b) + ( - (a - b))) / 2) by A2, XXREAL_0:def 10

 .= (((a + b) + |.( - (a - b)).|) / 2) by A3, Th43

 .= (((a + b) + |.(a - b).|) / 2) by Lm26;

 end;

 end;

 theorem :: COMPLEX1:75



 Th75: ( |.a.| ^2 ) = (a ^2 )

 proof

 |.a.| = a or |.a.| = ( - a) by Th71;

 hence thesis;

 end;

 theorem :: COMPLEX1:76

 ( - |.a.|) <= a & a <= |.a.| by Lm29;

 theorem :: COMPLEX1:77

 (a + (b * )) = (c + (d * )) implies a = c & b = d

 proof

 assume

 A1: (a + (b * )) = (c + (d * ));

 then ((a - c) + ((b - d) * )) = 0 ;

 then (a - c) = 0 by Th4, Th12;

 hence thesis by A1;

 end;

 theorem :: COMPLEX1:78

 ( sqrt ((a ^2 ) + (b ^2 ))) <= ( |.a.| + |.b.|)

 proof



 A1: (( sqrt ((a ^2 ) + (b ^2 ))) ^2 ) >= 0 by XREAL_1: 63;

 (a ^2 ) >= 0 & (b ^2 ) >= 0 by XREAL_1: 63;

 then

 A2: (( sqrt ((a ^2 ) + (b ^2 ))) ^2 ) = ((a ^2 ) + (b ^2 )) by SQUARE_1:def 2;

 (( |.a.| + |.b.|) ^2 ) = ((( |.a.| ^2 ) + ((2 * |.a.|) * |.b.|)) + ( |.b.| ^2 )) & ( |.a.| ^2 ) = (a ^2 ) by Th75;



 then ((( |.a.| + |.b.|) ^2 ) - (( sqrt ((a ^2 ) + (b ^2 ))) ^2 )) = ((((a ^2 ) + ((2 * |.a.|) * |.b.|)) + (b ^2 )) - ((a ^2 ) + (b ^2 ))) by A2, Th75

 .= ((2 * |.a.|) * |.b.|);

 then (( |.a.| + |.b.|) ^2 ) >= (( sqrt ((a ^2 ) + (b ^2 ))) ^2 ) by XREAL_1: 49;

 then ( sqrt (( |.a.| + |.b.|) ^2 )) >= ( sqrt (( sqrt ((a ^2 ) + (b ^2 ))) ^2 )) by A1, SQUARE_1: 26;

 hence thesis by A2, SQUARE_1: 22;

 end;

 theorem :: COMPLEX1:79

 |.a.| <= ( sqrt ((a ^2 ) + (b ^2 )))

 proof

 (a ^2 ) >= 0 & ((a ^2 ) + 0 ) <= ((a ^2 ) + (b ^2 )) by XREAL_1: 6, XREAL_1: 63;

 then ( sqrt (a ^2 )) <= ( sqrt ((a ^2 ) + (b ^2 ))) by SQUARE_1: 26;

 hence thesis by Lm28;

 end;

 theorem :: COMPLEX1:80

 |.(1 / z1).| = (1 / |.z1.|) by Th48, Th67;

 theorem :: COMPLEX1:81

 for z1,z2 be Complex holds (z1 + z2) = ((( Re z1) + ( Re z2)) + ((( Im z1) + ( Im z2)) * ))

 proof

 let z1,z2 be Complex;

 (z1 + z2) = [*(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))*] by Lm15;

 hence thesis by Lm21;

 end;

 theorem :: COMPLEX1:82

 for z1,z2 be Complex holds (z1 * z2) = (((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) + (((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) * ))

 proof

 let z1,z2 be Complex;

 (z1 * z2) = [*((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))), ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1)))*] by Lm16;

 hence thesis by Lm21;

 end;

 theorem :: COMPLEX1:83

 for z be Complex holds ( - z) = (( - ( Re z)) + (( - ( Im z)) * )) by Lm22;

 theorem :: COMPLEX1:84

 for z1,z2 be Complex holds (z1 - z2) = ((( Re z1) - ( Re z2)) + ((( Im z1) - ( Im z2)) * )) by Lm23;

 theorem :: COMPLEX1:85

 for z be Complex holds (z " ) = ((( Re z) / ((( Re z) ^2 ) + (( Im z) ^2 ))) + ((( - ( Im z)) / ((( Re z) ^2 ) + (( Im z) ^2 ))) * )) by Lm24;

 theorem :: COMPLEX1:86

 for z1,z2 be Complex holds (z1 / z2) = ((((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) + ((((( Re z2) * ( Im z1)) - (( Re z1) * ( Im z2))) / ((( Re z2) ^2 ) + (( Im z2) ^2 ))) * )) by Lm25;