let z be Element of COMPLEX ; :: thesis: ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| )
A1: |.z.| = sqrt (((Re z) ^2 ) + ((Im z) ^2 )) by COMPLEX1:def 16;
A2: 0 <= (Re z) ^2 by XREAL_1:65;
0 <= (Im z) ^2 by XREAL_1:65;
then 0 + ((Re z) ^2 ) <= ((Im z) ^2 ) + ((Re z) ^2 ) by XREAL_1:8;
then A3: ( 0 <= (Re z) ^2 & (Re z) ^2 <= ((Re z) ^2 ) + ((Im z) ^2 ) ) by XREAL_1:65;
0 + ((Im z) ^2 ) <= ((Re z) ^2 ) + ((Im z) ^2 ) by A2, XREAL_1:8;
then A4: ( 0 <= (Im z) ^2 & (Im z) ^2 <= ((Re z) ^2 ) + ((Im z) ^2 ) ) by XREAL_1:65;
A5: sqrt ((Re z) ^2 ) <= sqrt (((Re z) ^2 ) + ((Im z) ^2 )) by A3, SQUARE_1:94;
sqrt ((Im z) ^2 ) <= sqrt (((Re z) ^2 ) + ((Im z) ^2 )) by A4, SQUARE_1:94;
hence ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| ) by A1, A5, COMPLEX1:158; :: thesis: verum