let x, a, b, c be Real; ( 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
; ( ((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)) )
( x <> - (b / (2 * a)) implies ((a * (x ^2)) + (b * x)) + c < 0 )
assume
x <> - (b / (2 * a))
; ((a * (x ^2)) + (b * x)) + c < 0
then
x <> (- b) / (2 * a)
by XCMPLX_1:187;
then
((2 * a) * x) + b <> 0
by A3, XCMPLX_1:89;
then
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0
by A2, SQUARE_1:12;
hence
((a * (x ^2)) + (b * x)) + c < 0
by A1, Th23; verum