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