Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

by
Jan Popiolek

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) );

```