let x, a, b, c be Real; ( 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:106
.=
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:76
.=
a * (((x + (b / (2 * a))) ^2) - (((sqrt (delta (a,b,c))) ^2) / ((2 * a) ^2)))
by A2, SQUARE_1:def 2
.=
a * (((x + (b / (2 * a))) ^2) - (((sqrt (delta (a,b,c))) / (2 * a)) ^2))
by XCMPLX_1:76
.=
(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:187
.=
(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:187
.=
(a * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) / (2 * a)) - ((sqrt (delta (a,b,c))) / (2 * a))))
by XCMPLX_1:62
.=
(a * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))
by XCMPLX_1:120
;
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