let a, b, c, d, e, f be Real; :: thesis: ( a <> 0 & ((a * b) + (c * d)) + (e * f) = 0 implies b = (- ((c / a) * d)) - ((e / a) * f) )
assume that
A1: a <> 0 and
A2: ((a * b) + (c * d)) + (e * f) = 0 ; :: thesis: b = (- ((c / a) * d)) - ((e / a) * f)
b = (((- c) * d) + ((- e) * f)) / a by A1, A2, XCMPLX_1:89
.= (((- c) * d) / a) + (((- e) * f) / a) by XCMPLX_1:62
.= (((- c) / a) * d) + (((- e) * f) / a) by XCMPLX_1:74
.= (((- c) / a) * d) + (((- e) / a) * f) by XCMPLX_1:74
.= ((- (c / a)) * d) + (((- e) / a) * f) by XCMPLX_1:187
.= ((- (c / a)) * d) + ((- (e / a)) * f) by XCMPLX_1:187 ;
hence b = (- ((c / a) * d)) - ((e / a) * f) ; :: thesis: verum