let a, b be Element of 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, Th68;
set br = b * r;
set ar = a * r;
( Arg (b * r) = Arg (- b) & Arg (a * r) = Arg (- a) ) by A1, Th41;
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, Th68;
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:52;
A8: ( 0 <= Arg (Rotate (- b),(- (Arg (- a)))) & Arg (Rotate (- b),(- (Arg (- a)))) < 2 * PI ) by COMPTRIG:52;
thus angle a,b = angle (Rotate a,PI ),(Rotate b,PI ) by A2, A3, Th79
.= angle (- a),(Rotate b,PI ) by Th74
.= angle (- a),(- b) by Th74
.= Arg (Rotate (- b),(- (Arg (- a)))) by A3, Def5
.= Arg (Rotate (b * r),(- (Arg (a * r)))) by A6, A7, A8, Th3
.= angle (a * r),(b * r) by A1, A3, Def5 ; :: thesis: verum