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
( - (delta (a,b,c)) >= - 0 & 4 * a < 0 ) by A1, A2, XREAL_1:27, XREAL_1:134;
then (- (delta (a,b,c))) / (4 * a) <= 0 by XREAL_1:139;
then - ((delta (a,b,c)) / (4 * a)) <= 0 by XCMPLX_1:188;
then A3: (a * ((x + (b / (2 * a))) ^2)) + (- ((delta (a,b,c)) / (4 * a))) <= (a * ((x + (b / (2 * a))) ^2)) + 0 by XREAL_1:9;
a * ((x + (b / (2 * a))) ^2) <= 0 by A1, XREAL_1:65, XREAL_1:133;
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