let z be Complex; :: thesis: ( Im z = 0 iff ( Arg z = 0 or Arg z = PI ) )

hereby :: thesis: ( ( Arg z = 0 or Arg z = PI ) implies Im z = 0 )

A1: ( Arg ((Re z) + (0 * <i>)) = 0 or Arg ((Re z) + (0 * <i>)) = PI ) by COMPTRIG:35, COMPTRIG:36;
assume Im z = 0 ; :: thesis: ( Arg z = 0 or Arg z = PI )
hence ( Arg z = 0 or Arg z = PI ) by A1, COMPLEX1:13; :: thesis: verum

end;

assume ( Arg z = 0 or Arg z = PI ) ; :: thesis: Im z = 0
hence Im z = 0 by Th19, Th20; :: thesis: verum