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