let x, a, b, c be Real; ( a > 0 & ((a * (x ^2)) + (b * x)) + c >= 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 )
assume that
A1:
a > 0
and
A2:
((a * (x ^2)) + (b * x)) + c >= 0
; ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0
A3:
4 * a <> 0
by A1;
( 4 * a > 0 & (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) >= 0 )
by A1, A2, Th1, XREAL_1:129;
then
(4 * a) * ((a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))) >= 0
by XREAL_1:127;
then A4:
((((2 * a) * x) + ((2 * a) * (b / (2 * a)))) ^2) - ((4 * a) * ((delta (a,b,c)) / (4 * a))) >= 0
;
2 * a <> 0
by A1;
then
((((2 * a) * x) + b) ^2) - ((4 * a) * ((delta (a,b,c)) / (4 * a))) >= 0
by A4, XCMPLX_1:87;
hence
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0
by A3, XCMPLX_1:87; verum