let a, b be 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:34;
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 Def3;
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 Def4;
A5: angle (a,0c,b) < 2 * PI by Th68;
( ex i being Integer st Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) & 0 <= angle (a,0c,b) ) by A2, Th52, Th68;
hence angle (a,b) = angle (a,0,b) by A1, A3, A4, A5, Th2; :: 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, Th52;
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, Def4;
then ( 0 <= (2 * PI) + ((- (Arg a)) + (Arg b)) & (2 * PI) + ((- (Arg a)) + (Arg b)) < 2 * PI ) by Th68;
hence angle (a,b) = angle (a,0,b) by A1, A3, A9, A7, A8, Th2; :: 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:35;
angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by A11, Def3
.= 0 by A10, Lm1, Th50 ;
hence angle (a,b) = angle (a,0,b) by A12, Def4; :: thesis: verum
end;
suppose A13: Arg a <> 0 ; :: thesis: angle (a,b) = angle (a,0,b)
then A14: 0 < - (- (Arg a)) by COMPTRIG:34;
(Arg (b - 0c)) - (Arg (a - 0c)) = - (Arg a) by A10, Lm1;
then angle (a,0c,b) = (2 * PI) - (Arg a) by A14, Def4;
hence angle (a,b) = angle (a,0,b) by A10, A13, Def3; :: thesis: verum
end;
end;
end;
end;
end;