(Re a) - 1 <= |.a.| - 1 by COMPLEX1:54, XREAL_1:9;
hence (Re a) - 1 is negative ; :: thesis: verum