let x, y be Real; :: thesis: ( abs x <= |.(x + (y * <i> )).| & abs y <= |.(x + (y * <i> )).| )
set z = x + (y * <i> );
( Re (x + (y * <i> )) = x & Im (x + (y * <i> )) = y ) by COMPLEX1:28;
hence ( abs x <= |.(x + (y * <i> )).| & abs y <= |.(x + (y * <i> )).| ) by COMPLEX1:165; :: thesis: verum