let z1, z2 be complex number ; :: thesis: ( Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 ) )
assume that
A1: Re z1 = 0 and
A2: ( Re z2 = 0 & Im z2 <> 0 ) ; :: thesis: ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )
A3: ( z1 / z2 = z1 * (z2 " ) & Re (z2 " ) = 0 ) by A2, Th80, XCMPLX_0:def 9;
hence Re (z1 / z2) = - ((Im z1) * (Im (z2 " ))) by A1, Th31
.= - ((Im z1) * (- ((Im z2) " ))) by A2, Th80
.= - (- ((Im z1) * ((Im z2) " )))
.= (Im z1) / (Im z2) by XCMPLX_0:def 9 ;
:: thesis: Im (z1 / z2) = 0
thus Im (z1 / z2) = 0 by A1, A3, Th31; :: thesis: verum