let a, b, c, x be real number ; ( 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
; ((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)))
; verum