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

proof

assume ((a * (x ^2 )) + (b * x)) + c > 0 ; :: thesis: x <> - (b / (2 * a))
then ((((2 * a) * x) + b) ^2 ) - 0 > 0 by A1, A2, Th7;
then (2 * a) * x <> - b ;
then x <> (- b) / (2 * a) by A3, XCMPLX_1:88;
hence x <> - (b / (2 * a)) by XCMPLX_1:188; :: thesis: verum

end;

assume x <> - (b / (2 * a)) ; :: thesis: ((a * (x ^2 )) + (b * x)) + c > 0
then x <> (- b) / (2 * a) by XCMPLX_1:188;
then ((2 * a) * x) + b <> 0 by A3, XCMPLX_1:90;
then ((((2 * a) * x) + b) ^2 ) - (delta a,b,c) > 0 by A2, SQUARE_1:74;
hence ((a * (x ^2 )) + (b * x)) + c > 0 by A1, Th23; :: thesis: verum