let x, a, b, c be Real; :: thesis: ( a > 0 & delta (a,b,c) > 0 implies ( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c > 0 ) )
assume that
A1: a > 0 and
A2: delta (a,b,c) > 0 ; :: thesis: ( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c > 0 )
thus ( not ((a * (x ^2)) + (b * x)) + c > 0 or x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) :: thesis: ( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or 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: ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or 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:83;
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:134;
hence ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) by XREAL_1:47, XREAL_1:48; :: thesis: verum

end;

assume ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ; :: thesis: ((a * (x ^2)) + (b * x)) + c > 0
then A3: ( x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) < 0 or x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) > 0 ) by XREAL_1:49, XREAL_1:50;
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by A1, A2, Th25;
then x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) < x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) by XREAL_1:10;
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 A3, XXREAL_0:2;
then (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) > 0 by XREAL_1:129, XREAL_1:130;
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:129;
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