let z be Complex; :: thesis: ( Re z <> 0 & Im z = 0 implies ( Re (z ") = (Re z) " & Im (z ") = 0 ) )
assume that
A1: Re z <> 0 and
A2: Im z = 0 ; :: thesis: ( Re (z ") = (Re z) " & Im (z ") = 0 )
Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence Re (z ") = (1 * (Re z)) / ((Re z) * (Re z)) by A2
.= 1 / (Re z) by A1, XCMPLX_1:91
.= (Re z) " by XCMPLX_1:215 ;
:: thesis: Im (z ") = 0
Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence Im (z ") = 0 by A2; :: thesis: verum