let a, b be 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, Def3;
A4: Arg (Rotate ((- b),(- (Arg a)))) = Arg (- (Rotate (b,(- (Arg a))))) by Th56;
Rotate (b,(- (Arg a))) <> 0 by A1, Th50;
then Arg (- (Rotate (b,(- (Arg a))))) = (Arg (Rotate (b,(- (Arg a))))) + PI by A3, Th12, COMPTRIG:5
.= PI by A3 ;
hence angle (a,(- b)) = PI by A1, A4, Def3; :: thesis: verum