let x, y, z be Complex; :: thesis: ( angle (x,y,z) <> 0 implies angle (z,y,x) = (2 * PI) - (angle (x,y,z)) )
assume A1: angle (x,y,z) <> 0 ; :: thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z))
now :: thesis: ( ( (Arg (x - y)) - (Arg (z - y)) > 0 & angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ) or ( (Arg (x - y)) - (Arg (z - y)) <= 0 & angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ) )
per cases ( (Arg (x - y)) - (Arg (z - y)) > 0 or (Arg (x - y)) - (Arg (z - y)) <= 0 ) ;
case A2: (Arg (x - y)) - (Arg (z - y)) > 0 ; :: thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z))
then - (- ((Arg (x - y)) - (Arg (z - y)))) > 0 ;
then angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by Def4
.= (2 * PI) - ((Arg (x - y)) - (Arg (z - y))) ;
hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) by A2, Def4; :: thesis: verum
end;
case A3: (Arg (x - y)) - (Arg (z - y)) <= 0 ; :: thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z))
(Arg (x - y)) - (Arg (z - y)) <> 0 by A1, Def4;
then A4: angle (z,y,x) = (2 * PI) - ((Arg (z - y)) - (Arg (x - y))) by A3, Def4;
- (- ((Arg (x - y)) - (Arg (z - y)))) <= 0 by A3;
then (angle (x,y,z)) + (angle (z,y,x)) = ((2 * PI) - ((Arg (z - y)) - (Arg (x - y)))) + ((Arg (z - y)) - (Arg (x - y))) by A4, Def4
.= 2 * PI ;
hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ; :: thesis: verum
end;
end;
end;
hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ; :: thesis: verum