let x, a, b, c be Real; ( 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
; ((a * (x ^2)) + (b * x)) + c < 0
( - (delta (a,b,c)) > 0 & 4 * a < 0 )
by A1, A2, XREAL_1:58, XREAL_1:132;
then
(- (delta (a,b,c))) / (4 * a) < 0
by XREAL_1:142;
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:6;
a * ((x + (b / (2 * a))) ^2) <= 0
by A1, XREAL_1:63, XREAL_1:131;
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; verum