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

Quadratic Inequalities

Jan Popiolek
Warsaw University, Bialystok


Consider a quadratic trinomial of the form $P(x)=ax^2+bx+c$, where $a\ne 0$. The determinant of the equation $P(x)=0$ is of the form $\Delta(a,b,c)=b^2-4ac$. We prove several quadratic inequalities when $\Delta(a,b,c)<0$, $\Delta(a,b,c)=0$ and $\Delta(a,b,c)>0$.

MML Identifier: QUIN_1

The terminology and notation used in this paper have been introduced in the following articles [1] [2]

Contents (PDF format)


[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

Received July 19, 1991

[ Download a postscript version, MML identifier index, Mizar home page]