let z be 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) ") )
Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence Re (z ") = 0 by A1; :: thesis: Im (z ") = - ((Im z) ")
Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence Im (z ") = - ((1 * (Im z)) / ((Im z) * (Im z))) by A1, XCMPLX_1:187
.= - (1 / (Im z)) by A2, XCMPLX_1:91
.= - ((Im z) ") by XCMPLX_1:215 ;
:: thesis: verum