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

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