let a be Element of COMPLEX ; :: thesis: ( a <> 0 implies ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) )
assume A1: a <> 0 ; :: thesis: ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) )
A2: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i> ) by Th19;
A3: - a = (|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i> ) by Th19;
|.(- a).| = |.a.| by COMPLEX1:138;
then A4: 0 + (0 * <i> ) = ((|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a))))) + (((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i> ) by A2, A3;
then A5: |.a.| * ((cos (Arg a)) + (cos (Arg (- a)))) = 0 by COMPLEX1:12, COMPLEX1:28;
A6: |.a.| * ((sin (Arg a)) + (sin (Arg (- a)))) = 0 by A4, COMPLEX1:12, COMPLEX1:28;
|.a.| <> 0 by A1, COMPLEX1:131;
then ( (cos (Arg a)) + (- (- (cos (Arg (- a))))) = 0 & (sin (Arg a)) + (- (- (sin (Arg (- a))))) = 0 ) by A5, A6;
hence ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) ; :: thesis: verum