let x, a, b, c be Real; :: thesis: ( a > 0 & delta (a,b,c) > 0 implies ( ((a * (x ^2)) + (b * x)) + c < 0 iff ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) )
assume that
A1: a > 0 and
A2: delta (a,b,c) > 0 ; :: thesis: ( ((a * (x ^2)) + (b * x)) + c < 0 iff ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )
thus ( ((a * (x ^2)) + (b * x)) + c < 0 implies ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) :: thesis: ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) implies ((a * (x ^2)) + (b * x)) + c < 0 )

proof

assume ((a * (x ^2)) + (b * x)) + c < 0 ; :: thesis: ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) )
then (a * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) < 0 by A1, A2, Th16;
then a * ((x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)))) < 0 ;
then (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) < 0 / a by A1, XREAL_1:81;
then ( ( x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) > 0 & x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) < 0 ) or ( x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) < 0 & x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) > 0 ) ) by XREAL_1:133;
then ( ( x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) by A1, A2, Th25, XREAL_1:47, XREAL_1:48;
hence ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) by XXREAL_0:2; :: thesis: verum

end;

assume ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ; :: thesis: ((a * (x ^2)) + (b * x)) + c < 0
then ( x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) > 0 & x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) < 0 ) by XREAL_1:49, XREAL_1:50;
then (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) < 0 by XREAL_1:132;
then a * ((x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)))) < 0 by A1, XREAL_1:132;
then (a * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) < 0 ;
hence ((a * (x ^2)) + (b * x)) + c < 0 by A1, A2, Th16; :: thesis: verum