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