let r be Real; :: thesis: for a, b being complex number st Arg a = Arg b & a <> 0 & b <> 0 holds
Arg (Rotate a,r) = Arg (Rotate b,r)
let a, b be complex number ; :: thesis: ( Arg a = Arg b & a <> 0 & b <> 0 implies Arg (Rotate a,r) = Arg (Rotate b,r) )
assume that
A1: Arg a = Arg b and
A2: a <> 0 and
A3: b <> 0 ; :: thesis: Arg (Rotate a,r) = Arg (Rotate b,r)
consider i being Integer such that
A4: Arg (Rotate a,r) = ((2 * PI ) * i) + (r + (Arg a)) by A2, Th68;
consider j being Integer such that
A5: Arg (Rotate b,r) = ((2 * PI ) * j) + (r + (Arg b)) by A3, Th68;
A6: Arg (Rotate b,r) = ((2 * PI ) * (j - i)) + (Arg (Rotate a,r)) by A1, A4, A5;
( 0 <= Arg (Rotate a,r) & 0 <= Arg (Rotate b,r) & Arg (Rotate a,r) < 2 * PI & Arg (Rotate b,r) < 2 * PI ) by COMPTRIG:52;
hence Arg (Rotate a,r) = Arg (Rotate b,r) by A6, Th3; :: thesis: verum