let r be Real; :: thesis: for a, b being Complex st Arg a = Arg b & a <> 0 & b <> 0 holds
Arg (Rotate (a,r)) = Arg (Rotate (b,r))
let a, b be Complex; :: 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, Th52;
consider j being Integer such that
A5: Arg (Rotate (b,r)) = ((2 * PI) * j) + (r + (Arg b)) by A3, Th52;
A6: ( 0 <= Arg (Rotate (a,r)) & 0 <= Arg (Rotate (b,r)) ) by COMPTRIG:34;
A7: ( Arg (Rotate (a,r)) < 2 * PI & Arg (Rotate (b,r)) < 2 * PI ) by COMPTRIG:34;
Arg (Rotate (b,r)) = ((2 * PI) * (j - i)) + (Arg (Rotate (a,r))) by A1, A4, A5;
hence Arg (Rotate (a,r)) = Arg (Rotate (b,r)) by A6, A7, Th2; :: thesis: verum