let z be Complex; ( |.(Re z).| <= |.z.| & |.(Im z).| <= |.z.| )
0 <= (Re z) ^2
by XREAL_1:63;
then A1:
0 + ((Im z) ^2) <= ((Re z) ^2) + ((Im z) ^2)
by XREAL_1:6;
0 <= (Im z) ^2
by XREAL_1:63;
then A2:
sqrt ((Im z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2))
by A1, SQUARE_1:26;
0 <= (Im z) ^2
by XREAL_1:63;
then A3:
0 + ((Re z) ^2) <= ((Im z) ^2) + ((Re z) ^2)
by XREAL_1:6;
0 <= (Re z) ^2
by XREAL_1:63;
then
( |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)) & sqrt ((Re z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2)) )
by A3, COMPLEX1:def 12, SQUARE_1:26;
hence
( |.(Re z).| <= |.z.| & |.(Im z).| <= |.z.| )
by A2, COMPLEX1:72; verum