let b, a be Element of COMPLEX ; :: thesis: ( b <> 0 & angle a,b = 0 implies angle a,(- b) = PI )
assume that
A1: b <> 0 and
A2: angle a,b = 0 ; :: thesis: angle a,(- b) = PI
A3: Arg (Rotate b,(- (Arg a))) = 0 by A1, A2, Def5;
A4: Arg (Rotate (- b),(- (Arg a))) = Arg (- (Rotate b,(- (Arg a)))) by Th72;
Rotate b,(- (Arg a)) <> 0 by A1, Th66;
then Arg (- (Rotate b,(- (Arg a)))) = (Arg (Rotate b,(- (Arg a)))) + PI by A3, Th22, COMPTRIG:21
.= PI by A3 ;
hence angle a,(- b) = PI by A1, A4, Def5; :: thesis: verum