let a, b be Complex; :: thesis: for r being Real st r < 0 & a <> 0 & b <> 0 holds
angle (a,b) = angle ((a * r),(b * r))
let r be Real; :: thesis: ( r < 0 & a <> 0 & b <> 0 implies angle (a,b) = angle ((a * r),(b * r)) )
assume that
A1: r < 0 and
A2: a <> 0 and
A3: b <> 0 ; :: thesis: angle (a,b) = angle ((a * r),(b * r))
consider i being Integer such that
A4: Arg (Rotate ((- b),(- (Arg (- a))))) = ((2 * PI) * i) + ((- (Arg (- a))) + (Arg (- b))) by A3, Th52;
set br = b * r;
set ar = a * r;
( Arg (b * r) = Arg (- b) & Arg (a * r) = Arg (- a) ) by A1, Th26;
then consider j being Integer such that
A5: Arg (Rotate ((b * r),(- (Arg (a * r))))) = ((2 * PI) * j) + ((- (Arg (- a))) + (Arg (- b))) by A1, A3, Th52;
A6: Arg (Rotate ((b * r),(- (Arg (a * r))))) = ((2 * PI) * (j - i)) + (Arg (Rotate ((- b),(- (Arg (- a)))))) by A4, A5;
A7: ( 0 <= Arg (Rotate ((b * r),(- (Arg (a * r))))) & Arg (Rotate ((b * r),(- (Arg (a * r))))) < 2 * PI ) by COMPTRIG:34;
A8: ( 0 <= Arg (Rotate ((- b),(- (Arg (- a))))) & Arg (Rotate ((- b),(- (Arg (- a))))) < 2 * PI ) by COMPTRIG:34;
thus angle (a,b) = angle ((Rotate (a,PI)),(Rotate (b,PI))) by A2, A3, Th63
.= angle ((- a),(Rotate (b,PI))) by Th58
.= angle ((- a),(- b)) by Th58
.= Arg (Rotate ((- b),(- (Arg (- a))))) by A3, Def3
.= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A6, A7, A8, Th2
.= angle ((a * r),(b * r)) by A1, A3, Def3 ; :: thesis: verum