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:5
.= PI by A3 ;
hence angle (a,(- b)) = PI by A1, A4, Def5; :: thesis: verum