let a, b, p, q, s be Real; :: thesis: ( a > 0 & p > 0 & (s - b) / a = (s - q) / (- p) implies ( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) ) )
assume AA: a > 0 ; :: thesis: ( not p > 0 or not (s - b) / a = (s - q) / (- p) or ( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) ) )
assume PP: p > 0 ; :: thesis: ( not (s - b) / a = (s - q) / (- p) or ( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) ) )
assume A4: (s - b) / a = (s - q) / (- p) ; :: thesis: ( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) )
then (s - b) * (- p) = (((s - q) / (- p)) * a) * (- p) by XCMPLX_1:87, AA;
then (s - b) * (- p) = (((s - q) / (- p)) * (- p)) * a ;
then ((- p) * s) - (b * (- p)) = (s - q) * a by XCMPLX_1:87, PP;
then ((a * q) + (b * p)) / (a + p) = (s * (a + p)) / (a + p) ;
then s - b = (((a * q) + (b * p)) / (a + p)) - b by XCMPLX_1:89, AA, PP
.= (((a * q) + (b * p)) / (a + p)) - (b * ((a + p) / (a + p))) by XCMPLX_1:88, AA, PP
.= (((a * q) + (b * p)) / (a + p)) - ((b * (a + p)) / (a + p)) by XCMPLX_1:74
.= (((a * q) + (b * p)) - ((b * a) + (b * p))) / (a + p) by XCMPLX_1:120
.= (a * (q - b)) / (a + p) ;
then (s - b) / a = (a * ((q - b) / (a + p))) / a by XCMPLX_1:74
.= (q - b) / (a + p) by XCMPLX_1:89, AA ;
hence ( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) ) by A4; :: thesis: verum