let p, q, r, a1 be Real; :: thesis: ( r <> 0 & q <> 0 implies ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) )
assume that
A1: r <> 0 and
A2: q <> 0 ; :: thesis: ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = (((p * q) + (r * a1)) / (r * q)) / (((r * q) + (p * a1)) / (r * q)) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) + (p * a1)) / (r * q)) by XCMPLX_1:62
.= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by XCMPLX_1:62
.= ((p / r) + ((a1 * r) / (q * r))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A2, XCMPLX_1:91
.= ((p / r) + (a1 / q)) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A1, XCMPLX_1:91
.= ((p / r) + (a1 / q)) / (1 + ((p * a1) / (r * q))) by A1, A2, XCMPLX_1:6, XCMPLX_1:60
.= ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) by XCMPLX_1:76 ;
hence ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) ; :: thesis: verum