let z be complex number ; :: thesis: Im z <= |.z.|
( (Im z) ^2 <= (Im z) ^2 & 0 <= (Re z) ^2 ) by XREAL_1:65;
then ((Im z) ^2 ) + 0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by XREAL_1:9;
then ( 0 <= (Im z) ^2 & (Im z) ^2 <= ((Re z) ^2 ) + ((Im z) ^2 ) ) by XREAL_1:65;
then sqrt ((Im z) ^2 ) <= |.z.| by SQUARE_1:94;
then ( Im z <= |.(Im z).| & |.(Im z).| <= |.z.| ) by Lm24, Lm25;
hence Im z <= |.z.| by XXREAL_0:2; :: thesis: verum