complex2.miz

begin

 theorem :: COMPLEX2:1



 Th1: for a,b be Real st b > 0 holds ex r be Real st r = ((b * ( - [\(a / b)/])) + a) & 0 <= r & r 0 ;

 set ab = [\(a / b)/];

 set i = ( - ab);

 take r = ((b * i) + a);

 thus r = ((b * i) + a);

 ab <= (a / b) by INT_1:def 6;

 then (ab * b) <= ((a / b) * b) by A1, XREAL_1: 64;

 then (ab * b) <= a by A1, XCMPLX_1: 87;

 then ( - (ab * b)) >= ( - a) by XREAL_1: 24;

 then ((b * i) + a) >= (a + ( - a)) by XREAL_1: 6;

 hence 0 <= r;

 ((a / b) - 1) < ab by INT_1:def 6;

 then ( - ((a / b) - 1)) > i by XREAL_1: 24;

 then ((( - (a / b)) + 1) * b) > (i * b) by A1, XREAL_1: 68;

 then (( - ((a / b) * b)) + b) > (i * b);

 then (( - a) + b) > (i * b) by A1, XCMPLX_1: 87;

 then ((( - a) + b) + a) > r by XREAL_1: 8;

 hence thesis;

 end;

 theorem :: COMPLEX2:2



 Th2: for a,b,c be Real st a > 0 & b >= 0 & c >= 0 & b < a & c < a holds for i be Integer st b = (c + (a * i)) holds b = c

 proof

 let a,b,c be Real such that

 A1: a > 0 and

 A2: b >= 0 and

 A3: c >= 0 and

 A4: b < a and

 A5: c < a;



 A6: ( 0 + a) <= (c + a) by A3, XREAL_1: 7;

 let i be Integer such that

 A7: b = (c + (a * i));

 per cases ;

 suppose i < 0 ;

 then i <= ( - 1) by INT_1: 8;

 then (a * i) <= (a * ( - 1)) by A1, XREAL_1: 64;

 then (c + (a * i)) <= (c - a) by XREAL_1: 7;

 hence thesis by A2, A5, A7, XREAL_1: 49;

 end;

 suppose i = 0 ;

 hence thesis by A7;

 end;

 suppose i > 0 ;

 then ( 0 + 1) <= i by INT_1: 7;

 then (a * i) >= a by A1, XREAL_1: 151;

 then (c + (a * i)) >= (c + a) by XREAL_1: 7;

 hence thesis by A4, A7, A6, XXREAL_0: 2;

 end;

 end;

 theorem :: COMPLEX2:3



 Th3: for a,b be Real holds ( sin (a - b)) = ((( sin a) * ( cos b)) - (( cos a) * ( sin b))) & ( cos (a - b)) = ((( cos a) * ( cos b)) + (( sin a) * ( sin b)))

 proof

 let th1,th2 be Real;



 thus ( sin (th1 - th2)) = ( sin . (th1 + ( - th2))) by SIN_COS:def 17

 .= ((( sin . th1) * ( cos . ( - th2))) + (( cos . th1) * ( sin . ( - th2)))) by SIN_COS: 74

 .= ((( sin . th1) * ( cos . th2)) + (( cos . th1) * ( sin . ( - th2)))) by SIN_COS: 30

 .= ((( sin . th1) * ( cos . th2)) + (( cos . th1) * ( - ( sin . th2)))) by SIN_COS: 30

 .= ((( sin th1) * ( cos . th2)) - (( cos . th1) * ( sin . th2))) by SIN_COS:def 17

 .= ((( sin th1) * ( cos th2)) - (( cos . th1) * ( sin . th2))) by SIN_COS:def 19

 .= ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin . th2))) by SIN_COS:def 19

 .= ((( sin th1) * ( cos th2)) - (( cos th1) * ( sin th2))) by SIN_COS:def 17;



 thus ( cos (th1 - th2)) = ( cos . (th1 + ( - th2))) by SIN_COS:def 19

 .= ((( cos . th1) * ( cos . ( - th2))) - (( sin . th1) * ( sin . ( - th2)))) by SIN_COS: 74

 .= ((( cos . th1) * ( cos . th2)) - (( sin . th1) * ( sin . ( - th2)))) by SIN_COS: 30

 .= ((( cos . th1) * ( cos . th2)) - (( sin . th1) * ( - ( sin . th2)))) by SIN_COS: 30

 .= ((( cos th1) * ( cos . th2)) + (( sin . th1) * ( sin . th2))) by SIN_COS:def 19

 .= ((( cos th1) * ( cos th2)) + (( sin . th1) * ( sin . th2))) by SIN_COS:def 19

 .= ((( cos th1) * ( cos th2)) + (( sin th1) * ( sin . th2))) by SIN_COS:def 17

 .= ((( cos th1) * ( cos th2)) + (( sin th1) * ( sin th2))) by SIN_COS:def 17;

 end;

 theorem :: COMPLEX2:4

 for a be Real holds ( sin . (a - PI )) = ( - ( sin . a)) & ( cos . (a - PI )) = ( - ( cos . a))

 proof

 let th be Real;



 thus ( sin . (th - PI )) = ((( sin . th) * ( cos . ( - PI ))) + (( cos . th) * ( sin . ( - PI )))) by SIN_COS: 74

 .= ((( sin . th) * ( cos . PI )) + (( cos . th) * ( sin . ( - PI )))) by SIN_COS: 30

 .= ((( sin . th) * ( cos . PI )) + (( cos . th) * ( - ( sin . PI )))) by SIN_COS: 30

 .= ( - ( sin . th)) by SIN_COS: 76;



 thus ( cos . (th - PI )) = ((( cos . th) * ( cos . ( - PI ))) - (( sin . th) * ( sin . ( - PI )))) by SIN_COS: 74

 .= ((( cos . th) * ( cos . PI )) - (( sin . th) * ( sin . ( - PI )))) by SIN_COS: 30

 .= ((( cos . th) * ( cos . PI )) - (( sin . th) * ( - ( sin . PI )))) by SIN_COS: 30

 .= ( - ( cos . th)) by SIN_COS: 76;

 end;

 theorem :: COMPLEX2:5



 Th5: for a be Real holds ( sin (a - PI )) = ( - ( sin a)) & ( cos (a - PI )) = ( - ( cos a))

 proof

 let r be Real;



 thus ( sin (r - PI )) = ((( sin r) * ( cos PI )) - (( cos r) * ( sin PI ))) by Th3

 .= ( - ( sin r)) by SIN_COS: 77;



 thus ( cos (r - PI )) = ((( cos r) * ( cos PI )) + (( sin r) * ( sin PI ))) by Th3

 .= ( - ( cos r)) by SIN_COS: 77;

 end;

 theorem :: COMPLEX2:6



 Th6: for a,b be Real st a in ]. 0 , ( PI / 2).[ & b in ]. 0 , ( PI / 2).[ holds a < b iff ( sin a) < ( sin b)

 proof

 let a,b be Real;

 assume a in ]. 0 , ( PI / 2).[ & b in ]. 0 , ( PI / 2).[;

 then

 A1: a in ( ]. 0 , ( PI / 2).[ /\ ( dom sin )) & b in ( ]. 0 , ( PI / 2).[ /\ ( dom sin )) by SIN_COS: 24, XBOOLE_0:def 4;



 A2: ( sin a) = ( sin . a) & ( sin b) = ( sin . b) by SIN_COS:def 17;

 hence a = b;

 then a > b by A3, XXREAL_0: 1;

 hence contradiction by A2, A1, A3, RFUNCT_2: 20, SIN_COS2: 2;

 end;

 theorem :: COMPLEX2:7



 Th7: for a,b be Real st a in ].( PI / 2), PI .[ & b in ].( PI / 2), PI .[ holds a ( sin b)

 proof

 let a,b be Real;

 assume a in ].( PI / 2), PI .[ & b in ].( PI / 2), PI .[;

 then

 A1: a in ( ].( PI / 2), PI .[ /\ ( dom sin )) & b in ( ].( PI / 2), PI .[ /\ ( dom sin )) by SIN_COS: 24, XBOOLE_0:def 4;



 A2: ( sin a) = ( sin . a) & ( sin b) = ( sin . b) by SIN_COS:def 17;

 hence a ( sin b) by A1, RFUNCT_2: 21, SIN_COS2: 3;

 assume

 A3: ( sin a) > ( sin b);

 assume a >= b;

 then a > b by A3, XXREAL_0: 1;

 hence contradiction by A2, A1, A3, RFUNCT_2: 21, SIN_COS2: 3;

 end;

 theorem :: COMPLEX2:8



 Th8: for a be Real, i be Integer holds ( sin a) = ( sin (((2 * PI ) * i) + a))

 proof

 let r be Real, i be Integer;



 A1: ( sin . r) = ( sin r) by SIN_COS:def 17;



 A2: ( sin . (((2 * PI ) * i) + r)) = ( sin (((2 * PI ) * i) + r)) by SIN_COS:def 17;



 A3: ( sin . (((2 * PI ) * ( - i)) + (((2 * PI ) * i) + r))) = ( sin (((2 * PI ) * ( - i)) + (((2 * PI ) * i) + r))) by SIN_COS:def 17;

 per cases ;

 suppose i >= 0 ;

 then

 reconsider iN = i as Element of NAT by INT_1: 3;

 ( sin r) = ( sin (((2 * PI ) * iN) + r)) by A1, A2, SIN_COS2: 10;

 hence thesis;

 end;

 suppose i < 0 ;

 then

 reconsider iN = ( - i) as Element of NAT by INT_1: 3;

 set aa = (((2 * PI ) * i) + r);

 ( sin aa) = ( sin (((2 * PI ) * iN) + aa)) by A2, A3, SIN_COS2: 10;

 hence thesis;

 end;

 end;

 theorem :: COMPLEX2:9



 Th9: for a be Real, i be Integer holds ( cos a) = ( cos (((2 * PI ) * i) + a))

 proof

 let r be Real, i be Integer;



 A1: ( cos . r) = ( cos r) by SIN_COS:def 19;



 A2: ( cos . (((2 * PI ) * i) + r)) = ( cos (((2 * PI ) * i) + r)) by SIN_COS:def 19;



 A3: ( cos . (((2 * PI ) * ( - i)) + (((2 * PI ) * i) + r))) = ( cos (((2 * PI ) * ( - i)) + (((2 * PI ) * i) + r))) by SIN_COS:def 19;

 per cases ;

 suppose i >= 0 ;

 then

 reconsider iN = i as Element of NAT by INT_1: 3;

 ( cos r) = ( cos (((2 * PI ) * iN) + r)) by A1, A2, SIN_COS2: 11;

 hence thesis;

 end;

 suppose i < 0 ;

 then

 reconsider iN = ( - i) as Element of NAT by INT_1: 3;

 set aa = (((2 * PI ) * i) + r);

 ( cos aa) = ( cos (((2 * PI ) * iN) + aa)) by A2, A3, SIN_COS2: 11;

 hence thesis;

 end;

 end;

 theorem :: COMPLEX2:10



 Th10: for a be Real st ( sin a) = 0 holds ( cos a) <> 0

 proof

 let a be Real;

 assume that

 A1: ( sin a) = 0 and

 A2: ( cos a) = 0 ;

 consider r be Real such that

 A3: r = (((2 * PI ) * ( - [\(a / (2 * PI ))/])) + a) and

 A4: 0 <= r & r < (2 * PI ) by Th1, COMPTRIG: 5;



 A5: ( cos a) = ( cos r) by A3, Th9;

 ( sin a) = ( sin r) by A3, Th8;

 then r = 0 or r = PI by A4, A1, COMPTRIG: 17;

 hence thesis by A5, A2, COMPTRIG: 5, COMPTRIG: 18;

 end;

 theorem :: COMPLEX2:11



 Th11: for a,b be Real st 0 <= a & a < (2 * PI ) & 0 <= b & b < (2 * PI ) & ( sin a) = ( sin b) & ( cos a) = ( cos b) holds a = b

 proof

 let r,s be Real such that

 A1: 0 <= r and

 A2: r < (2 * PI ) & 0 <= s and

 A3: s < (2 * PI ) and

 A4: ( sin r) = ( sin s) & ( cos r) = ( cos s);



 A5: ( cos (r - s)) = ((( cos r) * ( cos s)) + (( sin r) * ( sin s))) by Th3

 .= 1 by A4, SIN_COS: 29;



 A6: ( sin (r - s)) = ((( sin r) * ( cos s)) - (( cos r) * ( sin s))) by Th3

 .= 0 by A4;



 A7: ( cos (s - r)) = ((( cos r) * ( cos s)) + (( sin r) * ( sin s))) by Th3

 .= 1 by A4, SIN_COS: 29;



 A8: ( sin (s - r)) = ((( sin s) * ( cos r)) - (( cos s) * ( sin r))) by Th3

 .= 0 by A4;

 per cases by XXREAL_0: 1;

 suppose

 A9: r > s;

 (r + 0 ) < ((2 * PI ) + s) by A2, XREAL_1: 8;

 then

 A10: (r - s) < (2 * PI ) by XREAL_1: 19;

 r > (s + 0 ) by A9;

 then 0 <= (r - s) by XREAL_1: 20;

 then (r - s) = 0 or (r - s) = PI by A6, A10, COMPTRIG: 17;

 hence thesis by A5, SIN_COS: 77;

 end;

 suppose r < s;

 then s > (r + 0 );

 then

 A11: 0 <= (s - r) by XREAL_1: 20;

 (s + 0 ) < ((2 * PI ) + r) by A1, A3, XREAL_1: 8;

 then (s - r) < (2 * PI ) by XREAL_1: 19;

 then (s - r) = 0 or (s - r) = PI by A8, A11, COMPTRIG: 17;

 hence thesis by A7, SIN_COS: 77;

 end;

 suppose r = s;

 hence thesis;

 end;

 end;

 begin



 Lm1: ( Arg 0 ) = 0 by COMPTRIG: 35;

 ::$Canceled

 theorem :: COMPLEX2:13



 Th12: for z be Complex st z <> 0 holds (( Arg z) < PI implies ( Arg ( - z)) = (( Arg z) + PI )) & (( Arg z) >= PI implies ( Arg ( - z)) = (( Arg z) - PI ))

 proof

 let z be Complex;

 assume

 A1: z <> 0 ;

 then

 A2: |.z.| <> 0 by COMPLEX1: 45;

 z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) by COMPTRIG: 62;

 then

 A3: ( - z) = (( - ( |.z.| * ( cos ( Arg z)))) + (( - ( |.z.| * ( sin ( Arg z)))) * ));

 ( Arg z) < (2 * PI ) by COMPTRIG: 34;

 then (( Arg z) + 0 ) < ((2 * PI ) + PI ) by COMPTRIG: 5, XREAL_1: 8;

 then

 A4: (( Arg z) - PI ) < (2 * PI ) by XREAL_1: 19;



 A5: ( - z) = (( |.( - z).| * ( cos ( Arg ( - z)))) + (( |.( - z).| * ( sin ( Arg ( - z)))) * )) by COMPTRIG: 62;



 A6: |.z.| = |.( - z).| by COMPLEX1: 52;

 then ( |.z.| * ( sin ( Arg ( - z)))) = ( |.z.| * ( - ( sin ( Arg z)))) by A5, A3, COMPLEX1: 77;

 then

 A7: ( sin ( Arg ( - z))) = ( - ( sin ( Arg z))) by A2, XCMPLX_1: 5;

 then

 A8: ( sin ( Arg ( - z))) = ( sin (( Arg z) + PI )) by SIN_COS: 79;

 ( |.z.| * ( cos ( Arg ( - z)))) = ( |.z.| * ( - ( cos ( Arg z)))) by A5, A3, A6, COMPLEX1: 77;

 then

 A9: ( cos ( Arg ( - z))) = ( - ( cos ( Arg z))) by A2, XCMPLX_1: 5;

 then

 A10: ( cos ( Arg ( - z))) = ( cos (( Arg z) + PI )) by SIN_COS: 79;

 hereby

 assume ( Arg z) < PI ;

 then

 A11: (( Arg z) + PI ) < ( PI + PI ) by XREAL_1: 8;

 0 <= ( Arg z) by COMPTRIG: 34;

 hence ( Arg ( - z)) = (( Arg z) + PI ) by A1, A5, A10, A8, A11, COMPTRIG: 5, COMPTRIG:def 1;

 end;

 assume ( Arg z) >= PI ;

 then

 A12: (( Arg z) - PI ) >= ( PI - PI ) by XREAL_1: 9;



 A13: ( sin ( Arg ( - z))) = ( sin (( Arg z) - PI )) by A7, Th5;

 ( cos ( Arg ( - z))) = ( cos (( Arg z) - PI )) by A9, Th5;

 hence thesis by A1, A5, A13, A12, A4, COMPTRIG:def 1;

 end;

 ::$Canceled

 theorem :: COMPLEX2:15



 Th13: for z be Complex holds ( Arg z) = 0 iff z = |.z.|

 proof

 let z be Complex;

 hereby

 assume ( Arg z) = 0 ;

 then z = (( |.z.| * ( cos 0 )) + (( |.z.| * ( sin 0 )) * )) by COMPTRIG: 62;

 hence z = |.z.| by SIN_COS: 31;

 end;

 assume z = |.z.|;

 hence thesis by COMPTRIG: 35, COMPLEX1: 46;

 end;

 theorem :: COMPLEX2:16



 Th14: for z be Complex st z <> 0 holds ( Arg z) < PI iff ( Arg ( - z)) >= PI

 proof

 let z be Complex;

 assume

 A1: z <> 0 ;

 thus ( Arg z) < PI implies ( Arg ( - z)) >= PI

 proof

 ( Arg z) >= 0 by COMPTRIG: 34;

 then

 A2: ( PI + 0 ) <= ( PI + ( Arg z)) by XREAL_1: 7;

 assume ( Arg z) < PI ;

 hence thesis by A1, A2, Th12;

 end;

 thus ( Arg ( - z)) >= PI implies ( Arg z) < PI

 proof

 (2 * PI ) > ( Arg ( - z)) by COMPTRIG: 34;

 then

 A3: (( PI + PI ) - PI ) > (( Arg ( - z)) - PI ) by XREAL_1: 9;

 assume ( Arg ( - z)) >= PI ;

 then ( Arg ( - ( - z))) = (( Arg ( - z)) - PI ) by A1, Th12;

 hence thesis by A3;

 end;

 end;

 theorem :: COMPLEX2:17



 Th15: for x,y be Complex st x <> y or (x - y) <> 0 holds ( Arg (x - y)) < PI iff ( Arg (y - x)) >= PI

 proof

 let z1,z2 be Complex;

 assume z1 <> z2 or (z1 - z2) <> 0 ;

 then (z1 - z2) <> 0c ;

 then ( Arg (z1 - z2)) < PI iff ( Arg ( - (z1 - z2))) >= PI by Th14;

 hence thesis;

 end;

 theorem :: COMPLEX2:18



 Th16: for z be Complex holds ( Arg z) in ]. 0 , PI .[ iff ( Im z) > 0

 proof

 let z be Complex;

 thus ( Arg z) in ]. 0 , PI .[ implies ( Im z) > 0

 proof

 assume ( Arg z) in ]. 0 , PI .[;

 then

 A1: 0 < ( Arg z) & ( Arg z) < PI by XXREAL_1: 4;



 A2: ( Arg z) < ( PI / 2) or ( Arg z) = ( PI / 2) or ( Arg z) > ( PI / 2) by XXREAL_0: 1;

 now

 per cases by A1, A2, XXREAL_1: 4;

 case ( Arg z) in ]. 0 , ( PI / 2).[;

 hence thesis by COMPTRIG: 41;

 end;

 case ( Arg z) = ( PI / 2);

 hence thesis by COMPTRIG: 48, SIN_COS: 77;

 end;

 case ( Arg z) in ].( PI / 2), PI .[;

 hence thesis by COMPTRIG: 42;

 end;

 end;

 hence thesis;

 end;



 A3: ].( PI / 2), PI .[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;



 A4: ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

 thus ( Im z) > 0 implies ( Arg z) in ]. 0 , PI .[

 proof

 assume

 A5: ( Im z) > 0 ;

 now

 per cases ;

 case ( Re z) > 0 ;

 then ( Arg z) in ]. 0 , ( PI / 2).[ by A5, COMPTRIG: 41;

 hence thesis by A4;

 end;

 case ( Re z) = 0 ;

 then z = ( 0 + (( Im z) * )) by COMPLEX1: 13;

 then ( Arg z) = ( PI / 2) by A5, COMPTRIG: 37;

 hence thesis by COMPTRIG: 5, XXREAL_1: 4;

 end;

 case ( Re z) < 0 ;

 then ( Arg z) in ].( PI / 2), PI .[ by A5, COMPTRIG: 42;

 hence thesis by A3;

 end;

 end;

 hence thesis;

 end;

 end;

 theorem :: COMPLEX2:19

 for z be Complex st ( Arg z) <> 0 holds ( Arg z) < PI iff ( sin ( Arg z)) > 0

 proof

 let z be Complex;



 A1: ( Arg z) >= 0 by COMPTRIG: 34;

 assume

 A2: ( Arg z) <> 0 ;

 hereby

 assume ( Arg z) < PI ;

 then ( Arg z) in ]. 0 , PI .[ by A2, A1, XXREAL_1: 4;

 then ( Im z) > 0 by Th16;

 hence ( sin ( Arg z)) > 0 by COMPTRIG: 45;

 end;



 A3: ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

 thus ( sin ( Arg z)) > 0 implies ( Arg z) < PI

 proof

 assume

 A4: ( sin ( Arg z)) > 0 ;

 then

 A5: ( Im z) > 0 by COMPTRIG: 48;

 now

 per cases ;

 suppose ( Re z) > 0 ;

 then ( Arg z) in ]. 0 , ( PI / 2).[ by A5, COMPTRIG: 41;

 hence thesis by A3, XXREAL_1: 4;

 end;

 suppose ( Re z) = 0 ;

 then z = ( 0 + (( Im z) * )) by COMPLEX1: 13;

 hence thesis by A4, COMPTRIG: 5, COMPTRIG: 37, COMPTRIG: 48;

 end;

 suppose ( Re z) < 0 ;

 then ( Arg z) in ].( PI / 2), PI .[ by A5, COMPTRIG: 42;

 hence thesis by XXREAL_1: 4;

 end;

 end;

 hence thesis;

 end;

 end;

 theorem :: COMPLEX2:20

 for x,y be Complex st ( Arg x) < PI & ( Arg y) < PI holds ( Arg (x + y)) < PI

 proof

 let z1,z2 be Complex;

 assume that

 A1: ( Arg z1) < PI and

 A2: ( Arg z2) < PI ;



 A3: |.z2.| = ( |.z2.| + ( 0 * ));



 A4: |.z1.| = ( |.z1.| + ( 0 * ));

 per cases by COMPTRIG: 34;

 suppose

 A5: ( Arg z1) = 0 ;

 then z1 = |.z1.| by Th13;

 then

 A6: ( Im z1) = 0 by A4, COMPLEX1: 12;

 per cases by COMPTRIG: 34;

 suppose ( Arg z2) = 0 ;

 then z2 = |.z2.| by Th13;

 then

 A7: (z1 + z2) = (( |.z1.| + |.z2.|) + ( 0 * )) by A5, Th13;

 0 <= |.z1.| & 0 <= |.z2.| by COMPLEX1: 46;

 hence thesis by A7, COMPTRIG: 5, COMPTRIG: 35;

 end;

 suppose ( Arg z2) > 0 ;

 then ( Arg z2) in ]. 0 , PI .[ by A2, XXREAL_1: 4;

 then

 A8: ( Im z2) > 0 by Th16;

 ( Im (z1 + z2)) = (( Im z1) + ( Im z2)) by COMPLEX1: 8;

 then ( Arg (z1 + z2)) in ]. 0 , PI .[ by A6, A8, Th16;

 hence thesis by XXREAL_1: 4;

 end;

 end;

 suppose ( Arg z1) > 0 ;

 then ( Arg z1) in ]. 0 , PI .[ by A1, XXREAL_1: 4;

 then

 A9: ( Im z1) > 0 by Th16;

 per cases by COMPTRIG: 34;

 suppose ( Arg z2) = 0 ;

 then z2 = |.z2.| by Th13;

 then

 A10: ( Im z2) = 0 by A3, COMPLEX1: 12;

 ( Im (z1 + z2)) = (( Im z1) + ( Im z2)) by COMPLEX1: 8;

 then ( Arg (z1 + z2)) in ]. 0 , PI .[ by A9, A10, Th16;

 hence thesis by XXREAL_1: 4;

 end;

 suppose ( Arg z2) > 0 ;

 then ( Arg z2) in ]. 0 , PI .[ by A2, XXREAL_1: 4;

 then

 A11: ( Im z2) > 0 by Th16;

 ( Im (z1 + z2)) = (( Im z1) + ( Im z2)) by COMPLEX1: 8;

 then ( Arg (z1 + z2)) in ]. 0 , PI .[ by A9, A11, Th16;

 hence thesis by XXREAL_1: 4;

 end;

 end;

 end;

 theorem :: COMPLEX2:21



 Th19: for z be Complex holds ( Arg z) = 0 iff ( Re z) >= 0 & ( Im z) = 0

 proof

 let z be Complex;



 A1: |.z.| = ( |.z.| + ( 0 * ));

 hereby

 assume ( Arg z) = 0 ;

 then

 A2: z = |.z.| by Th13;

 then ( Re z) = |.z.| by A1, COMPLEX1: 12;

 hence ( Re z) >= 0 & ( Im z) = 0 by A1, A2, COMPLEX1: 12, COMPLEX1: 46;

 end;

 assume that

 A3: ( Re z) >= 0 and

 A4: ( Im z) = 0 ;

 z = (( Re z) + ( 0 * )) by A4, COMPLEX1: 13;

 hence thesis by A3, COMPTRIG: 35;

 end;

 theorem :: COMPLEX2:22



 Th20: for z be Complex holds ( Arg z) = PI iff ( Re z) < 0 & ( Im z) = 0

 proof

 let z be Complex;

 hereby

 assume

 A1: ( Arg z) = PI ;

 per cases ;

 suppose

 A2: z <> 0 ;

 reconsider zz = |.z.| as Element of REAL by XREAL_0:def 1;



 A3: z = ((zz * ( cos PI )) + (( |.z.| * ( sin PI )) * )) & ( - ( - |.z.|)) > 0 by A1, COMPLEX1: 47, COMPTRIG:def 1, A2;

 ( cos PI ) = ( - 1) & ( sin PI ) = 0 by SIN_COS: 77;

 then

 A5: z = ((zz * ( - 1)) + ((zz * 0 ) * )) by A3;

 hence ( Re z) < 0 by COMPLEX1:def 1, A3;

 thus ( Im z) = 0 by COMPLEX1:def 2, A5;

 end;

 suppose z = 0 ;

 hence ( Re z) < 0 & ( Im z) = 0 by A1, COMPTRIG: 5, COMPTRIG: 35;

 end;

 end;

 assume that

 A6: ( Re z) < 0 and

 A7: ( Im z) = 0 ;

 z = (( Re z) + ( 0 * )) by A7, COMPLEX1: 13;

 hence thesis by A6, COMPTRIG: 36;

 end;

 theorem :: COMPLEX2:23



 Th21: for z be Complex holds ( Im z) = 0 iff ( Arg z) = 0 or ( Arg z) = PI

 proof

 let z be Complex;

 hereby



 A1: ( Arg (( Re z) + ( 0 * ))) = 0 or ( Arg (( Re z) + ( 0 * ))) = PI by COMPTRIG: 35, COMPTRIG: 36;

 assume ( Im z) = 0 ;

 hence ( Arg z) = 0 or ( Arg z) = PI by A1, COMPLEX1: 13;

 end;

 assume ( Arg z) = 0 or ( Arg z) = PI ;

 hence thesis by Th19, Th20;

 end;

 theorem :: COMPLEX2:24



 Th22: for z be Complex st ( Arg z) <= PI holds ( Im z) >= 0

 proof

 let z be Complex;

 assume

 A1: ( Arg z) <= PI ;

 per cases by A1, COMPTRIG: 34, XXREAL_0: 1;

 suppose ( Arg z) = PI or ( Arg z) = 0 ;

 hence thesis by Th21;

 end;

 suppose 0 < ( Arg z) & ( Arg z) < PI ;

 then ( Arg z) in ]. 0 , PI .[ by XXREAL_1: 4;

 hence thesis by Th16;

 end;

 end;

 theorem :: COMPLEX2:25



 Th23: for z be Element of COMPLEX st z <> 0 holds ( cos ( Arg ( - z))) = ( - ( cos ( Arg z))) & ( sin ( Arg ( - z))) = ( - ( sin ( Arg z)))

 proof

 let a be Element of COMPLEX ;



 A1: |.( - a).| = |.a.| by COMPLEX1: 52;

 assume a <> 0 ;

 then

 A2: |.a.| <> 0 by COMPLEX1: 45;

 a = (( |.a.| * ( cos ( Arg a))) + (( |.a.| * ( sin ( Arg a))) * )) & ( - a) = (( |.( - a).| * ( cos ( Arg ( - a)))) + (( |.( - a).| * ( sin ( Arg ( - a)))) * )) by COMPTRIG: 62;

 then

 A3: ( 0 + ( 0 * )) = ((( |.a.| * ( cos ( Arg a))) + ( |.a.| * ( cos ( Arg ( - a))))) + ((( |.a.| * ( sin ( Arg a))) + ( |.a.| * ( sin ( Arg ( - a))))) * )) by A1;

 then ( |.a.| * (( sin ( Arg a)) + ( sin ( Arg ( - a))))) = 0 by COMPLEX1: 4, COMPLEX1: 12;

 then

 A4: (( sin ( Arg a)) + ( - ( - ( sin ( Arg ( - a)))))) = 0 by A2;

 ( |.a.| * (( cos ( Arg a)) + ( cos ( Arg ( - a))))) = 0 by A3, COMPLEX1: 4, COMPLEX1: 12;

 then (( cos ( Arg a)) + ( - ( - ( cos ( Arg ( - a)))))) = 0 by A2;

 hence thesis by A4;

 end;

 theorem :: COMPLEX2:26



 Th24: for a be Complex st a <> 0 holds ( cos ( Arg a)) = (( Re a) / |.a.|) & ( sin ( Arg a)) = (( Im a) / |.a.|)

 proof

 let a be Complex;

 a = (( |.a.| * ( cos ( Arg a))) + (( |.a.| * ( sin ( Arg a))) * )) by COMPTRIG: 62;

 then

 A1: ( Re a) = ( |.a.| * ( cos ( Arg a))) & ( Im a) = ( |.a.| * ( sin ( Arg a))) by COMPLEX1: 12;

 assume a <> 0 ;

 hence thesis by A1, COMPLEX1: 45, XCMPLX_1: 89;

 end;

 theorem :: COMPLEX2:27



 Th25: for a be Complex, r be Real st r > 0 holds ( Arg (a * r)) = ( Arg a)

 proof

 let a be Complex, r be Real such that

 A1: r > 0 ;

 per cases ;

 suppose a = 0 ;

 hence thesis;

 end;

 suppose

 A2: a <> 0 ;

 then

 A3: ( sin ( Arg a)) = (( Im a) / |.a.|) by Th24;

 set b = (a * r);



 A4: |.b.| = ( |.a.| * |.r.|) by COMPLEX1: 65

 .= ( |.a.| * r) by A1, ABSVALUE:def 1;



 A5: ( cos ( Arg a)) = (( Re a) / |.a.|) by A2, Th24;



 A6: 0 <= ( Arg a) & ( Arg a) < (2 * PI ) by COMPTRIG: 34;

 r = (r + ( 0 * ));

 then

 A7: ( Re r) = r & ( Im r) = 0 by COMPLEX1: 12;



 then

 A8: ( Im b) = ((( Re a) * 0 ) + (r * ( Im a))) by COMPLEX1: 9

 .= (r * ( Im a));



 A9: ( sin ( Arg b)) = (( Im b) / |.b.|) by A1, A2, Th24

 .= ( sin ( Arg a)) by A1, A8, A4, A3, XCMPLX_1: 91;



 A10: 0 <= ( Arg b) & ( Arg b) < (2 * PI ) by COMPTRIG: 34;



 A11: ( Re b) = ((( Re a) * r) - ( 0 * ( Im a))) by A7, COMPLEX1: 9

 .= (r * ( Re a));

 ( cos ( Arg b)) = (( Re b) / |.b.|) by A1, A2, Th24

 .= ( cos ( Arg a)) by A1, A11, A4, A5, XCMPLX_1: 91;

 hence thesis by A9, A10, A6, Th11;

 end;

 end;

 theorem :: COMPLEX2:28



 Th26: for a be Complex, r be Real st r < 0 holds ( Arg (a * r)) = ( Arg ( - a))

 proof

 let a be Complex, r be Real such that

 A1: r < 0 ;

 per cases ;

 suppose a = 0 ;

 hence thesis;

 end;

 suppose

 A2: a <> 0 ;

 then

 A3: ( cos ( Arg a)) = (( Re a) / |.a.|) by Th24;



 A4: 0 <= ( Arg ( - a)) & ( Arg ( - a)) < (2 * PI ) by COMPTRIG: 34;



 A5: ( sin ( Arg a)) = (( Im a) / |.a.|) by A2, Th24;

 set b = (a * r);



 A6: a in COMPLEX by XCMPLX_0:def 2;



 A7: 0 <= ( Arg b) & ( Arg b) < (2 * PI ) by COMPTRIG: 34;



 A8: |.b.| = ( |.a.| * |.r.|) by COMPLEX1: 65

 .= ( |.a.| * ( - r)) by A1, ABSVALUE:def 1;

 r = (r + ( 0 * ));

 then

 A9: ( Re r) = r & ( Im r) = 0 by COMPLEX1: 12;



 then ( Im b) = ((( Re a) * 0 ) + (r * ( Im a))) by COMPLEX1: 9

 .= (r * ( Im a));



 then

 A10: ( sin ( Arg b)) = ((r * ( Im a)) / ( - ( |.a.| * r))) by A1, A2, A8, Th24

 .= ( - ((r * ( Im a)) / ( |.a.| * r))) by XCMPLX_1: 188

 .= ( - ( sin ( Arg a))) by A1, A5, XCMPLX_1: 91

 .= ( sin ( Arg ( - a))) by A2, A6, Th23;

 ( Re b) = ((( Re a) * r) - ( 0 * ( Im a))) by A9, COMPLEX1: 9

 .= (r * ( Re a));



 then ( cos ( Arg b)) = ((r * ( Re a)) / ( - ( |.a.| * r))) by A1, A2, A8, Th24

 .= ( - ((r * ( Re a)) / ( |.a.| * r))) by XCMPLX_1: 188

 .= ( - ( cos ( Arg a))) by A1, A3, XCMPLX_1: 91

 .= ( cos ( Arg ( - a))) by A2, A6, Th23;

 hence thesis by A10, A7, A4, Th11;

 end;

 end;

 begin

 definition

 let x,y be Complex;

 :: COMPLEX2:def1

 func x .|. y -> Element of COMPLEX equals (x * (y *' ));

 correctness by XCMPLX_0:def 2;

 end

 reserve a,b,c,d,x,y,z for Complex;

 theorem :: COMPLEX2:29



 Th27: (x .|. y) = (((( Re x) * ( Re y)) + (( Im x) * ( Im y))) + ((( - (( Re x) * ( Im y))) + (( Im x) * ( Re y))) * ))

 proof

 x = (( Re x) + (( Im x) * )) & (y *' ) = (( Re y) - (( Im y) * )) by COMPLEX1: 13, COMPLEX1:def 11;

 hence thesis;

 end;

 theorem :: COMPLEX2:30



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

 proof



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

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

 hence thesis;

 end;

 theorem :: COMPLEX2:31



 Th29: (z .|. z) = ( |.z.| ^2 ) & ( |.z.| ^2 ) = ( Re (z .|. z))

 proof



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



 A2: |.z.| = ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 ))) by COMPLEX1:def 12;



 thus

 A3: (z .|. z) = ((( Re z) ^2 ) + (( Im z) ^2 )) by Th28

 .= ( |.z.| ^2 ) by A1, A2, SQUARE_1:def 2;

 ( |.z.| ^2 ) = (( |.z.| ^2 ) + ( 0 * ) qua Complex);

 hence thesis by A3, COMPLEX1: 12;

 end;

 theorem :: COMPLEX2:32



 Th30: |.(x .|. y).| = ( |.x.| * |.y.|)

 proof



 thus |.(x .|. y).| = ( |.x.| * |.(y *' ).|) by COMPLEX1: 65

 .= ( |.x.| * |.y.|) by COMPLEX1: 53;

 end;

 theorem :: COMPLEX2:33

 (x .|. x) = 0 implies x = 0

 proof

 assume (x .|. x) = 0 ;

 then ((( Re x) ^2 ) + (( Im x) ^2 )) = 0 by Th28;

 hence thesis by COMPLEX1: 5;

 end;

 theorem :: COMPLEX2:34



 Th32: (y .|. x) = ((x .|. y) *' )

 proof



 thus (y .|. x) = (((y * (x *' )) *' ) *' )

 .= ((((x *' ) *' ) * (y *' )) *' ) by COMPLEX1: 35

 .= ((x .|. y) *' );

 end;

 theorem :: COMPLEX2:35

 ((x + y) .|. z) = ((x .|. z) + (y .|. z));

 theorem :: COMPLEX2:36



 Th34: (x .|. (y + z)) = ((x .|. y) + (x .|. z))

 proof



 thus (x .|. (y + z)) = (x * ((y *' ) + (z *' ))) by COMPLEX1: 32

 .= ((x .|. y) + (x .|. z));

 end;

 theorem :: COMPLEX2:37

 ((a * x) .|. y) = (a * (x .|. y));

 theorem :: COMPLEX2:38



 Th36: (x .|. (a * y)) = ((a *' ) * (x .|. y))

 proof



 thus (x .|. (a * y)) = (x * ((a *' ) * (y *' ))) by COMPLEX1: 35

 .= ((a *' ) * (x .|. y));

 end;

 theorem :: COMPLEX2:39

 ((a * x) .|. y) = (x .|. ((a *' ) * y))

 proof



 thus ((a * x) .|. y) = (x * (((a *' ) *' ) * (y *' )))

 .= (x .|. ((a *' ) * y)) by COMPLEX1: 35;

 end;

 theorem :: COMPLEX2:40

 (((a * x) + (b * y)) .|. z) = ((a * (x .|. z)) + (b * (y .|. z)));

 theorem :: COMPLEX2:41

 (x .|. ((a * y) + (b * z))) = (((a *' ) * (x .|. y)) + ((b *' ) * (x .|. z)))

 proof



 thus (x .|. ((a * y) + (b * z))) = ((x .|. (a * y)) + (x .|. (b * z))) by Th34

 .= (((a *' ) * (x .|. y)) + (x .|. (b * z))) by Th36

 .= (((a *' ) * (x .|. y)) + ((b *' ) * (x .|. z))) by Th36;

 end;

 theorem :: COMPLEX2:42



 Th40: (( - x) .|. y) = (x .|. ( - y))

 proof



 thus (( - x) .|. y) = (( - ( 1r *' )) * (x .|. y)) by COMPLEX1: 30, COMPLEX1:def 4

 .= ((( - 1r ) *' ) * (x .|. y)) by COMPLEX1: 33

 .= (x .|. (( - 1r ) * y)) by Th36

 .= (x .|. ( - y)) by COMPLEX1:def 4;

 end;

 theorem :: COMPLEX2:43

 (( - x) .|. y) = ( - (x .|. y));

 theorem :: COMPLEX2:44



 Th42: ( - (x .|. y)) = (x .|. ( - y))

 proof



 thus ( - (x .|. y)) = (( - x) .|. y)

 .= (x .|. ( - y)) by Th40;

 end;

 theorem :: COMPLEX2:45

 (( - x) .|. ( - y)) = (x .|. y)

 proof

 (( - x) .|. ( - y)) = ( - (x .|. ( - y)))

 .= ( - ( - (x .|. y))) by Th42;

 hence thesis;

 end;

 theorem :: COMPLEX2:46

 ((x - y) .|. z) = ((x .|. z) - (y .|. z));

 theorem :: COMPLEX2:47



 Th45: (x .|. (y - z)) = ((x .|. y) - (x .|. z))

 proof



 thus (x .|. (y - z)) = (x * ((y *' ) - (z *' ))) by COMPLEX1: 34

 .= ((x .|. y) - (x .|. z));

 end;

 theorem :: COMPLEX2:48

 ((x + y) .|. (x + y)) = ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))

 proof

 ((x + y) .|. (x + y)) = ((x .|. (x + y)) + (y .|. (x + y)))

 .= (((x .|. x) + (x .|. y)) + (y .|. (x + y))) by Th34

 .= (((x .|. x) + (x .|. y)) + ((y .|. x) + (y .|. y))) by Th34

 .= ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y));

 hence thesis;

 end;

 theorem :: COMPLEX2:49



 Th47: ((x - y) .|. (x - y)) = ((((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y))

 proof

 ((x - y) .|. (x - y)) = ((x .|. (x - y)) - (y .|. (x - y)))

 .= (((x .|. x) - (x .|. y)) - (y .|. (x - y))) by Th45

 .= (((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y))) by Th45

 .= ((((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y));

 hence thesis;

 end;



 Lm2: ( |.z.| ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 ))

 proof



 thus ( |.z.| ^2 ) = |.(z * z).| by COMPLEX1: 65

 .= ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 68;

 end;

 theorem :: COMPLEX2:50



 Th48: ( Re (x .|. y)) = 0 iff ( Im (x .|. y)) = ( |.x.| * |.y.|) or ( Im (x .|. y)) = ( - ( |.x.| * |.y.|))

 proof

 hereby

 assume

 A1: ( Re (x .|. y)) = 0 ;

 (( |.x.| * |.y.|) ^2 ) = ( |.(x .|. y).| ^2 ) by Th30

 .= (( 0 ^2 ) + (( Im (x .|. y)) ^2 )) by A1, Lm2

 .= (( Im (x .|. y)) ^2 );

 hence ( Im (x .|. y)) = ( |.x.| * |.y.|) or ( Im (x .|. y)) = ( - ( |.x.| * |.y.|)) by SQUARE_1: 40;

 end;

 hereby

 assume ( Im (x .|. y)) = ( |.x.| * |.y.|) or ( Im (x .|. y)) = ( - ( |.x.| * |.y.|));



 then (( Im (x .|. y)) ^2 ) = (( |.x.| * |.y.|) ^2 )

 .= ( |.(x .|. y).| ^2 ) by Th30

 .= ((( Re (x .|. y)) ^2 ) + (( Im (x .|. y)) ^2 )) by Lm2;

 hence ( Re (x .|. y)) = 0 ;

 end;

 end;

 begin

 definition

 let a be Complex, r be Real;

 :: COMPLEX2:def2

 func Rotate (a,r) -> Element of COMPLEX equals (( |.a.| * ( cos (r + ( Arg a)))) + (( |.a.| * ( sin (r + ( Arg a)))) * ));

 correctness by XCMPLX_0:def 2;

 end

 reserve r for Real;

 theorem :: COMPLEX2:51

 ( Rotate (a, 0 )) = a by COMPTRIG: 62;

 theorem :: COMPLEX2:52



 Th50: for a be Complex holds ( Rotate (a,r)) = 0 iff a = 0

 proof

 let a be Complex;

 hereby

 assume ( Rotate (a,r)) = 0 ;

 then

 A1: ( Rotate (a,r)) = ( 0 + ( 0 * ));

 per cases by A1, COMPLEX1: 77;

 suppose |.a.| = 0 ;

 hence a = 0 by COMPLEX1: 45;

 end;

 suppose ( cos (r + ( Arg a))) = 0 & ( sin (r + ( Arg a))) = 0 ;

 hence a = 0 by Th10;

 end;

 end;

 assume a = 0 ;

 hence thesis by COMPLEX1: 44;

 end;

 theorem :: COMPLEX2:53



 Th51: for a be Complex holds |.( Rotate (a,r)).| = |.a.|

 proof

 let a be Complex;

 ( Re ( Rotate (a,r))) = ( |.a.| * ( cos (r + ( Arg a)))) & ( Im ( Rotate (a,r))) = ( |.a.| * ( sin (r + ( Arg a)))) by COMPLEX1: 12;



 hence |.( Rotate (a,r)).| = ( sqrt ((( |.a.| * ( cos (r + ( Arg a)))) ^2 ) + (( |.a.| * ( sin (r + ( Arg a)))) ^2 ))) by COMPLEX1:def 12

 .= ( sqrt (( |.a.| ^2 ) * ((( cos (r + ( Arg a))) ^2 ) + (( sin (r + ( Arg a))) ^2 ))))

 .= ( sqrt (( |.a.| ^2 ) * 1)) by SIN_COS: 29

 .= |.a.| by COMPLEX1: 46, SQUARE_1: 22;

 end;

 theorem :: COMPLEX2:54



 Th52: for a be Complex st a <> 0 holds ex i be Integer st ( Arg ( Rotate (a,r))) = (((2 * PI ) * i) + (r + ( Arg a)))

 proof

 let a be Complex;



 A1: |.a.| = |.( Rotate (a,r)).| by Th51;

 assume a <> 0 ;

 then

 A2: ( Rotate (a,r)) <> 0c by Th50;

 take ( - [\((r + ( Arg a)) / (2 * PI ))/]);

 consider AR be Real such that

 A3: AR = (((2 * PI ) * ( - [\((r + ( Arg a)) / (2 * PI ))/])) + (r + ( Arg a))) and

 A4: 0 <= AR & AR < (2 * PI ) by Th1, COMPTRIG: 5;

 ( cos (r + ( Arg a))) = ( cos AR) & ( sin (r + ( Arg a))) = ( sin AR) by A3, Th8, Th9;

 hence thesis by A2, A1, A3, A4, COMPTRIG:def 1;

 end;

 theorem :: COMPLEX2:55

 ( Rotate (a,( - ( Arg a)))) = |.a.| by SIN_COS: 31;

 theorem :: COMPLEX2:56



 Th54: ( Re ( Rotate (a,r))) = ((( Re a) * ( cos r)) - (( Im a) * ( sin r))) & ( Im ( Rotate (a,r))) = ((( Re a) * ( sin r)) + (( Im a) * ( cos r)))

 proof

 a = (( |.a.| * ( cos ( Arg a))) + (( |.a.| * ( sin ( Arg a))) * )) by COMPTRIG: 62;

 then

 A1: ( Re a) = ( |.a.| * ( cos ( Arg a))) & ( Im a) = ( |.a.| * ( sin ( Arg a))) by COMPLEX1: 12;



 thus ( Re ( Rotate (a,r))) = ( |.a.| * ( cos (r + ( Arg a)))) by COMPLEX1: 12

 .= ( |.a.| * ((( cos r) * ( cos ( Arg a))) - (( sin r) * ( sin ( Arg a))))) by SIN_COS: 75

 .= ((( Re a) * ( cos r)) - (( Im a) * ( sin r))) by A1;



 thus ( Im ( Rotate (a,r))) = ( |.a.| * ( sin (r + ( Arg a)))) by COMPLEX1: 12

 .= ( |.a.| * ((( sin r) * ( cos ( Arg a))) + (( cos r) * ( sin ( Arg a))))) by SIN_COS: 75

 .= ((( Re a) * ( sin r)) + (( Im a) * ( cos r))) by A1;

 end;

 theorem :: COMPLEX2:57



 Th55: ( Rotate ((a + b),r)) = (( Rotate (a,r)) + ( Rotate (b,r)))

 proof

 set ab = (a + b);

 set rab = ( Rotate (ab,r)), ra = ( Rotate (a,r)), rb = ( Rotate (b,r));



 A1: ( Re ab) = (( Re a) + ( Re b)) & ( Im ab) = (( Im a) + ( Im b)) by COMPLEX1: 8;



 A2: ( Im rab) = ((( Re ab) * ( sin r)) + (( Im ab) * ( cos r))) by Th54;

 ( Im ra) = ((( Re a) * ( sin r)) + (( Im a) * ( cos r))) & ( Im rb) = ((( Re b) * ( sin r)) + (( Im b) * ( cos r))) by Th54;



 then

 A3: ( Im (ra + rb)) = (((( Re a) * ( sin r)) + (( Im a) * ( cos r))) + ((( Re b) * ( sin r)) + (( Im b) * ( cos r)))) by COMPLEX1: 8

 .= ( Im rab) by A2, A1;



 A4: ( Re rab) = ((( Re ab) * ( cos r)) - (( Im ab) * ( sin r))) by Th54;

 ( Re ra) = ((( Re a) * ( cos r)) - (( Im a) * ( sin r))) & ( Re rb) = ((( Re b) * ( cos r)) - (( Im b) * ( sin r))) by Th54;



 then ( Re (ra + rb)) = (((( Re a) * ( cos r)) - (( Im a) * ( sin r))) + ((( Re b) * ( cos r)) - (( Im b) * ( sin r)))) by COMPLEX1: 8

 .= ( Re rab) by A4, A1;

 hence thesis by A3, COMPLEX1: 3;

 end;

 theorem :: COMPLEX2:58



 Th56: ( Rotate (( - a),r)) = ( - ( Rotate (a,r)))

 proof

 per cases ;

 suppose

 A1: a <> 0c ;



 A2: ( cos (r + ( Arg ( - a)))) = ( - ( cos (r + ( Arg a)))) & ( sin (r + ( Arg ( - a)))) = ( - ( sin (r + ( Arg a))))

 proof

 per cases ;

 suppose ( Arg a) < PI ;

 then ( Arg ( - a)) = ( PI + ( Arg a)) by A1, Th12;

 then (r + ( Arg ( - a))) = ( PI + (r + ( Arg a)));

 hence thesis by SIN_COS: 79;

 end;

 suppose ( Arg a) >= PI ;

 then ( Arg ( - a)) = (( Arg a) - PI ) by A1, Th12;

 then (r + ( Arg ( - a))) = ((( Arg a) + r) - PI );

 hence thesis by Th5;

 end;

 end;

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by A2;

 end;

 suppose

 A3: a = 0c ;



 hence ( Rotate (( - a),r)) = ( - 0 ) by Th50

 .= ( - ( Rotate (a,r))) by A3, Th50;

 end;

 end;

 theorem :: COMPLEX2:59



 Th57: ( Rotate ((a - b),r)) = (( Rotate (a,r)) - ( Rotate (b,r)))

 proof



 thus ( Rotate ((a - b),r)) = (( Rotate (a,r)) + ( Rotate (( - b),r))) by Th55

 .= (( Rotate (a,r)) - ( Rotate (b,r))) by Th56;

 end;

 theorem :: COMPLEX2:60



 Th58: ( Rotate (a, PI )) = ( - a)

 proof



 A1: a = (( |.a.| * ( cos ( Arg a))) + (( |.a.| * ( sin ( Arg a))) * )) by COMPTRIG: 62;



 A2: ( |.a.| * ( - ( sin ( Arg a)))) = ( - ( |.a.| * ( sin ( Arg a))))

 .= ( - ( Im a)) by A1, COMPLEX1: 12;



 A3: ( |.a.| * ( - ( cos ( Arg a)))) = ( - ( |.a.| * ( cos ( Arg a))))

 .= ( - ( Re a)) by A1, COMPLEX1: 12;



 thus ( Rotate (a, PI )) = (( |.a.| * ( - ( cos ( Arg a)))) + (( |.a.| * ( sin ( PI + ( Arg a)))) * )) by SIN_COS: 79

 .= (( |.a.| * ( - ( cos ( Arg a)))) + (( |.a.| * ( - ( sin ( Arg a)))) * )) by SIN_COS: 79

 .= ( - a) by A3, A2, COMPLEX1: 83;

 end;

 begin

 definition

 let a,b be Complex;

 :: COMPLEX2:def3

 func angle (a,b) -> Real equals

 : Def3: ( Arg ( Rotate (b,( - ( Arg a))))) if ( Arg a) = 0 or b <> 0

 otherwise ((2 * PI ) - ( Arg a));

 correctness ;

 end

 theorem :: COMPLEX2:61



 Th59: for a be Complex holds r >= 0 implies ( angle (r,a)) = ( Arg a)

 proof

 let a be Complex;

 assume r >= 0 ;

 then ( Arg r) = 0 by COMPTRIG: 35;



 hence ( angle (r,a)) = ( Arg ( Rotate (a,( - 0 )))) by Def3

 .= ( Arg a) by COMPTRIG: 62;

 end;

 theorem :: COMPLEX2:62



 Th60: for a,b be Complex holds ( Arg a) = ( Arg b) & a <> 0 & b <> 0 implies ( Arg ( Rotate (a,r))) = ( Arg ( Rotate (b,r)))

 proof

 let a,b be Complex;

 assume that

 A1: ( Arg a) = ( Arg b) and

 A2: a <> 0 and

 A3: b <> 0 ;

 consider i be Integer such that

 A4: ( Arg ( Rotate (a,r))) = (((2 * PI ) * i) + (r + ( Arg a))) by A2, Th52;

 consider j be Integer such that

 A5: ( Arg ( Rotate (b,r))) = (((2 * PI ) * j) + (r + ( Arg b))) by A3, Th52;



 A6: 0 <= ( Arg ( Rotate (a,r))) & 0 <= ( Arg ( Rotate (b,r))) by COMPTRIG: 34;



 A7: ( Arg ( Rotate (a,r))) < (2 * PI ) & ( Arg ( Rotate (b,r))) < (2 * PI ) by COMPTRIG: 34;

 ( Arg ( Rotate (b,r))) = (((2 * PI ) * (j - i)) + ( Arg ( Rotate (a,r)))) by A1, A4, A5;

 hence thesis by A6, A7, Th2;

 end;

 theorem :: COMPLEX2:63



 Th61: r > 0 implies ( angle (a,b)) = ( angle ((a * r),(b * r)))

 proof

 assume

 A1: r > 0 ;

 then

 A2: ( Arg (a * r)) = ( Arg a) by Th25;

 per cases ;

 suppose

 A3: b <> 0 ;



 hence ( angle (a,b)) = ( Arg ( Rotate (b,( - ( Arg a))))) by Def3

 .= ( Arg ( Rotate ((b * r),( - ( Arg (a * r)))))) by A1, A2, A3, Th25, Th60

 .= ( angle ((a * r),(b * r))) by A1, A3, Def3;

 end;

 suppose

 A4: b = 0 ;

 thus thesis

 proof

 per cases ;

 suppose

 A5: ( Arg a) = 0 ;



 hence ( angle (a,b)) = ( Arg ( Rotate (b,( - ( Arg a))))) by Def3

 .= ( Arg 0c ) by A4, Th50

 .= ( Arg ( Rotate ((b * r),( - ( Arg (a * r)))))) by A4, Th50

 .= ( angle ((a * r),(b * r))) by A2, A5, Def3;

 end;

 suppose

 A6: ( Arg a) <> 0 ;



 hence ( angle (a,b)) = ((2 * PI ) - ( Arg a)) by A4, Def3

 .= ( angle ((a * r),(b * r))) by A2, A4, A6, Def3;

 end;

 end;

 end;

 end;

 theorem :: COMPLEX2:64



 Th62: a <> 0 & b <> 0 & ( Arg a) = ( Arg b) implies ( Arg ( - a)) = ( Arg ( - b))

 proof

 assume a <> 0 & b <> 0 & ( Arg a) = ( Arg b);

 then ( Arg ( Rotate (a, PI ))) = ( Arg ( Rotate (b, PI ))) by Th60;

 then ( Arg ( - a)) = ( Arg ( Rotate (b, PI ))) by Th58;

 hence thesis by Th58;

 end;

 theorem :: COMPLEX2:65



 Th63: a <> 0 & b <> 0 implies ( angle (a,b)) = ( angle (( Rotate (a,r)),( Rotate (b,r))))

 proof

 assume that

 A1: a <> 0 and

 A2: b <> 0 ;

 consider i be Integer such that

 A3: ( Arg ( Rotate (b,( - ( Arg a))))) = (((2 * PI ) * i) + (( - ( Arg a)) + ( Arg b))) by A2, Th52;

 consider l be Integer such that

 A4: ( Arg ( Rotate (b,r))) = (((2 * PI ) * l) + (r + ( Arg b))) by A2, Th52;

 consider k be Integer such that

 A5: ( Arg ( Rotate (a,r))) = (((2 * PI ) * k) + (r + ( Arg a))) by A1, Th52;



 A6: 0 <= ( Arg ( Rotate (( Rotate (b,r)),( - ( Arg ( Rotate (a,r))))))) & ( Arg ( Rotate (( Rotate (b,r)),( - ( Arg ( Rotate (a,r))))))) < (2 * PI ) by COMPTRIG: 34;



 A7: 0 <= ( Arg ( Rotate (b,( - ( Arg a))))) & ( Arg ( Rotate (b,( - ( Arg a))))) < (2 * PI ) by COMPTRIG: 34;



 A8: ( Rotate (b,r)) <> 0 by A2, Th50;

 then

 consider j be Integer such that

 A9: ( Arg ( Rotate (( Rotate (b,r)),( - ( Arg ( Rotate (a,r))))))) = (((2 * PI ) * j) + (( - ( Arg ( Rotate (a,r)))) + ( Arg ( Rotate (b,r))))) by Th52;



 A10: ( Arg ( Rotate (( Rotate (b,r)),( - ( Arg ( Rotate (a,r))))))) = (((2 * PI ) * (((j - k) + l) - i)) + ( Arg ( Rotate (b,( - ( Arg a)))))) by A3, A9, A5, A4;



 thus ( angle (a,b)) = ( Arg ( Rotate (b,( - ( Arg a))))) by A2, Def3

 .= ( Arg ( Rotate (( Rotate (b,r)),( - ( Arg ( Rotate (a,r))))))) by A10, A7, A6, Th2

 .= ( angle (( Rotate (a,r)),( Rotate (b,r)))) by A8, Def3;

 end;

 theorem :: COMPLEX2:66

 r < 0 & a <> 0 & b <> 0 implies ( angle (a,b)) = ( angle ((a * r),(b * r)))

 proof

 assume that

 A1: r < 0 and

 A2: a <> 0 and

 A3: b <> 0 ;

 consider i be Integer such that

 A4: ( Arg ( Rotate (( - b),( - ( Arg ( - a)))))) = (((2 * PI ) * i) + (( - ( Arg ( - a))) + ( Arg ( - b)))) by A3, Th52;

 set br = (b * r), ar = (a * r);

 ( Arg (b * r)) = ( Arg ( - b)) & ( Arg (a * r)) = ( Arg ( - a)) by A1, Th26;

 then

 consider j be Integer such that

 A5: ( Arg ( Rotate (br,( - ( Arg ar))))) = (((2 * PI ) * j) + (( - ( Arg ( - a))) + ( Arg ( - b)))) by A1, A3, Th52;



 A6: ( Arg ( Rotate (br,( - ( Arg ar))))) = (((2 * PI ) * (j - i)) + ( Arg ( Rotate (( - b),( - ( Arg ( - a))))))) by A4, A5;



 A7: 0 <= ( Arg ( Rotate (br,( - ( Arg ar))))) & ( Arg ( Rotate (br,( - ( Arg ar))))) < (2 * PI ) by COMPTRIG: 34;



 A8: 0 <= ( Arg ( Rotate (( - b),( - ( Arg ( - a)))))) & ( Arg ( Rotate (( - b),( - ( Arg ( - a)))))) < (2 * PI ) by COMPTRIG: 34;



 thus ( angle (a,b)) = ( angle (( Rotate (a, PI )),( Rotate (b, PI )))) by A2, A3, Th63

 .= ( angle (( - a),( Rotate (b, PI )))) by Th58

 .= ( angle (( - a),( - b))) by Th58

 .= ( Arg ( Rotate (( - b),( - ( Arg ( - a)))))) by A3, Def3

 .= ( Arg ( Rotate (br,( - ( Arg ar))))) by A6, A7, A8, Th2

 .= ( angle ((a * r),(b * r))) by A1, A3, Def3;

 end;

 theorem :: COMPLEX2:67

 a <> 0 & b <> 0 implies ( angle (a,b)) = ( angle (( - a),( - b)))

 proof

 assume a <> 0 & b <> 0 ;



 hence ( angle (a,b)) = ( angle (( Rotate (a, PI )),( Rotate (b, PI )))) by Th63

 .= ( angle (( - a),( Rotate (b, PI )))) by Th58

 .= ( angle (( - a),( - b))) by Th58;

 end;

 theorem :: COMPLEX2:68

 b <> 0 & ( angle (a,b)) = 0 implies ( angle (a,( - b))) = PI

 proof

 assume that

 A1: b <> 0 and

 A2: ( angle (a,b)) = 0 ;



 A3: ( Arg ( Rotate (b,( - ( Arg a))))) = 0 by A1, A2, Def3;



 A4: ( Arg ( Rotate (( - b),( - ( Arg a))))) = ( Arg ( - ( Rotate (b,( - ( Arg a)))))) by Th56;

 ( Rotate (b,( - ( Arg a)))) <> 0 by A1, Th50;



 then ( Arg ( - ( Rotate (b,( - ( Arg a)))))) = (( Arg ( Rotate (b,( - ( Arg a))))) + PI ) by A3, Th12, COMPTRIG: 5

 .= PI by A3;

 hence thesis by A1, A4, Def3;

 end;

 theorem :: COMPLEX2:69



 Th67: a <> 0 & b <> 0 implies ( cos ( angle (a,b))) = (( Re (a .|. b)) / ( |.a.| * |.b.|)) & ( sin ( angle (a,b))) = ( - (( Im (a .|. b)) / ( |.a.| * |.b.|)))

 proof

 assume that

 A1: a <> 0 and

 A2: b <> 0 ;



 A3: |.a.| <> 0 & |.b.| <> 0 by A1, A2, COMPLEX1: 45;

 set ra = ( Rotate (a,( - ( Arg a)))), rb = ( Rotate (b,( - ( Arg a)))), r = ( - ( Arg a));

 set mabi = (( |.a.| * |.b.|) " );



 A4: |.a.| >= 0 & |.b.| >= 0 by COMPLEX1: 46;

 ( angle (a,b)) = ( angle (ra,rb)) by A1, A2, Th63;



 then

 A5: ( angle (a,b)) = ( angle (( |.a.| * mabi),(rb * mabi))) by A3, A4, Th61, SIN_COS: 31

 .= ( Arg (rb * mabi)) by A4, Th59;



 A6: a = (( |.a.| * ( cos ( Arg a))) + (( |.a.| * ( sin ( Arg a))) * )) by COMPTRIG: 62;

 then ( Re a) = ( |.a.| * ( cos ( Arg a))) by COMPLEX1: 12;

 then

 A7: ( cos ( Arg a)) = (( Re a) / |.a.|) by A1, COMPLEX1: 45, XCMPLX_1: 89;

 ( Im a) = ( |.a.| * ( sin ( Arg a))) by A6, COMPLEX1: 12;

 then

 A8: ( sin ( Arg a)) = (( Im a) / |.a.|) by A1, COMPLEX1: 45, XCMPLX_1: 89;



 A9: (a .|. b) = (((( Re a) * ( Re b)) + (( Im a) * ( Im b))) + ((( - (( Re a) * ( Im b))) + (( Im a) * ( Re b))) * )) by Th27;

 then

 A10: ( Re (a .|. b)) = ((( Re a) * ( Re b)) + (( Im a) * ( Im b))) by COMPLEX1: 12;

 ( Re rb) = ((( Re b) * ( cos r)) - (( Im b) * ( sin r))) by Th54;



 then

 A11: ( Re rb) = ((( Re b) * ( cos r)) - (( Im b) * ( - ( sin ( Arg a))))) by SIN_COS: 31

 .= ((( Re b) * (( Re a) / |.a.|)) + (( Im b) * (( Im a) / |.a.|))) by A7, A8, SIN_COS: 31

 .= (( Re (a .|. b)) / |.a.|) by A10;



 A12: (( Im rb) ^2 ) >= 0 by XREAL_1: 63;

 ( Im rb) = ((( Re b) * ( sin r)) + (( Im b) * ( cos r))) by Th54;



 then

 A13: ( Im rb) = ((( Re b) * ( - ( sin ( Arg a)))) + (( Im b) * ( cos r))) by SIN_COS: 31

 .= ((( - ( Re b)) * (( Im a) / |.a.|)) + (( Im b) * (( Re a) / |.a.|))) by A7, A8, SIN_COS: 31

 .= ( - (( - ((( - ( Re b)) * ( Im a)) + (( Im b) * ( Re a)))) / |.a.|))

 .= ( - (( Im (a .|. b)) / |.a.|)) by A9, COMPLEX1: 12;

 set IT = (rb * mabi);

 set mab = ( |.a.| * |.b.|);



 A14: (mabi ^2 ) >= 0 & (( Re rb) ^2 ) >= 0 by XREAL_1: 63;

 mabi = (mabi + ( 0 * ));

 then

 A15: ( Re mabi) = mabi & ( Im mabi) = 0 by COMPLEX1: 12;



 then

 A16: ( Re IT) = ((( Re rb) * mabi) - (( Im rb) * 0 )) by COMPLEX1: 9

 .= (( Re rb) * mabi);



 A17: ( Im IT) = ((( Re rb) * 0 ) + (( Im rb) * mabi)) by A15, COMPLEX1: 9

 .= (( Im rb) * mabi);



 then

 A18: |.IT.| = ( sqrt (((( Re rb) * mabi) ^2 ) + ((( Im rb) * mabi) ^2 ))) by A16, COMPLEX1:def 12

 .= ( sqrt ((mabi ^2 ) * ((( Re rb) ^2 ) + (( Im rb) ^2 ))))

 .= (( sqrt (mabi ^2 )) * ( sqrt ((( Re rb) ^2 ) + (( Im rb) ^2 )))) by A14, A12, SQUARE_1: 29

 .= (mabi * ( sqrt ((( Re rb) ^2 ) + (( Im rb) ^2 )))) by A4, SQUARE_1: 22

 .= (mabi * |.rb.|) by COMPLEX1:def 12

 .= (mabi * |.b.|) by Th51;



 A19: IT = (( |.IT.| * ( cos ( Arg IT))) + (( |.IT.| * ( sin ( Arg IT))) * )) by COMPTRIG: 62;

 then ( |.IT.| * ( cos ( Arg IT))) = (( Re rb) * mabi) by A16, COMPLEX1: 12;



 hence ( cos ( angle (a,b))) = ((( Re rb) * mabi) / |.IT.|) by A3, A5, A18, XCMPLX_1: 89

 .= (( Re rb) * (mabi / |.IT.|))

 .= ((( Re (a .|. b)) / |.a.|) * ((mabi / mabi) / |.b.|)) by A11, A18, XCMPLX_1: 78

 .= ((( Re (a .|. b)) / |.a.|) * (1 / |.b.|)) by A3, XCMPLX_1: 60

 .= ((( Re (a .|. b)) * 1) / ( |.a.| * |.b.|)) by XCMPLX_1: 76

 .= (( Re (a .|. b)) / mab);

 ( |.IT.| * ( sin ( Arg IT))) = (( Im rb) * mabi) by A19, A17, COMPLEX1: 12;



 hence ( sin ( angle (a,b))) = ((( Im rb) * mabi) / |.IT.|) by A3, A5, A18, XCMPLX_1: 89

 .= (( Im rb) * (mabi / |.IT.|))

 .= (( - (( Im (a .|. b)) / |.a.|)) * ((mabi / mabi) / |.b.|)) by A13, A18, XCMPLX_1: 78

 .= ((( - ( Im (a .|. b))) / |.a.|) * (1 / |.b.|)) by A3, XCMPLX_1: 60

 .= ((( - ( Im (a .|. b))) * 1) / ( |.a.| * |.b.|)) by XCMPLX_1: 76

 .= ( - (( Im (a .|. b)) / mab));

 end;

 definition

 let x,y,z be Complex;

 :: COMPLEX2:def4

 func angle (x,y,z) -> Real equals

 : Def4: (( Arg (z - y)) - ( Arg (x - y))) if (( Arg (z - y)) - ( Arg (x - y))) >= 0

 otherwise ((2 * PI ) + (( Arg (z - y)) - ( Arg (x - y))));

 correctness ;

 end

 theorem :: COMPLEX2:70



 Th68: 0 <= ( angle (x,y,z)) & ( angle (x,y,z)) < (2 * PI )

 proof

 now

 per cases ;

 case

 A1: (( Arg (z - y)) - ( Arg (x - y))) >= 0 ;

 ( Arg (x - y)) >= 0 by COMPTRIG: 34;

 then (( Arg (z - y)) + 0 ) <= (( Arg (z - y)) + ( Arg (x - y))) by XREAL_1: 7;

 then

 A2: ( Arg (z - y)) < (2 * PI ) & (( Arg (z - y)) - ( Arg (x - y))) <= ( Arg (z - y)) by COMPTRIG: 34, XREAL_1: 20;

 ( angle (x,y,z)) = (( Arg (z - y)) - ( Arg (x - y))) by A1, Def4;

 hence thesis by A1, A2, XXREAL_0: 2;

 end;

 case

 A3: (( Arg (z - y)) - ( Arg (x - y))) < 0 ;

 ( Arg (z - y)) >= 0 by COMPTRIG: 34;

 then (( Arg (x - y)) + 0 ) <= (( Arg (x - y)) + ( Arg (z - y))) by XREAL_1: 7;

 then ( Arg (x - y)) < (2 * PI ) & (( Arg (x - y)) - ( Arg (z - y))) <= ( Arg (x - y)) by COMPTRIG: 34, XREAL_1: 20;

 then (( Arg (x - y)) - ( Arg (z - y))) < (2 * PI ) by XXREAL_0: 2;

 then

 A4: ((2 * PI ) - (( Arg (x - y)) - ( Arg (z - y)))) > 0 by XREAL_1: 50;

 ((( Arg (z - y)) - ( Arg (x - y))) + (2 * PI )) < ( 0 + (2 * PI )) by A3, XREAL_1: 8;

 hence thesis by A3, A4, Def4;

 end;

 end;

 hence thesis;

 end;

 theorem :: COMPLEX2:71



 Th69: ( angle (x,y,z)) = ( angle ((x - y), 0 ,(z - y)))

 proof

 now

 per cases ;

 case

 A1: (( Arg ((z - y) - 0c )) - ( Arg ((x - y) - 0c ))) >= 0 ;

 then ( angle ((x - y), 0c ,(z - y))) = (( Arg (z - y)) - ( Arg (x - y))) by Def4;

 hence ( angle ((x - y), 0c ,(z - y))) = ( angle (x,y,z)) by A1, Def4;

 end;

 case

 A2: (( Arg ((z - y) - 0c )) - ( Arg ((x - y) - 0c ))) < 0 ;

 then ( angle ((x - y), 0c ,(z - y))) = ((2 * PI ) + (( Arg (z - y)) - ( Arg (x - y)))) by Def4;

 hence ( angle ((x - y), 0c ,(z - y))) = ( angle (x,y,z)) by A2, Def4;

 end;

 end;

 hence thesis;

 end;

 theorem :: COMPLEX2:72



 Th70: ( angle (a,b,c)) = ( angle ((a + d),(b + d),(c + d)))

 proof



 thus ( angle (a,b,c)) = ( angle ((a - b), 0c ,(c - b))) by Th69

 .= ( angle (((a + d) - (b + d)), 0c ,((c + d) - (b + d))))

 .= ( angle ((a + d),(b + d),(c + d))) by Th69;

 end;

 theorem :: COMPLEX2:73



 Th71: ( angle (a,b)) = ( angle (a, 0 ,b))

 proof

 set ab2 = ( angle (a,b));



 A1: 0 <= ( Arg ( Rotate (b,( - ( Arg a))))) & ( Arg ( Rotate (b,( - ( Arg a))))) < (2 * PI ) by COMPTRIG: 34;

 per cases ;

 suppose

 A2: b <> 0 ;

 then

 A3: ab2 = ( Arg ( Rotate (b,( - ( Arg a))))) by Def3;

 thus thesis

 proof

 per cases ;

 suppose (( Arg (b - 0c )) - ( Arg (a - 0c ))) >= 0 ;

 then

 A4: ( angle (a, 0c ,b)) = (( - ( Arg a)) + ( Arg b)) by Def4;



 A5: ( angle (a, 0c ,b)) < (2 * PI ) by Th68;

 (ex i be Integer st ( Arg ( Rotate (b,( - ( Arg a))))) = (((2 * PI ) * i) + (( - ( Arg a)) + ( Arg b)))) & 0 <= ( angle (a, 0c ,b)) by A2, Th52, Th68;

 hence thesis by A1, A3, A4, A5, Th2;

 end;

 suppose

 A6: (( Arg (b - 0c )) - ( Arg (a - 0c ))) < 0 ;

 consider i be Integer such that

 A7: ( Arg ( Rotate (b,( - ( Arg a))))) = (((2 * PI ) * i) + (( - ( Arg a)) + ( Arg b))) by A2, Th52;



 A8: (((2 * PI ) * i) + (( - ( Arg a)) + ( Arg b))) = (((2 * PI ) * (i - 1)) + ((2 * PI ) + (( - ( Arg a)) + ( Arg b))));



 A9: ( angle (a, 0c ,b)) = ((2 * PI ) + (( Arg b) + ( - ( Arg a)))) by A6, Def4;

 then 0 <= ((2 * PI ) + (( - ( Arg a)) + ( Arg b))) & ((2 * PI ) + (( - ( Arg a)) + ( Arg b))) < (2 * PI ) by Th68;

 hence thesis by A1, A3, A9, A7, A8, Th2;

 end;

 end;

 end;

 suppose

 A10: b = 0 ;

 thus thesis

 proof

 per cases ;

 suppose

 A11: ( Arg a) = 0 ;

 then

 A12: (( Arg (b - 0c )) - ( Arg (a - 0c ))) = 0 by A10, COMPTRIG: 35;

 ab2 = ( Arg ( Rotate (b,( - ( Arg a))))) by A11, Def3

 .= 0 by A10, Lm1, Th50;

 hence thesis by A12, Def4;

 end;

 suppose

 A13: ( Arg a) <> 0 ;

 then

 A14: 0 < ( - ( - ( Arg a))) by COMPTRIG: 34;

 (( Arg (b - 0c )) - ( Arg (a - 0c ))) = ( - ( Arg a)) by A10, Lm1;

 then ( angle (a, 0c ,b)) = ((2 * PI ) - ( Arg a)) by A14, Def4;

 hence thesis by A10, A13, Def3;

 end;

 end;

 end;

 end;

 theorem :: COMPLEX2:74



 Th72: ( angle (x,y,z)) = 0 implies ( Arg (x - y)) = ( Arg (z - y)) & ( angle (z,y,x)) = 0

 proof

 assume

 A1: ( angle (x,y,z)) = 0 ;

 now

 per cases ;

 case (( Arg (z - y)) - ( Arg (x - y))) >= 0 ;

 then (( Arg (z - y)) - ( Arg (x - y))) = 0 by A1, Def4;

 hence thesis by Def4;

 end;

 case

 A2: (( Arg (z - y)) - ( Arg (x - y))) < 0 ;

 then ( - (( Arg (z - y)) - ( Arg (x - y)))) > 0 ;

 then

 A3: ( angle (z,y,x)) = (( Arg (x - y)) - ( Arg (z - y))) by Def4;

 ( angle (x,y,z)) = ((2 * PI ) + (( Arg (z - y)) - ( Arg (x - y)))) by A2, Def4;

 hence contradiction by A1, A3, Th68;

 end;

 end;

 hence thesis;

 end;

 theorem :: COMPLEX2:75



 Th73: a <> 0 & b <> 0 implies (( Re (a .|. b)) = 0 iff ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI ))

 proof



 A1: ( - (( Im (a .|. b)) / ( |.a.| * |.b.|))) = (( - ( Im (a .|. b))) / ( |.a.| * |.b.|));

 assume

 A2: a <> 0 & b <> 0 ;

 then

 A3: |.a.| <> 0 & |.b.| <> 0 by COMPLEX1: 45;



 A4: ( angle (a,b)) = ( angle (a, 0c ,b)) & 0 <= ( angle (a, 0c ,b)) by Th68, Th71;



 A5: ( angle (a, 0c ,b)) < (2 * PI ) & ( PI / 2) < (2 * PI ) by Th68, COMPTRIG: 5, XXREAL_0: 2;



 A6: ( cos ( angle (a,b))) = (( Re (a .|. b)) / ( |.a.| * |.b.|)) by A2, Th67;



 A7: ( sin ( angle (a,b))) = ( - (( Im (a .|. b)) / ( |.a.| * |.b.|))) by A2, Th67;

 hereby

 assume

 A8: ( Re (a .|. b)) = 0 ;

 then ( Im (a .|. b)) = ( |.a.| * |.b.|) or ( Im (a .|. b)) = ( - ( |.a.| * |.b.|)) by Th48;

 then ( sin ( angle (a,b))) = 1 or ( sin ( angle (a,b))) = ( - 1) by A7, A3, A1, XCMPLX_1: 60;

 hence ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI ) by A6, A4, A5, A8, Th11, COMPTRIG: 5, SIN_COS: 77;

 end;

 assume ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI );

 hence thesis by A6, A3, Th71, SIN_COS: 77;

 end;

 theorem :: COMPLEX2:76

 a <> 0 & b <> 0 implies (( Im (a .|. b)) = ( |.a.| * |.b.|) or ( Im (a .|. b)) = ( - ( |.a.| * |.b.|)) iff ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI ))

 proof

 assume

 A1: a <> 0 & b <> 0 ;

 hereby

 assume ( Im (a .|. b)) = ( |.a.| * |.b.|) or ( Im (a .|. b)) = ( - ( |.a.| * |.b.|));

 then ( Re (a .|. b)) = 0 by Th48;

 hence ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI ) by A1, Th73;

 end;

 hereby

 assume ( angle (a, 0 ,b)) = ( PI / 2) or ( angle (a, 0 ,b)) = ((3 / 2) * PI );

 then ( Re (a .|. b)) = 0 by A1, Th73;

 hence ( Im (a .|. b)) = ( |.a.| * |.b.|) or ( Im (a .|. b)) = ( - ( |.a.| * |.b.|)) by Th48;

 end;

 end;



 Lm3: for a,b,c be Complex st a <> b & c <> b holds ( Re ((a - b) .|. (c - b))) = 0 iff ( angle (a,b,c)) = ( PI / 2) or ( angle (a,b,c)) = ((3 / 2) * PI )

 proof

 let x,y,z be Complex;

 assume x <> y & z <> y;

 then

 A1: (x - y) <> 0c & (z - y) <> 0c ;

 ( angle (x,y,z)) = ( angle ((x - y), 0c ,(z - y))) by Th69;

 hence thesis by A1, Th73;

 end;

 theorem :: COMPLEX2:77

 x <> y & z <> y & (( angle (x,y,z)) = ( PI / 2) or ( angle (x,y,z)) = ((3 / 2) * PI )) implies (( |.(x - y).| ^2 ) + ( |.(z - y).| ^2 )) = ( |.(x - z).| ^2 )

 proof

 assume

 A1: x <> y & z <> y & (( angle (x,y,z)) = ( PI / 2) or ( angle (x,y,z)) = ((3 / 2) * PI ));

 set x3 = (x - z);



 A2: (( |.(x - y).| ^2 ) + ( |.(z - y).| ^2 )) = (( Re ((x - y) .|. (x - y))) + ( |.(z - y).| ^2 )) by Th29

 .= (( Re ((x - y) .|. (x - y))) + ( Re ((z - y) .|. (z - y)))) by Th29

 .= ( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) by COMPLEX1: 8;

 x3 = ((x - y) - (z - y));

 then ((x - z) .|. (x - z)) = (((((x - y) .|. (x - y)) - ((x - y) .|. (z - y))) - ((z - y) .|. (x - y))) + ((z - y) .|. (z - y))) by Th47;



 then ( Re ((x - z) .|. (x - z))) = ( Re ((((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) - (((x - y) .|. (z - y)) + ((z - y) .|. (x - y)))))

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ( Re (((x - y) .|. (z - y)) + ((z - y) .|. (x - y))))) by COMPLEX1: 19

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (( Re ((x - y) .|. (z - y))) + ( Re ((z - y) .|. (x - y))))) by COMPLEX1: 8

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (( Re ((x - y) .|. (z - y))) + ( Re (((x - y) .|. (z - y)) *' )))) by Th32

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (( Re ((x - y) .|. (z - y))) + ( Re ((x - y) .|. (z - y))))) by COMPLEX1: 27

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ( 0 + ( Re ((x - y) .|. (z - y))))) by A1, Lm3

 .= (( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - 0 ) by A1, Lm3

 .= ( Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y))));

 hence thesis by A2, Th29;

 end;

 theorem :: COMPLEX2:78



 Th76: a <> b & b <> c implies ( angle (a,b,c)) = ( angle (( Rotate (a,r)),( Rotate (b,r)),( Rotate (c,r))))

 proof

 set cb = (c - b), ab = (a - b);

 set rc = ( Rotate (c,r)), rb = ( Rotate (b,r)), ra = ( Rotate (a,r));

 set rcb = (( Rotate (c,r)) - ( Rotate (b,r))), rab = (( Rotate (a,r)) - ( Rotate (b,r)));

 assume that

 A1: a <> b and

 A2: b <> c;



 A3: 0 <= ( angle (a,b,c)) & ( angle (a,b,c)) < (2 * PI ) by Th68;

 cb <> 0 by A2;

 then

 consider cbi be Integer such that

 A4: ( Arg ( Rotate (cb,r))) = (((2 * PI ) * cbi) + (r + ( Arg cb))) by Th52;

 ab <> 0 by A1;

 then

 consider abi be Integer such that

 A5: ( Arg ( Rotate (ab,r))) = (((2 * PI ) * abi) + (r + ( Arg ab))) by Th52;



 A6: 0 <= ( angle (( Rotate (a,r)),( Rotate (b,r)),( Rotate (c,r)))) & ( angle (( Rotate (a,r)),( Rotate (b,r)),( Rotate (c,r)))) < (2 * PI ) by Th68;

 rab = ( Rotate (ab,r)) by Th57;



 then

 A7: (( Arg rcb) - ( Arg rab)) = (((((2 * PI ) * cbi) + r) + ( Arg cb)) - ((((2 * PI ) * abi) + r) + ( Arg ab))) by A5, A4, Th57

 .= ((( Arg cb) - ( Arg ab)) + ((2 * PI ) * (cbi - abi)));

 per cases ;

 suppose (( Arg (c - b)) - ( Arg (a - b))) >= 0 ;

 then

 A8: ( angle (a,b,c)) = (( Arg (c - b)) - ( Arg (a - b))) by Def4;

 thus ( angle (a,b,c)) = ( angle (( Rotate (a,r)),( Rotate (b,r)),( Rotate (c,r))))

 proof

 per cases ;

 suppose (( Arg rcb) - ( Arg rab)) >= 0 ;

 then ( angle (ra,rb,rc)) = (( Arg rcb) - ( Arg rab)) by Def4;

 hence thesis by A3, A6, A7, A8, Th2;

 end;

 suppose (( Arg rcb) - ( Arg rab)) < 0 ;



 then ( angle (ra,rb,rc)) = (((( Arg cb) - ( Arg ab)) + ((2 * PI ) * (cbi - abi))) + (2 * PI )) by A7, Def4

 .= ((( Arg cb) - ( Arg ab)) + ((2 * PI ) * ((cbi - abi) + 1)));

 hence thesis by A3, A6, A8, Th2;

 end;

 end;

 end;

 suppose (( Arg cb) - ( Arg ab)) < 0 ;

 then

 A9: ( angle (a,b,c)) = ((2 * PI ) + (( Arg cb) - ( Arg ab))) by Def4;

 thus thesis

 proof

 per cases ;

 suppose (( Arg rcb) - ( Arg rab)) >= 0 ;

 then ( angle (ra,rb,rc)) = (((2 * PI ) + (( Arg cb) - ( Arg ab))) + ((2 * PI ) * ((cbi - abi) + ( - 1)))) by A7, Def4;

 hence thesis by A3, A6, A9, Th2;

 end;

 suppose (( Arg rcb) - ( Arg rab)) < 0 ;



 then ( angle (ra,rb,rc)) = (((( Arg cb) - ( Arg ab)) + ((2 * PI ) * (cbi - abi))) + (2 * PI )) by A7, Def4

 .= (((2 * PI ) + (( Arg cb) - ( Arg ab))) + ((2 * PI ) * (cbi - abi)));

 hence thesis by A3, A6, A9, Th2;

 end;

 end;

 end;

 end;

 theorem :: COMPLEX2:79



 Th77: ( angle (a,b,a)) = 0

 proof

 (( Arg (a - b)) - ( Arg (a - b))) = 0 ;

 hence thesis by Def4;

 end;



 Lm4: ( angle (x,y,z)) <> 0 implies ( angle (z,y,x)) = ((2 * PI ) - ( angle (x,y,z)))

 proof

 assume

 A1: ( angle (x,y,z)) <> 0 ;

 now

 per cases ;

 case

 A2: (( Arg (x - y)) - ( Arg (z - y))) > 0 ;

 then ( - ( - (( Arg (x - y)) - ( Arg (z - y))))) > 0 ;



 then ( angle (x,y,z)) = ((2 * PI ) + (( Arg (z - y)) - ( Arg (x - y)))) by Def4

 .= ((2 * PI ) - (( Arg (x - y)) - ( Arg (z - y))));

 hence thesis by A2, Def4;

 end;

 case

 A3: (( Arg (x - y)) - ( Arg (z - y))) <= 0 ;

 (( Arg (x - y)) - ( Arg (z - y))) <> 0 by A1, Def4;

 then

 A4: ( angle (z,y,x)) = ((2 * PI ) - (( Arg (z - y)) - ( Arg (x - y)))) by A3, Def4;

 ( - ( - (( Arg (x - y)) - ( Arg (z - y))))) <= 0 by A3;



 then (( angle (x,y,z)) + ( angle (z,y,x))) = (((2 * PI ) - (( Arg (z - y)) - ( Arg (x - y)))) + (( Arg (z - y)) - ( Arg (x - y)))) by A4, Def4

 .= (2 * PI );

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 theorem :: COMPLEX2:80



 Th78: ( angle (a,b,c)) <> 0 iff (( angle (a,b,c)) + ( angle (c,b,a))) = (2 * PI )

 proof

 hereby

 assume ( angle (a,b,c)) <> 0 ;

 then ( angle (c,b,a)) = ((2 * PI ) - ( angle (a,b,c))) by Lm4;

 hence (( angle (a,b,c)) + ( angle (c,b,a))) = (2 * PI );

 end;

 assume (( angle (a,b,c)) + ( angle (c,b,a))) = (2 * PI ) & ( angle (a,b,c)) = 0 ;

 hence contradiction by Th68;

 end;

 theorem :: COMPLEX2:81

 ( angle (a,b,c)) <> 0 implies ( angle (c,b,a)) <> 0

 proof

 assume ( angle (a,b,c)) <> 0 ;

 then

 A1: (( angle (a,b,c)) + ( angle (c,b,a))) = (2 * PI ) by Th78;

 assume not thesis;

 hence contradiction by A1, Th68;

 end;

 theorem :: COMPLEX2:82

 ( angle (a,b,c)) = PI implies ( angle (c,b,a)) = PI

 proof

 assume

 A1: ( angle (a,b,c)) = PI ;

 then (( angle (a,b,c)) + ( angle (c,b,a))) = ( 0 + (2 * PI )) by Th78, COMPTRIG: 5;

 hence thesis by A1;

 end;

 theorem :: COMPLEX2:83



 Th81: a <> b & a <> c & b <> c implies ( angle (a,b,c)) <> 0 or ( angle (b,c,a)) <> 0 or ( angle (c,a,b)) <> 0

 proof

 assume that

 A1: a <> b & a <> c and

 A2: b <> c;



 A3: (b - a) <> 0 & (a - c) <> 0 by A1;

 (c - b) <> 0 by A2;

 then

 A4: ( Arg (c - b)) < PI iff ( Arg ( - (c - b))) >= PI by Th14;



 A5: ( - (b - a)) = (a - b) & ( - (a - c)) = (c - a);



 A6: ( - (c - a)) = (a - c);

 assume

 A7: not thesis;

 then

 A8: ( Arg (a - c)) = ( Arg (b - c)) by Th72;

 ( Arg (b - a)) = ( Arg (c - a)) by A7, Th72;

 then ( Arg (a - b)) = ( Arg (a - c)) by A3, A5, A6, Th62;

 hence thesis by A7, A8, A4, Th72;

 end;



 Lm5: ( Im a) = 0 & ( Re a) > 0 & 0 < ( Arg b) & ( Arg b) < PI implies ((( angle (a, 0c ,b)) + ( angle ( 0c ,b,a))) + ( angle (b,a, 0c ))) = PI & 0 < ( angle ( 0c ,b,a)) & 0 < ( angle (b,a, 0c ))

 proof

 assume that

 A1: ( Im a) = 0 and

 A2: ( Re a) > 0 and

 A3: 0 < ( Arg b) and

 A4: ( Arg b) < PI ;

 a = (( Re a) + ( 0 * )) by A1, COMPLEX1: 13;

 then

 A5: ( Arg a) = 0 by A2, COMPTRIG: 35;



 then

 A6: (( Arg a) - ( Arg ( - a))) = (( Arg a) - (( Arg a) + PI )) by A2, Th12, COMPLEX1: 4, COMPTRIG: 5

 .= ( - PI );

 (( Arg (b - 0c )) - ( Arg (a - 0c ))) >= 0 by A3, A5;

 then

 A7: ( angle (a, 0c ,b)) = (( Arg b) - ( Arg a)) by Def4;

 ( Arg b) in ]. 0 , PI .[ by A3, A4, XXREAL_1: 4;

 then

 A8: ( Im b) > 0 by Th16;



 then

 A9: (( Arg b) - ( Arg ( - b))) = (( Arg b) - (( Arg b) + PI )) by A4, Th12, COMPLEX1: 4

 .= ( - PI );



 A10: ( Im (a - b)) = (( Im a) - ( Im b)) by COMPLEX1: 19

 .= ( - ( Im b)) by A1;

 then

 A11: ( Arg (a - b)) > PI by A8, Th22;

 then ( Arg (b - a)) <= PI by A8, A10, Th15, COMPLEX1: 4;

 then

 A12: ( - ( Arg (b - a))) >= ( - PI ) by XREAL_1: 24;



 A13: (( Arg (a - b)) - ( Arg (b - a))) = (( Arg (a - b)) - ( Arg ( - (a - b))))

 .= (( Arg (a - b)) - (( Arg (a - b)) - PI )) by A8, A10, A11, Th12, COMPLEX1: 4

 .= PI ;

 ( Arg ( - a)) = (( Arg a) + PI ) by A2, A5, Th12, COMPLEX1: 4, COMPTRIG: 5

 .= PI by A5;

 then (( Arg ( - a)) + ( - ( Arg (b - a)))) >= (( 0 - PI ) + PI ) by A12, XREAL_1: 7;

 then

 A14: ( angle (b,a, 0c )) = (( Arg ( 0c - a)) - ( Arg (b - a))) by Def4;

 now

 let a,b be Complex such that

 A15: ( Im a) = 0 and

 A16: ( Re a) > 0 and

 A17: 0 < ( Arg b) & ( Arg b) < PI ;



 A18: (( Re b) + ( - ( Re a))) < (( Re b) + 0 ) by A16, XREAL_1: 8;

 set ba = (b - a);

 set B = ( Arg b), BA = ( Arg ba), mb = |.b.|, mba = |.(b - a).|;



 A19: ( Re (b - a)) = (( Re b) - ( Re a)) by COMPLEX1: 19;

 (b - a) = ((mba * ( cos BA)) + ((mba * ( sin BA)) * )) & (b - a) = (( Re ba) + (( Im ba) * )) by COMPTRIG: 62, COMPLEX1: 13;

 then

 A20: ( Im ba) = (mba * ( sin BA)) by COMPLEX1: 77;

 set Rb = ( Re b), Rba = ( Re ba), Ib = ( Im b), Iba = ( Im ba);



 A21: ( Im (b - a)) = (( Im b) - ( Im a)) by COMPLEX1: 19

 .= ( Im b) by A15;

 then

 A22: mb = ( sqrt ((Rb ^2 ) + (Ib ^2 ))) & mba = ( sqrt ((Rba ^2 ) + (Ib ^2 ))) by COMPLEX1:def 12;



 A23: (Rb ^2 ) >= 0 & (Ib ^2 ) >= 0 by XREAL_1: 63;



 A24: (Rba ^2 ) >= 0 & (Ib ^2 ) >= 0 by XREAL_1: 63;

 ( Arg b) in ]. 0 , PI .[ by A17, XXREAL_1: 4;

 then

 A25: ( Im b) > 0 by Th16;

 then

 A26: mb >= 0 by COMPLEX1: 4, COMPLEX1: 47;



 A27: mba >= 0 by A25, A21, COMPLEX1: 4, COMPLEX1: 47;



 A28: ( sin BA) > 0 by A25, A21, COMPTRIG: 45;



 A29: mb <> 0 by A25, COMPLEX1: 4, COMPLEX1: 47;

 b = ((mb * ( cos B)) + ((mb * ( sin B)) * )) & b = (( Re b) + (( Im b) * )) by COMPTRIG: 62, COMPLEX1: 13;

 then ( Im b) = (mb * ( sin B)) by COMPLEX1: 77;

 then

 A30: (mba / mb) = (( sin B) / ( sin BA)) by A21, A20, A29, A28, XCMPLX_1: 94;

 per cases ;

 suppose

 A31: 0 < ( Re ba);

 then (Rb ^2 ) > (Rba ^2 ) by A19, A18, SQUARE_1: 16;

 then ((Rb ^2 ) + (Ib ^2 )) > ((Rba ^2 ) + (Ib ^2 )) by XREAL_1: 8;

 then mb > mba by A22, A24, SQUARE_1: 27;

 then (mba / mb) < 1 by A27, XREAL_1: 189;

 then ((( sin B) / ( sin BA)) * ( sin BA)) < (1 * ( sin BA)) by A28, A30, XREAL_1: 68;

 then

 A32: ( sin B) < (1 * ( sin BA)) by A28, XCMPLX_1: 87;

 B in ]. 0 , ( PI / 2).[ & BA in ]. 0 , ( PI / 2).[ by A25, A21, A19, A18, A31, COMPTRIG: 41;

 then BA > B by A32, Th6;

 then (BA + ( - B)) > (B + ( - B)) by XREAL_1: 8;

 hence (( Arg ba) - ( Arg b)) > 0 ;

 end;

 suppose

 A33: 0 = Rba;

 then ba = ( 0 + (Iba * )) by COMPLEX1: 13;

 then

 A34: BA = ( PI / 2) by A25, A21, COMPTRIG: 37;

 B in ]. 0 , ( PI / 2).[ by A16, A25, A19, A33, COMPTRIG: 41;

 then B < BA by A34, XXREAL_1: 4;

 then (B + ( - B)) < (BA + ( - B)) by XREAL_1: 8;

 hence (( Arg ba) - ( Arg b)) > 0 ;

 end;

 suppose

 A35: 0 > ( Re ba);

 thus (( Arg ba) - ( Arg b)) > 0

 proof

 per cases ;

 suppose 0 < ( Re b);

 then B in ]. 0 , ( PI / 2).[ by A25, COMPTRIG: 41;

 then

 A36: B < ( PI / 2) by XXREAL_1: 4;

 BA in ].( PI / 2), PI .[ by A25, A21, A35, COMPTRIG: 42;

 then BA > ( PI / 2) by XXREAL_1: 4;

 then BA > B by A36, XXREAL_0: 2;

 then (B + ( - B)) < (BA + ( - B)) by XREAL_1: 8;

 hence thesis;

 end;

 suppose 0 = ( Re b);

 then b = ( 0 + (Ib * )) by COMPLEX1: 13;

 then

 A37: B = ( PI / 2) by A25, COMPTRIG: 37;

 BA in ].( PI / 2), PI .[ by A25, A21, A35, COMPTRIG: 42;

 then B < BA by A37, XXREAL_1: 4;

 then (B + ( - B)) < (BA + ( - B)) by XREAL_1: 8;

 hence thesis;

 end;

 suppose

 A38: 0 > ( Re b);

 then (Rb ^2 ) < (Rba ^2 ) by A19, A18, SQUARE_1: 44;

 then ((Rb ^2 ) + (Ib ^2 )) < ((Rba ^2 ) + (Ib ^2 )) by XREAL_1: 8;

 then mb < mba by A22, A23, SQUARE_1: 27;

 then (mba / mb) > 1 by A26, A29, XREAL_1: 187;

 then ((( sin B) / ( sin BA)) * ( sin BA)) > (1 * ( sin BA)) by A28, A30, XREAL_1: 68;

 then

 A39: ( sin B) > (1 * ( sin BA)) by A28, XCMPLX_1: 87;



 A40: B in ].( PI / 2), PI .[ by A25, A38, COMPTRIG: 42;

 BA in ].( PI / 2), PI .[ by A25, A21, A35, COMPTRIG: 42;

 then BA > B by A40, A39, Th7;

 then (BA + ( - B)) > (B + ( - B)) by XREAL_1: 8;

 hence thesis;

 end;

 end;

 end;

 end;

 then (( Arg (b - a)) - ( Arg b)) > 0 by A1, A2, A3, A4;

 then (( Arg ( - (a - b))) - ( Arg b)) > 0 ;

 then ((( Arg (a - b)) - PI ) - ( Arg b)) > 0 by A8, A10, A11, Th12, COMPLEX1: 4;

 then

 A41: (( Arg (a - b)) - (( Arg b) + PI )) > 0 ;

 then (( Arg (a - b)) - ( Arg ( - b))) > 0 by A4, A8, Th12, COMPLEX1: 4;

 then ( angle ( 0c ,b,a)) = (( Arg (a - b)) - ( Arg ( 0c - b))) by Def4;



 hence ((( angle (a, 0c ,b)) + ( angle ( 0c ,b,a))) + ( angle (b,a, 0c ))) = ((((( Arg b) - ( Arg ( - b))) - ( Arg a)) + ( Arg (a - b))) + (( Arg ( - a)) - ( Arg (b - a)))) by A7, A14

 .= PI by A9, A6, A13;

 (( Arg (a - b)) - ( Arg ( 0c - b))) > 0 by A4, A8, A41, Th12, COMPLEX1: 4;

 hence 0 < ( angle ( 0c ,b,a)) by Def4;



 A42: ( Arg a) >= 0 by COMPTRIG: 34;

 (2 * PI ) > ( 0 + ( Arg (a - b))) by COMPTRIG: 34;

 then

 A43: ((2 * PI ) - ( Arg (a - b))) > 0 by XREAL_1: 20;

 (( Arg ( - a)) - (( Arg (a - b)) - PI )) = (( Arg a) + ((2 * PI ) - ( Arg (a - b)))) by A6;

 hence thesis by A14, A13, A43, A42;

 end;

 theorem :: COMPLEX2:84



 Th82: a <> b & b <> c & 0 < ( angle (a,b,c)) & ( angle (a,b,c)) < PI implies ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = PI & 0 < ( angle (b,c,a)) & 0 < ( angle (c,a,b))

 proof

 assume that

 A1: a <> b and

 A2: b <> c and

 A3: 0 < ( angle (a,b,c)) and

 A4: ( angle (a,b,c)) < PI ;



 A5: (c - b) <> 0 by A2;

 set r = ( - ( Arg (a + ( - b))));

 set A = ( Rotate ((a + ( - b)),r)), B = ( Rotate ((c + ( - b)),r));



 A6: ( Rotate ( 0c ,r)) = 0c by Th50;



 A7: (c + ( - b)) <> (a + ( - b)) by A3, Th77;



 A8: ( angle (b,c,a)) = ( angle ((b + ( - b)),(c + ( - b)),(a + ( - b)))) by Th70

 .= ( angle ( 0c ,B,A)) by A6, A7, A5, Th76;



 A9: ( angle ((a + ( - b)), 0c ,(c + ( - b)))) = ( angle ((a + ( - b)),(b + ( - b)),(c + ( - b))))

 .= ( angle (a,b,c)) by Th70;



 A10: (a - b) <> 0 by A1;

 then

 A11: ( angle ((a + ( - b)), 0c ,(c + ( - b)))) = ( angle (A, 0c ,B)) by A6, A5, Th76;

 (a + ( - b)) <> 0c by A1;

 then |.(a + ( - b)).| > 0 by COMPLEX1: 47;

 then

 A12: ( Im A) = 0 & ( Re A) > 0 by COMPLEX1: 12, SIN_COS: 31;

 then

 A13: ( Arg A) = 0c by Th19;

 then (( Arg (B - 0c )) - ( Arg (A - 0c ))) >= 0 by COMPTRIG: 34;

 then

 A14: ( angle (a,b,c)) = ( Arg B) by A9, A11, A13, Def4;



 A15: ( angle (c,a,b)) = ( angle ((c + ( - b)),(a + ( - b)),(b + ( - b)))) by Th70

 .= ( angle (B,A, 0c )) by A6, A10, A7, Th76;

 hence ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = PI by A3, A4, A9, A11, A12, A14, A8, Lm5;

 thus 0 < ( angle (b,c,a)) by A3, A4, A12, A14, A8, Lm5;

 thus thesis by A3, A4, A12, A14, A15, Lm5;

 end;

 theorem :: COMPLEX2:85



 Th83: a <> b & b <> c & ( angle (a,b,c)) > PI implies ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = (5 * PI ) & ( angle (b,c,a)) > PI & ( angle (c,a,b)) > PI

 proof

 assume that

 A1: a <> b & b <> c and

 A2: ( angle (a,b,c)) > PI ;



 A3: ( angle (c,b,a)) < PI

 proof

 assume not thesis;

 then (( angle (a,b,c)) + ( angle (c,b,a))) > ( PI + PI ) by A2, XREAL_1: 8;

 hence contradiction by A2, Th78, COMPTRIG: 5;

 end;



 A4: (( angle (a,b,c)) + ( angle (c,b,a))) = ((2 * PI ) + 0 ) by A2, Th78, COMPTRIG: 5;

 then

 A5: ( angle (c,b,a)) <> 0 by Th68;



 A6: 0 <= ( angle (c,b,a)) by Th68;

 then ( angle (b,a,c)) > 0 by A1, A5, A3, Th82;

 then

 A7: (( angle (c,a,b)) + ( angle (b,a,c))) = ((2 * PI ) + 0 ) by Th78;

 ( angle (a,c,b)) > 0 by A1, A6, A5, A3, Th82;

 then (( angle (b,c,a)) + ( angle (a,c,b))) = ((2 * PI ) + 0 ) by Th78;

 then ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = ((((2 * PI ) + (2 * PI )) + (2 * PI )) - ((( angle (c,b,a)) + ( angle (b,a,c))) + ( angle (a,c,b)))) by A4, A7;



 hence

 A8: ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = (((((2 * PI ) + (2 * PI )) + PI ) + PI ) - PI ) by A1, A6, A5, A3, Th82

 .= (5 * PI );



 A9: ( angle (a,b,c)) < (2 * PI ) by Th68;

 ( angle (b,c,a)) < (2 * PI ) by Th68;

 then

 A10: (((2 * PI ) + (2 * PI )) + PI ) = (5 * PI ) & (( angle (a,b,c)) + ( angle (b,c,a))) < ((2 * PI ) + (2 * PI )) by A9, XREAL_1: 8;



 A11: (((2 * PI ) + PI ) + (2 * PI )) = (5 * PI );

 hereby

 assume ( angle (b,c,a)) <= PI ;

 then

 A12: (( angle (a,b,c)) + ( angle (b,c,a))) < ((2 * PI ) + PI ) by A9, XREAL_1: 8;

 ( angle (c,a,b)) < (2 * PI ) by Th68;

 hence contradiction by A8, A11, A12, XREAL_1: 8;

 end;

 assume ( angle (c,a,b)) <= PI ;

 hence contradiction by A8, A10, XREAL_1: 8;

 end;



 Lm6: ( Im a) = 0 & ( Re a) > 0 & ( Arg b) = PI implies ((( angle (a, 0 ,b)) + ( angle ( 0 ,b,a))) + ( angle (b,a, 0 ))) = PI & 0 = ( angle ( 0 ,b,a)) & 0 = ( angle (b,a, 0 ))

 proof

 assume that

 A1: ( Im a) = 0 and

 A2: ( Re a) > 0 and

 A3: ( Arg b) = PI ;



 A4: ( Im (a - b)) = (( Im a) - ( Im b)) by COMPLEX1: 19

 .= ( - ( Im b)) by A1;



 A5: (( Re b) + 0 ) < ( Re a) by A2, A3, Th20;

 then (( Re a) - ( Re b)) > 0 by XREAL_1: 20;

 then

 A6: ( Re (a - b)) > 0 by COMPLEX1: 19;

 a = (( Re a) + ( 0 * )) by A1, COMPLEX1: 13;

 then

 A7: ( Arg a) = 0 by A2, COMPTRIG: 35;

 then

 A8: (( Arg (b - 0c )) - ( Arg (a - 0c ))) > 0 by A3, COMPTRIG: 5;

 ( - ( - (( Re a) - ( Re b)))) > 0 by A5, XREAL_1: 20;

 then (( Re b) - ( Re a)) < 0 ;

 then

 A9: ( Re (b - a)) < 0 by COMPLEX1: 19;



 A10: ( Im (b - a)) = (( Im b) - ( Im a)) by COMPLEX1: 19

 .= 0 by A1, A3, Th20;

 then

 A11: ( - ( Arg (b - a))) = ( - PI ) by A9, Th20;



 A12: ( Arg (b - a)) = PI by A9, A10, Th20;



 A13: ( Arg ( - b)) = (( Arg b) - PI ) by A3, Lm1, Th12, COMPTRIG: 5;



 A14: ( Im b) = 0 by A3, Th20;

 then

 A15: ( Arg (a - b)) = 0 by A4, A6, Th19;

 ( Arg ( - a)) = (( Arg a) + PI ) by A2, A7, Th12, COMPLEX1: 4, COMPTRIG: 5

 .= PI by A7;

 then

 A16: ( angle (b,a, 0c )) = (( Arg ( 0c - a)) - ( Arg (b - a))) by A11, Def4;



 A17: (( Arg a) - ( Arg ( - a))) = (( Arg a) - (( Arg a) + PI )) by A2, A7, Th12, COMPLEX1: 4, COMPTRIG: 5

 .= ( - PI );



 A18: ( Arg ( - b)) = (( Arg b) - PI ) by A3, Lm1, Th12, COMPTRIG: 5;

 then

 A19: (( Arg (a - b)) - ( Arg ( 0c - b))) = 0 by A3, A14, A4, A6, Th19;

 then ( angle ( 0c ,b,a)) = (( Arg (a - b)) - ( Arg ( - b))) by Def4;



 hence

 A20: ((( angle (a, 0 ,b)) + ( angle ( 0 ,b,a))) + ( angle (b,a, 0 ))) = (((( Arg b) - ( Arg a)) + (( Arg (a - b)) - ( Arg ( - b)))) + (( Arg ( 0 - a)) - ( Arg (b - a)))) by A8, A16, Def4

 .= ((((( Arg b) - ( Arg ( - b))) - ( Arg a)) + ( Arg (a - b))) + (( Arg ( - a)) - ( Arg (b - a))))

 .= PI by A15, A12, A13, A17;

 ((( Arg (a - b)) + PI ) - ( Arg b)) = 0 by A3, A14, A4, A6, Th19;

 then

 A21: ( angle ( 0c ,b,a)) = (( Arg (a - b)) - ( Arg ( 0c - b))) by A18, Def4;

 thus 0 = ( angle ( 0 ,b,a)) by A19, Def4;

 ( angle (a, 0c ,b)) = (( Arg b) - ( Arg a)) by A8, Def4;

 hence thesis by A3, A7, A19, A21, A20, XCMPLX_1: 3;

 end;

 theorem :: COMPLEX2:86



 Th84: a <> b & b <> c & ( angle (a,b,c)) = PI implies ( angle (b,c,a)) = 0 & ( angle (c,a,b)) = 0

 proof

 assume that

 A1: a <> b and

 A2: b <> c and

 A3: ( angle (a,b,c)) = PI ;



 A4: (c - b) <> 0 by A2;

 set r = ( - ( Arg (a + ( - b))));

 set A = ( Rotate ((a + ( - b)),r)), B = ( Rotate ((c + ( - b)),r));



 A5: ( Rotate ( 0c ,r)) = 0c by Th50;



 A6: ( angle ((a + ( - b)), 0c ,(c + ( - b)))) = ( angle ((a + ( - b)),(b + ( - b)),(c + ( - b))))

 .= ( angle (a,b,c)) by Th70;



 A7: (c + ( - b)) <> (a + ( - b)) by A3, Th77, COMPTRIG: 5;



 A8: (a - b) <> 0 by A1;

 then

 A9: ( angle ((a + ( - b)), 0c ,(c + ( - b)))) = ( angle (A, 0c ,B)) by A5, A4, Th76;

 (a + ( - b)) <> 0c by A1;

 then |.(a + ( - b)).| > 0 by COMPLEX1: 47;

 then

 A10: ( Im A) = 0 & ( Re A) > 0 by COMPLEX1: 12, SIN_COS: 31;

 then

 A11: ( Arg A) = 0c by Th19;

 then (( Arg (B - 0c )) - ( Arg (A - 0c ))) >= 0 by COMPTRIG: 34;

 then

 A12: ( angle (a,b,c)) = ( Arg B) by A6, A9, A11, Def4;

 ( angle (b,c,a)) = ( angle ((b + ( - b)),(c + ( - b)),(a + ( - b)))) by Th70

 .= ( angle ( 0c ,B,A)) by A5, A7, A4, Th76;

 hence ( angle (b,c,a)) = 0 by A3, A10, A12, Lm6;

 ( angle (c,a,b)) = ( angle ((c + ( - b)),(a + ( - b)),(b + ( - b)))) by Th70

 .= ( angle (B,A, 0c )) by A5, A8, A7, Th76;

 hence thesis by A3, A10, A12, Lm6;

 end;

 theorem :: COMPLEX2:87



 Th85: a <> b & a <> c & b <> c & ( angle (a,b,c)) = 0 implies ( angle (b,c,a)) = 0 & ( angle (c,a,b)) = PI or ( angle (b,c,a)) = PI & ( angle (c,a,b)) = 0

 proof

 assume that

 A1: a <> b and

 A2: a <> c and

 A3: b <> c and

 A4: ( angle (a,b,c)) = 0 ;

 per cases by A1, A2, A3, A4, Th81;

 suppose

 A5: ( angle (b,c,a)) <> 0 ;



 A6: 0 <= ( angle (b,c,a)) by Th68;

 thus thesis

 proof

 per cases by XXREAL_0: 1;

 suppose ( angle (b,c,a)) < PI ;

 hence thesis by A2, A3, A4, A5, A6, Th82;

 end;

 suppose ( angle (b,c,a)) = PI ;

 hence thesis by A2, A3, Th84;

 end;

 suppose ( angle (b,c,a)) > PI ;

 hence thesis by A2, A3, A4, Th83, COMPTRIG: 5;

 end;

 end;

 end;

 suppose

 A7: ( angle (c,a,b)) <> 0 ;



 A8: 0 <= ( angle (c,a,b)) by Th68;

 thus thesis

 proof

 per cases by XXREAL_0: 1;

 suppose ( angle (c,a,b)) < PI ;

 hence thesis by A1, A2, A4, A7, A8, Th82;

 end;

 suppose ( angle (c,a,b)) = PI ;

 hence thesis by A1, A2, Th84;

 end;

 suppose ( angle (c,a,b)) > PI ;

 hence thesis by A1, A2, A4, Th83, COMPTRIG: 5;

 end;

 end;

 end;

 end;

 theorem :: COMPLEX2:88

 ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = PI or ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = (5 * PI ) iff a <> b & a <> c & b <> c

 proof

 hereby

 assume

 A1: ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = PI or ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = (5 * PI );

 per cases by A1;

 suppose

 A2: ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = PI ;

 thus a <> b & a <> c & b <> c

 proof

 assume

 A3: not (a <> b & a <> c & b <> c);

 per cases by A3;

 suppose

 A4: a = b;



 A5: ( angle (a,c,a)) = 0 by Th77;

 not (( angle (a,a,c)) = 0 & ( angle (c,a,a)) = 0 ) by A2, A4, Th77, COMPTRIG: 5;

 hence contradiction by A2, A4, A5, Th78, COMPTRIG: 5;

 end;

 suppose

 A6: a = c;



 A7: ( angle (a,b,a)) = 0 by Th77;

 not (( angle (a,a,b)) = 0 & ( angle (b,a,a)) = 0 ) by A2, A6, Th77, COMPTRIG: 5;

 hence contradiction by A2, A6, A7, Th78, COMPTRIG: 5;

 end;

 suppose

 A8: b = c;



 A9: ( angle (b,a,b)) = 0 by Th77;

 not (( angle (a,b,b)) = 0 & ( angle (b,b,a)) = 0 ) by A2, A8, Th77, COMPTRIG: 5;

 hence contradiction by A2, A8, A9, Th78, COMPTRIG: 5;

 end;

 end;

 end;

 suppose

 A10: ((( angle (a,b,c)) + ( angle (b,c,a))) + ( angle (c,a,b))) = (5 * PI );



 A11: ((2 + 2) * PI ) < (5 * PI ) by COMPTRIG: 5, XREAL_1: 68;

 then

 A12: ((2 * PI ) + (2 * PI )) < (5 * PI );

 thus a <> b & a <> c & b <> c

 proof

 assume

 A13: not (a <> b & a <> c & b <> c);

 per cases by A13;

 suppose a = b;

 then ( angle (b,c,a)) = 0 by Th77;

 then

 A14: (( angle (a,b,c)) + ( angle (b,c,a))) < (2 * PI ) by Th68;

 ( angle (c,a,b)) < (2 * PI ) by Th68;

 hence contradiction by A10, A12, A14, XREAL_1: 8;

 end;

 suppose

 A15: b = c;

 ( angle (a,b,c)) < (2 * PI ) & ( angle (b,c,a)) < (2 * PI ) by Th68;

 then

 A16: (( angle (a,b,c)) + ( angle (b,c,a))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 ( angle (c,a,b)) = 0 by A15, Th77;

 hence contradiction by A10, A11, A16;

 end;

 suppose a = c;

 then ( angle (a,b,c)) = 0 by Th77;

 then

 A17: (( angle (a,b,c)) + ( angle (b,c,a))) < (2 * PI ) by Th68;

 ( angle (c,a,b)) < (2 * PI ) by Th68;

 hence contradiction by A10, A12, A17, XREAL_1: 8;

 end;

 end;

 end;

 end;

 assume that

 A18: a <> b and

 A19: a <> c and

 A20: b <> c;

 per cases by XXREAL_0: 1;

 suppose

 A21: ( angle (a,b,c)) = 0 ;

 (( angle (b,c,a)) + ( angle (c,a,b))) = PI

 proof

 per cases by A18, A19, A20, A21, Th85;

 suppose ( angle (b,c,a)) = 0 & ( angle (c,a,b)) = PI ;

 hence thesis;

 end;

 suppose ( angle (b,c,a)) = PI & ( angle (c,a,b)) = 0 ;

 hence thesis;

 end;

 end;

 hence thesis by A21;

 end;

 suppose

 A22: 0 <> ( angle (a,b,c)) & ( angle (a,b,c)) < PI ;

 0 <= ( angle (a,b,c)) by Th68;

 hence thesis by A18, A20, A22, Th82;

 end;

 suppose

 A23: 0 <> ( angle (a,b,c)) & ( angle (a,b,c)) = PI ;

 then ( angle (b,c,a)) = 0 by A18, A20, Th84;

 hence thesis by A18, A20, A23, Th84;

 end;

 suppose 0 <> ( angle (a,b,c)) & ( angle (a,b,c)) > PI ;

 hence thesis by A18, A20, Th83;

 end;

 end;