:: Quadratic Inequalities
:: by Jan Popio\l ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let a, b, c be complex number ;
func delta (a,b,c) ->  set  equals :: QUIN_1:def 1
(b ^2) - ((4 * a) * c);
coherence
 (b ^2) - ((4 * a) * c) is set ;
end;

:: deftheorem  defines delta QUIN_1:def_1_:_
 for a, b, c being complex number holds delta (a,b,c) = (b ^2) - ((4 * a) * c);

registration
let a, b, c be complex number ;
cluster delta (a,b,c) ->  complex ;
coherence
 delta (a,b,c) is complex ;
end;

registration
let a, b, c be real number ;
cluster delta (a,b,c) ->  real ;
coherence
 delta (a,b,c) is real ;
end;

definition
let a, b, c be Real;
:: original:delta
redefine func delta (a,b,c) ->  Real;
coherence
 delta (a,b,c) is Real by XREAL_0:def_1;
end;

theorem Th1: :: QUIN_1:1
for a, b, c, x being complex number st a <> 0 holds
((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))
proofend;

theorem :: QUIN_1:2
for a, b, c, x being real number st a > 0 &amp; delta (a,b,c) <= 0 holds
((a * (x ^2)) + (b * x)) + c >= 0
proofend;

theorem :: QUIN_1:3
for a, b, c, x being real number st a > 0 &amp; delta (a,b,c) < 0 holds
((a * (x ^2)) + (b * x)) + c > 0
proofend;

theorem :: QUIN_1:4
for a, b, c, x being real number st a < 0 &amp; delta (a,b,c) <= 0 holds
((a * (x ^2)) + (b * x)) + c <= 0
proofend;

theorem :: QUIN_1:5
for a, b, c, x being real number st a < 0 &amp; delta (a,b,c) < 0 holds
((a * (x ^2)) + (b * x)) + c < 0
proofend;

theorem Th6: :: QUIN_1:6
for a, x, b, c being real number st a > 0 &amp; ((a * (x ^2)) + (b * x)) + c >= 0 holds
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0
proofend;

theorem Th7: :: QUIN_1:7
for a, x, b, c being real number st a > 0 &amp; ((a * (x ^2)) + (b * x)) + c > 0 holds
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0
proofend;

theorem Th8: :: QUIN_1:8
for a, x, b, c being real number st a < 0 &amp; ((a * (x ^2)) + (b * x)) + c <= 0 holds
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0
proofend;

theorem Th9: :: QUIN_1:9
for a, x, b, c being real number st a < 0 &amp; ((a * (x ^2)) + (b * x)) + c < 0 holds
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0
proofend;

theorem :: QUIN_1:10
for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c >= 0 ) &amp; a > 0 holds
delta (a,b,c) <= 0
proofend;

theorem :: QUIN_1:11
for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c <= 0 ) &amp; a < 0 holds
delta (a,b,c) <= 0
proofend;

theorem :: QUIN_1:12
for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c > 0 ) &amp; a > 0 holds
delta (a,b,c) < 0
proofend;

theorem :: QUIN_1:13
for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c < 0 ) &amp; a < 0 holds
delta (a,b,c) < 0
proofend;

theorem Th14: :: QUIN_1:14
for a, b, c, x being complex number st a <> 0 &amp; ((a * (x ^2)) + (b * x)) + c = 0 holds
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0
proofend;

Lm1:  for a, b being complex number holds
( not a ^2 = b ^2 or a = b or a = - b )
proofend;

theorem :: QUIN_1:15
for a, b, c, x being real number st a <> 0 &amp; delta (a,b,c) >= 0 &amp; ((a * (x ^2)) + (b * x)) + c = 0 &amp; not x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) holds
x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a)
proofend;

theorem Th16: :: QUIN_1:16
for a, b, c, x being real number st a <> 0 &amp; delta (a,b,c) >= 0 holds
((a * (x ^2)) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)))
proofend;

theorem Th17: :: QUIN_1:17
for a, b, c being real number st a < 0 &amp; delta (a,b,c) > 0 holds
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
proofend;

theorem :: QUIN_1:18
for a, b, c, x being real number st a < 0 &amp; delta (a,b,c) > 0 holds
( ((a * (x ^2)) + (b * x)) + c > 0 iff ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x &amp; x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) )
proofend;

theorem :: QUIN_1:19
for a, b, c, x being real number st a < 0 &amp; delta (a,b,c) > 0 holds
( ( 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 )
proofend;

theorem :: QUIN_1:20
for a, b, c, x being complex number st a <> 0 &amp; delta (a,b,c) = 0 &amp; ((a * (x ^2)) + (b * x)) + c = 0 holds
x = - (b / (2 * a))
proofend;

theorem Th21: :: QUIN_1:21
for a, x, b, c being real number st a > 0 &amp; ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds
((a * (x ^2)) + (b * x)) + c > 0
proofend;

theorem :: QUIN_1:22
for a, b, c, x being real number st a > 0 &amp; delta (a,b,c) = 0 holds
( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) )
proofend;

theorem Th23: :: QUIN_1:23
for a, x, b, c being real number st a < 0 &amp; ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds
((a * (x ^2)) + (b * x)) + c < 0
proofend;

theorem :: QUIN_1:24
for a, b, c, x being real number st a < 0 &amp; delta (a,b,c) = 0 holds
( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) )
proofend;

theorem Th25: :: QUIN_1:25
for a, b, c being real number st a > 0 &amp; delta (a,b,c) > 0 holds
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
proofend;

theorem :: QUIN_1:26
for a, b, c, x being real number st a > 0 &amp; delta (a,b,c) > 0 holds
( ((a * (x ^2)) + (b * x)) + c < 0 iff ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x &amp; x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )
proofend;

theorem :: QUIN_1:27
for a, b, c, x being real number st a > 0 &amp; delta (a,b,c) > 0 holds
( ( 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 )
proofend;