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;
A4: z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> ) by Th19;
A5: - z = (|.(- z).| * (cos (Arg (- z)))) + ((|.(- z).| * (sin (Arg (- z)))) * <i> ) by Th19;
A6: - z = (- (|.z.| * (cos (Arg z)))) + ((- (|.z.| * (sin (Arg z)))) * <i> ) by A4;
A7: |.z.| = |.(- z).| by COMPLEX1:138;
then |.z.| * (cos (Arg (- z))) = |.z.| * (- (cos (Arg z))) by A5, A6, COMPLEX1:163;
then cos (Arg (- z)) = - (cos (Arg z)) by A2, XCMPLX_1:5;
then A8: ( cos (Arg (- z)) = cos ((Arg z) + PI ) & cos (Arg (- z)) = cos ((Arg z) - PI ) ) by Th6, SIN_COS:84;
|.z.| * (sin (Arg (- z))) = |.z.| * (- (sin (Arg z))) by A5, A6, A7, COMPLEX1:163;
then sin (Arg (- z)) = - (sin (Arg z)) by A2, XCMPLX_1:5;
then A9: ( sin (Arg (- z)) = sin ((Arg z) + PI ) & sin (Arg (- z)) = sin ((Arg z) - PI ) ) by Th6, 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 A10: (Arg z) + PI < PI + PI by XREAL_1:10;
0 <= Arg z by COMPTRIG:52;
hence Arg (- z) = (Arg z) + PI by A1, A5, A8, A9, A10, COMPTRIG:def 1, COMPTRIG:21; :: thesis: verum

end;

assume Arg z >= PI ; :: thesis: Arg (- z) = (Arg z) - PI
then A11: (Arg z) - PI >= PI - PI by XREAL_1:11;
Arg z < 2 * PI by COMPTRIG:52;
then (Arg z) + 0 < (2 * PI ) + PI by COMPTRIG:21, XREAL_1:10;
then (Arg z) - PI < 2 * PI by XREAL_1:21;
hence Arg (- z) = (Arg z) - PI by A1, A5, A8, A9, A11, COMPTRIG:def 1; :: thesis: verum