let z be complex number ; :: 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:131;
z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> ) by Th19;
then A3: - z = (- (|.z.| * (cos (Arg z)))) + ((- (|.z.| * (sin (Arg z)))) * <i> ) ;
Arg z < 2 * PI by COMPTRIG:52;
then (Arg z) + 0 < (2 * PI ) + PI by COMPTRIG:21, XREAL_1:10;
then A4: (Arg z) - PI < 2 * PI by XREAL_1:21;
A5: - z = (|.(- z).| * (cos (Arg (- z)))) + ((|.(- z).| * (sin (Arg (- z)))) * <i> ) by Th19;
A6: |.z.| = |.(- z).| by COMPLEX1:138;
then |.z.| * (sin (Arg (- z))) = |.z.| * (- (sin (Arg z))) by A5, A3, COMPLEX1:163;
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:84;
|.z.| * (cos (Arg (- z))) = |.z.| * (- (cos (Arg z))) by A5, A3, A6, COMPLEX1:163;
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:84;

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:10;
0 <= Arg z by COMPTRIG:52;
hence Arg (- z) = (Arg z) + PI by A1, A5, A10, A8, A11, COMPTRIG:21, 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:11;
A13: sin (Arg (- z)) = sin ((Arg z) - PI ) by A7, Th6;
cos (Arg (- z)) = cos ((Arg z) - PI ) by A9, Th6;
hence Arg (- z) = (Arg z) - PI by A1, A5, A13, A12, A4, COMPTRIG:def 1; :: thesis: verum