let a, x, b, c be real number ; :: thesis: ( a > 0 & ((((2 * a) * x) + b) ^2 ) - (delta a,b,c) > 0 implies ((a * (x ^2 )) + (b * x)) + c > 0 )
assume that
A1: a > 0 and
A2: ((((2 * a) * x) + b) ^2 ) - (delta a,b,c) > 0 ; :: thesis: ((a * (x ^2 )) + (b * x)) + c > 0
A3: 4 * a > 0 by A1, XREAL_1:131;
A4: 2 * a <> 0 by A1;
4 * a <> 0 by A1;
then ((((2 * a) * x) + b) ^2 ) - ((4 * a) * ((delta a,b,c) / (4 * a))) > 0 by A2, XCMPLX_1:88;
then ((((2 * a) * x) + ((2 * a) * (b / (2 * a)))) ^2 ) - ((4 * a) * ((delta a,b,c) / (4 * a))) > 0 by A4, XCMPLX_1:88;
then (4 * a) * ((a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a))) > 0 ;
then (a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a)) > 0 / (4 * a) by A3, XREAL_1:85;
hence ((a * (x ^2 )) + (b * x)) + c > 0 by A1, Th1; :: thesis: verum