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