( Re (z * r) = ((Re z) * (Re r)) - ((Im r) * (Im z)) & Re z = 0 & Im r = 0 ) by Def3, COMPLEX1:9;
hence z * r is imaginary ; :: thesis: verum