let a, b, c, x be real number ; :: 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
A3: - (delta a,b,c) >= - 0 by A2, XREAL_1:27;
4 * a > 0 by A1, XREAL_1:131;
then (- (delta a,b,c)) / (4 * a) >= 0 by A3, XREAL_1:138;
then - ((delta a,b,c) / (4 * a)) >= 0 by XCMPLX_1:188;
then A4: (a * ((x + (b / (2 * a))) ^2 )) + (- ((delta a,b,c) / (4 * a))) >= (a * ((x + (b / (2 * a))) ^2 )) + 0 by XREAL_1:9;
(x + (b / (2 * a))) ^2 >= 0 by XREAL_1:65;
then a * ((x + (b / (2 * a))) ^2 ) >= 0 by A1, XREAL_1:129;
then (a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a)) >= 0 by A4, XXREAL_0:2;
hence ((a * (x ^2 )) + (b * x)) + c >= 0 by A1, Th1; :: thesis: verum