let x, a, b, c be Real; ( 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
; ( ((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) ) )
( ((- 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
;
( ((- 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;
verum
end;
assume
( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) )
; ((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; verum