let z be Complex; :: thesis: ( z <> 0 implies ( Arg z < PI iff Arg (- z) >= PI ) )
assume A1: z <> 0 ; :: thesis: ( Arg z < PI iff Arg (- z) >= PI )
thus ( Arg z < PI implies Arg (- z) >= PI ) :: thesis: ( Arg (- z) >= PI implies Arg z < PI )
proof
Arg z >= 0 by COMPTRIG:34;
then A2: PI + 0 <= PI + (Arg z) by XREAL_1:7;
assume Arg z < PI ; :: thesis: Arg (- z) >= PI
hence Arg (- z) >= PI by A1, A2, Th12; :: thesis: verum
end;
thus ( Arg (- z) >= PI implies Arg z < PI ) :: thesis: verum
proof
2 * PI > Arg (- z) by COMPTRIG:34;
then A3: (PI + PI) - PI > (Arg (- z)) - PI by XREAL_1:9;
assume Arg (- z) >= PI ; :: thesis: Arg z < PI
then Arg (- (- z)) = (Arg (- z)) - PI by A1, Th12;
hence Arg z < PI by A3; :: thesis: verum
end;