let a be non zero Real; :: thesis: for b, c, d, e being Real st a * b = c - (d * e) holds
b ^2 = (((c ^2) / (a ^2)) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2) / (a ^2)) * (e ^2))
let b, c, d, e be Real; :: thesis: ( a * b = c - (d * e) implies b ^2 = (((c ^2) / (a ^2)) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2) / (a ^2)) * (e ^2)) )
assume A1: a * b = c - (d * e) ; :: thesis: b ^2 = (((c ^2) / (a ^2)) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2) / (a ^2)) * (e ^2))
b = (a * b) / a by XCMPLX_1:89
.= (c / a) - ((d * e) / a) by A1, XCMPLX_1:120
.= (c / a) - ((d / a) * e) ;
then b ^2 = (((c / a) ^2) - ((2 * (c / a)) * ((d / a) * e))) + (((d / a) * e) ^2)
.= (((c ^2) / (a ^2)) - ((2 * (c / a)) * ((d / a) * e))) + (((d / a) ^2) * (e ^2)) by XCMPLX_1:76
.= (((c ^2) / (a ^2)) - ((2 * ((c / a) * (d / a))) * e)) + (((d ^2) / (a ^2)) * (e ^2)) by XCMPLX_1:76
.= (((c ^2) / (a ^2)) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2) / (a ^2)) * (e ^2)) by XCMPLX_1:76 ;
hence b ^2 = (((c ^2) / (a ^2)) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2) / (a ^2)) * (e ^2)) ; :: thesis: verum