let a be Element of COMPLEX ; :: thesis: ( a <> 0 implies ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) )
A1: |.(- a).| = |.a.| by COMPLEX1:52;
assume a <> 0 ; :: thesis: ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) )
then A2: |.a.| <> 0 by COMPLEX1:45;
( a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) & - a = (|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i>) ) by COMPTRIG:62;
then A3: 0 + (0 * <i>) = ((|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a))))) + (((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i>) 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 ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) by A4; :: thesis: verum