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