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


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 first-degree and second-degree (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 third-degree (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.

MML Identifier: POLYEQ_1

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

Contents (PDF format)

  1. Equation of Degree 1 and 2
  2. Equation of Degree 3


[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]