Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients

Xiquan Liang

Northeast Normal University,
China
Summary.

In this paper, we describe the definition of the first, second, and third degree
algebraic equations and their properties.
In Section 1, we defined the simple firstdegree and seconddegree (quadratic)
equation and discussed the relation between the roots of each equation and
their coefficients. Also, we clarified the form of the root within the range
of real numbers. Furthermore, the extraction of the root using the discriminant
of equation is clarified.
In Section 2, we defined the thirddegree (cubic) equation and clarified the
relation between the three roots of this equation and its coefficient. Also,
the form of these roots for various conditions is discussed. This solution
is known as the Cardano solution.
The terminology and notation used in this paper have been
introduced in the following articles
[1]
[4]
[3]
[2]

Equation of Degree 1 and 2

Equation of Degree 3
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Jan Popiolek.
Quadratic inequalities.
Journal of Formalized Mathematics,
3, 1991.
 [3]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
Journal of Formalized Mathematics,
1, 1989.
Received May 18, 2000
[
Download a postscript version,
MML identifier index,
Mizar home page]