let a, b be Element of COMPLEX ; :: thesis: angle a,b = angle a,0 ,b
set ab2 = angle a,b;
A1: ( 0 <= Arg (Rotate b,(- (Arg a))) & Arg (Rotate b,(- (Arg a))) < 2 * PI ) by COMPTRIG:52;

per cases ( b <> 0 or b = 0 ) ;

suppose A2: b <> 0 ; :: thesis: angle a,b = angle a,0 ,b

then A3: angle a,b = Arg (Rotate b,(- (Arg a))) by Def5;
thus angle a,b = angle a,0 ,b :: thesis: verum

proof

per cases ( (Arg (b - 0c )) - (Arg (a - 0c )) >= 0 or (Arg (b - 0c )) - (Arg (a - 0c )) < 0 ) ;

suppose (Arg (b - 0c )) - (Arg (a - 0c )) >= 0 ; :: thesis: angle a,b = angle a,0 ,b

then A4: angle a,0c ,b = (- (Arg a)) + (Arg b) by Def6;
A5: angle a,0c ,b < 2 * PI by Th84;
( ex i being Integer st Arg (Rotate b,(- (Arg a))) = ((2 * PI ) * i) + ((- (Arg a)) + (Arg b)) & 0 <= angle a,0c ,b ) by A2, Th68, Th84;
hence angle a,b = angle a,0 ,b by A1, A3, A4, A5, Th3; :: thesis: verum

end;

suppose A6: (Arg (b - 0c )) - (Arg (a - 0c )) < 0 ; :: thesis: angle a,b = angle a,0 ,b

consider i being Integer such that
A7: Arg (Rotate b,(- (Arg a))) = ((2 * PI ) * i) + ((- (Arg a)) + (Arg b)) by A2, Th68;
A8: ((2 * PI ) * i) + ((- (Arg a)) + (Arg b)) = ((2 * PI ) * (i - 1)) + ((2 * PI ) + ((- (Arg a)) + (Arg b))) ;
A9: angle a,0c ,b = (2 * PI ) + ((Arg b) + (- (Arg a))) by A6, Def6;
then ( 0 <= (2 * PI ) + ((- (Arg a)) + (Arg b)) & (2 * PI ) + ((- (Arg a)) + (Arg b)) < 2 * PI ) by Th84;
hence angle a,b = angle a,0 ,b by A1, A3, A9, A7, A8, Th3; :: thesis: verum

end;

end;

end;

end;

suppose A10: b = 0 ; :: thesis: angle a,b = angle a,0 ,b

thus angle a,b = angle a,0 ,b :: thesis: verum

proof

per cases ( Arg a = 0 or Arg a <> 0 ) ;

suppose A11: Arg a = 0 ; :: thesis: angle a,b = angle a,0 ,b

then A12: (Arg (b - 0c )) - (Arg (a - 0c )) = 0 by A10, COMPTRIG:53;
angle a,b = Arg (Rotate b,(- (Arg a))) by A11, Def5
.= 0 by A10, Lm1, Th66 ;
hence angle a,b = angle a,0 ,b by A12, Def6; :: thesis: verum

end;

suppose A13: Arg a <> 0 ; :: thesis: angle a,b = angle a,0 ,b

then A14: 0 < - (- (Arg a)) by COMPTRIG:52;
(Arg (b - 0c )) - (Arg (a - 0c )) = - (Arg a) by A10, Lm1;
then angle a,0c ,b = (2 * PI ) - (Arg a) by A14, Def6;
hence angle a,b = angle a,0 ,b by A10, A13, Def5; :: thesis: verum

end;

end;

end;

end;

end;