The abstract of the Mizar article:

Quadratic Inequalities

by

Jan Popiolek

Received July 19, 1991

MML identifier: QUIN_1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, FUNCT_3, SQUARE_1, ARYTM_1, ARYTM_3;
 notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1;
 constructors REAL_1, SQUARE_1, MEMBERED, XBOOLE_0;
 clusters XREAL_0, SQUARE_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

 reserve x, a, b, c for real number;

definition let a,b,c;
  func delta(a,b,c) equals
:: QUIN_1:def 1
   b^2 - 4 * a * c;
end;

definition let a,b,c;
  cluster delta(a,b,c) -> real;
end;

definition let a,b,c be Real;
  redefine func delta(a,b,c) -> Real;
end;

theorem :: QUIN_1:1
  a <> 0 implies
    a * x^2 + b * x + c = a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a);

theorem :: QUIN_1:2
    a > 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c >= 0;

theorem :: QUIN_1:3
    a > 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c > 0;

theorem :: QUIN_1:4
    a < 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c <= 0;

theorem :: QUIN_1:5
    a < 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c < 0;

theorem :: QUIN_1:6
  a > 0 & a * x^2 + b * x + c >= 0 implies (2 * a * x + b)^2
 - delta(a,b,c) >= 0;

theorem :: QUIN_1:7
  a > 0 & a * x^2 + b * x + c > 0 implies (2 * a * x + b)^2 - delta(a,b,c) > 0;

theorem :: QUIN_1:8
  a < 0 & a * x^2 + b * x + c <= 0 implies
    (2 * a * x + b)^2 - delta(a,b,c) >= 0;

theorem :: QUIN_1:9
  a < 0 & a * x^2 + b * x + c < 0 implies (2 * a * x + b)^2 - delta(a,b,c) > 0;

theorem :: QUIN_1:10
    ( for x holds a * x^2 + b * x + c >= 0 ) & a > 0 implies delta(a,b,c) <= 0;

theorem :: QUIN_1:11
    ( for x holds a * x^2 + b * x + c <= 0 ) & a < 0 implies delta(a,b,c) <= 0;

theorem :: QUIN_1:12
    ( for x holds a * x^2 + b * x + c > 0 ) & a > 0 implies delta(a,b,c) < 0;

theorem :: QUIN_1:13
    ( for x holds a * x^2 + b * x + c < 0 ) & a < 0 implies delta(a,b,c) < 0;

theorem :: QUIN_1:14
  a <> 0 & a * x^2 + b * x + c = 0 implies (2 * a * x + b)^2
 - delta(a,b,c) = 0;

theorem :: QUIN_1:15
    a <> 0 & delta(a,b,c) >= 0 & a * x^2 + b * x + c = 0 implies
     x = (- b - sqrt delta(a,b,c))/(2 * a) or
     x = (- b + sqrt delta(a,b,c))/(2 * a);

theorem :: QUIN_1:16
  a <> 0 & delta(a,b,c) >= 0 implies 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));

theorem :: QUIN_1:17
  a < 0 & delta(a,b,c) > 0 implies
     (- b + sqrt delta(a,b,c))/(2 * a) < (- b - sqrt delta(a,b,c))/(2 * a);

theorem :: QUIN_1:18
    ( 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) );

theorem :: QUIN_1:19
    ( a < 0 & delta(a,b,c) > 0 ) implies ( a * x^2 + b * x + c < 0 iff
     x < (- b + sqrt delta(a,b,c))/(2 * a) or
     x > (- b - sqrt delta(a,b,c))/(2 * a) );

canceled 2;

theorem :: QUIN_1:22
    a <> 0 & delta(a,b,c) = 0 & a * x^2 + b * x + c = 0 implies x = - b/(2 * a)
;

theorem :: QUIN_1:23
  a > 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c > 0;

theorem :: QUIN_1:24
    ( a > 0 & delta(a,b,c) = 0 ) implies ( a * x^2 + b * x + c > 0 iff
     x <> - b/(2 * a) );

theorem :: QUIN_1:25
  a < 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c < 0;

theorem :: QUIN_1:26
    ( a < 0 & delta(a,b,c) = 0 ) implies ( a * x^2 + b * x + c < 0 iff
     x <> - b/(2 * a) );

theorem :: QUIN_1:27
  a > 0 & delta(a,b,c) > 0 implies
     (- b + sqrt delta(a,b,c))/(2 * a) > (- b - sqrt delta(a,b,c))/(2 * a);

theorem :: QUIN_1:28
    ( 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) );

theorem :: QUIN_1:29
    ( a > 0 & delta(a,b,c) > 0 ) implies ( a * x^2 + b * x + c > 0 iff
     x < (- b - sqrt delta(a,b,c))/(2 * a) or
     x > (- b + sqrt delta(a,b,c))/(2 * a) );