let z1, z2 be Complex; :: thesis: ( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) )
thus Re (z1 / z2) = Re (((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm25
.= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; :: thesis: Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))
thus Im (z1 / z2) = Im (((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm25
.= (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; :: thesis: verum