let z be Complex; :: thesis: ( z <> 0 implies ( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) ) )
assume A1: z <> 0 ; :: thesis: ( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) )
then A2: |.z.| <> 0 by COMPLEX1:45;
z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>) by COMPTRIG:62;
then A3: - z = (- (|.z.| * (cos (Arg z)))) + ((- (|.z.| * (sin (Arg z)))) * <i>) ;
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)))) * <i>) 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 :: thesis: ( Arg z >= PI implies Arg (- z) = (Arg z) - PI )
assume Arg z < PI ; :: thesis: Arg (- z) = (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; :: thesis: verum
end;
assume Arg z >= PI ; :: thesis: Arg (- z) = (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 Arg (- z) = (Arg z) - PI by A1, A5, A13, A12, A4, COMPTRIG:def 1; :: thesis: verum