let z be complex number ; :: thesis: ( Re (z " ) = (Re z) / (((Re z) ^2 ) + ((Im z) ^2 )) & Im (z " ) = (- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 )) )
z in COMPLEX by XCMPLX_0:def 2;
then z " = ((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> ) by Def13;
hence ( Re (z " ) = (Re z) / (((Re z) ^2 ) + ((Im z) ^2 )) & Im (z " ) = (- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 )) ) by Th28; :: thesis: verum