let z be Element of COMPLEX ; :: thesis: ( Re z <> 0 & Im z = 0 implies ( Re (z " ) = (Re z) " & Im (z " ) = 0 ) )
assume A1: ( Re z <> 0 & Im z = 0 ) ; :: thesis: ( Re (z " ) = (Re z) " & Im (z " ) = 0 )
hence Re (z " ) = (1 * (Re z)) / ((Re z) * (Re z)) by Th64
.= 1 / (Re z) by A1, XCMPLX_1:92
.= (Re z) " by XCMPLX_1:217 ;
:: thesis: Im (z " ) = 0
thus Im (z " ) = 0 by A1, Th64; :: thesis: verum