let a, b, c, x be real number ; :: thesis: ( a <> 0 & delta a,b,c >= 0 implies ((a * (x ^2 )) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a))) )
assume that
A1: a <> 0 and
A2: delta a,b,c >= 0 ; :: thesis: ((a * (x ^2 )) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a)))
((a * (x ^2 )) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2 )) - (1 * ((delta a,b,c) / (4 * a))) by A1, Th1
.= (a * ((x + (b / (2 * a))) ^2 )) - ((a * (1 / a)) * ((delta a,b,c) / (4 * a))) by A1, XCMPLX_1:107
.= a * (((x + (b / (2 * a))) ^2 ) - ((1 / a) * ((delta a,b,c) / (4 * a))))
.= a * (((x + (b / (2 * a))) ^2 ) - (((delta a,b,c) * 1) / ((4 * a) * a))) by XCMPLX_1:77
.= a * (((x + (b / (2 * a))) ^2 ) - (((sqrt (delta a,b,c)) ^2 ) / ((2 * a) ^2 ))) by A2, SQUARE_1:def 4
.= a * (((x + (b / (2 * a))) ^2 ) - (((sqrt (delta a,b,c)) / (2 * a)) ^2 )) by XCMPLX_1:77
.= (a * (x - ((- (b / (2 * a))) + ((sqrt (delta a,b,c)) / (2 * a))))) * (x - ((- (b / (2 * a))) - ((sqrt (delta a,b,c)) / (2 * a))))
.= (a * (x - (((- b) / (2 * a)) + ((sqrt (delta a,b,c)) / (2 * a))))) * (x - ((- (b / (2 * a))) - ((sqrt (delta a,b,c)) / (2 * a)))) by XCMPLX_1:188
.= (a * (x - (((- b) / (2 * a)) + ((sqrt (delta a,b,c)) / (2 * a))))) * (x - (((- b) / (2 * a)) - ((sqrt (delta a,b,c)) / (2 * a)))) by XCMPLX_1:188
.= (a * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) / (2 * a)) - ((sqrt (delta a,b,c)) / (2 * a)))) by XCMPLX_1:63
.= (a * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) - (sqrt (delta a,b,c))) / (2 * a))) by XCMPLX_1:121 ;
hence ((a * (x ^2 )) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a))) ; :: thesis: verum