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