let a, b be Element of 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, Th68;
A4: Rotate b,r <> 0 by A2, Th66;
then consider j being Integer such that
A5: Arg (Rotate (Rotate b,r),(- (Arg (Rotate a,r)))) = ((2 * PI ) * j) + ((- (Arg (Rotate a,r))) + (Arg (Rotate b,r))) by Th68;
consider k being Integer such that
A6: Arg (Rotate a,r) = ((2 * PI ) * k) + (r + (Arg a)) by A1, Th68;
consider l being Integer such that
A7: Arg (Rotate b,r) = ((2 * PI ) * l) + (r + (Arg b)) by A2, Th68;
A8: Arg (Rotate (Rotate b,r),(- (Arg (Rotate a,r)))) = ((2 * PI ) * (((j - k) + l) - i)) + (Arg (Rotate b,(- (Arg a)))) by A3, A5, A6, A7;
A9: ( 0 <= Arg (Rotate b,(- (Arg a))) & Arg (Rotate b,(- (Arg a))) < 2 * PI & 0 <= Arg (Rotate (Rotate b,r),(- (Arg (Rotate a,r)))) & Arg (Rotate (Rotate b,r),(- (Arg (Rotate a,r)))) < 2 * PI ) by COMPTRIG:52;
thus angle a,b = Arg (Rotate b,(- (Arg a))) by A2, Def5
.= Arg (Rotate (Rotate b,r),(- (Arg (Rotate a,r)))) by A8, A9, Th3
.= angle (Rotate a,r),(Rotate b,r) by A4, Def5 ; :: thesis: verum