let z be complex number ; :: thesis: Im z >= - |.z.|
0 <= (Re z) ^2 by XREAL_1:65;
then A1: ((Im z) ^2 ) + 0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by XREAL_1:9;
0 <= (Im z) ^2 by XREAL_1:65;
then sqrt ((Im z) ^2 ) <= |.z.| by A1, SQUARE_1:94;
then - (sqrt ((Im z) ^2 )) >= - |.z.| by XREAL_1:26;
then ( Im z >= - (abs (Im z)) & - (abs (Im z)) >= - |.z.| ) by ABSVALUE:11, COMPLEX1:158;
hence Im z >= - |.z.| by XXREAL_0:2; :: thesis: verum