let x, a, b, c be Real; :: thesis: ( a > 0 & delta (a,b,c) <= 0 implies ((a * (x ^2)) + (b * x)) + c >= 0 )

assume that

A1: a > 0 and

A2: delta (a,b,c) <= 0 ; :: thesis: ((a * (x ^2)) + (b * x)) + c >= 0

( - (delta (a,b,c)) >= - 0 & 4 * a > 0 ) by A1, A2, XREAL_1:25, XREAL_1:129;

then (- (delta (a,b,c))) / (4 * a) >= 0 by XREAL_1:136;

then - ((delta (a,b,c)) / (4 * a)) >= 0 by XCMPLX_1:187;

then A3: (a * ((x + (b / (2 * a))) ^2)) + (- ((delta (a,b,c)) / (4 * a))) >= (a * ((x + (b / (2 * a))) ^2)) + 0 by XREAL_1:7;

(x + (b / (2 * a))) ^2 >= 0 by XREAL_1:63;

then a * ((x + (b / (2 * a))) ^2) >= 0 by A1, XREAL_1:127;

then (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) >= 0 by A3, XXREAL_0:2;

hence ((a * (x ^2)) + (b * x)) + c >= 0 by A1, Th1; :: thesis: verum

assume that

A1: a > 0 and

A2: delta (a,b,c) <= 0 ; :: thesis: ((a * (x ^2)) + (b * x)) + c >= 0

( - (delta (a,b,c)) >= - 0 & 4 * a > 0 ) by A1, A2, XREAL_1:25, XREAL_1:129;

then (- (delta (a,b,c))) / (4 * a) >= 0 by XREAL_1:136;

then - ((delta (a,b,c)) / (4 * a)) >= 0 by XCMPLX_1:187;

then A3: (a * ((x + (b / (2 * a))) ^2)) + (- ((delta (a,b,c)) / (4 * a))) >= (a * ((x + (b / (2 * a))) ^2)) + 0 by XREAL_1:7;

(x + (b / (2 * a))) ^2 >= 0 by XREAL_1:63;

then a * ((x + (b / (2 * a))) ^2) >= 0 by A1, XREAL_1:127;

then (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) >= 0 by A3, XXREAL_0:2;

hence ((a * (x ^2)) + (b * x)) + c >= 0 by A1, Th1; :: thesis: verum