let x, y be Real; :: thesis: for z being Complex st z = x + (y * <i>) holds
|.z.| <= |.x.| + |.y.|
let z be Complex; :: thesis: ( z = x + (y * <i>) implies |.z.| <= |.x.| + |.y.| )
assume z = x + (y * <i>) ; :: thesis: |.z.| <= |.x.| + |.y.|
then ( Re z = x & Im z = y ) by COMPLEX1:12;
hence |.z.| <= |.x.| + |.y.| by COMPLEX1:78; :: thesis: verum