let x, y be Complex; :: thesis: ( Im x = 0 & Re y = 0 implies Re (x / y) = 0 )
reconsider R2 = (Re y) ^2 , I2 = (Im y) ^2 as Real ;
assume A1: ( Im x = 0 & Re y = 0 ) ; :: thesis: Re (x / y) = 0
then Re (x / y) = (((Re x) * 0) + ((Im x) * (Im y))) / (R2 + I2) by COMPLEX1:24
.= 0 / (R2 + I2) by A1 ;
hence Re (x / y) = 0 ; :: thesis: verum