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 & 0 <= Arg b & Arg b < 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;
consider i being Integer such that
A5: Arg (Rotate b,(- (Arg a))) = ((2 * PI ) * i) + ((- (Arg a)) + (Arg b)) by A2, Th68;
( 0 <= angle a,0c ,b & angle a,0c ,b < 2 * PI ) by Th84;
hence angle a,b = angle a,0 ,b by A1, A3, A4, A5, Th3; :: thesis: verum

end;

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

then A6: angle a,0c ,b = (2 * PI ) + ((Arg b) + (- (Arg a))) by Def6;
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))) ;
( 0 <= (2 * PI ) + ((- (Arg a)) + (Arg b)) & (2 * PI ) + ((- (Arg a)) + (Arg b)) < 2 * PI ) by A6, Th84;
hence angle a,b = angle a,0 ,b by A1, A3, A6, A7, A8, Th3; :: thesis: verum

end;

end;

end;

end;

suppose A9: 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 A10: Arg a = 0 ; :: thesis: angle a,b = angle a,0 ,b

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

end;

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

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

end;

end;

end;

end;

end;