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

by
Xiquan Liang

MML identifier: POLYEQ_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, ARYTM_1, ARYTM_3, RELAT_1, SQUARE_1, FUNCT_3, PREPOWER,
POWER, POLYEQ_1, GROUP_1;
notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SQUARE_1, PREPOWER,
POWER, QUIN_1;
constructors REAL_1, NAT_1, SQUARE_1, PREPOWER, POWER, QUIN_1, MEMBERED;
clusters XREAL_0, SQUARE_1, NEWTON, QUIN_1, MEMBERED;
requirements NUMERALS, SUBSET, REAL, ARITHM;

begin :: Polynomial of Degree 1 and 2

reserve a, a', a1, a2, a3, b, b', c, c', d, d', h,
p, q, x, x1, x2, x3, u, v, y, z for real number;

definition let a, b, x be real number;
func Poly1(a ,b ,x) equals
:: POLYEQ_1:def 1

a*x+b;
end;

definition let a, b, x be real number;
cluster Poly1(a ,b ,x) -> real;
end;

definition let a, b, x be Real;
redefine func Poly1(a ,b ,x) -> Real;
end;

theorem :: POLYEQ_1:1
a <> 0 & Poly1(a,b,x) = 0 implies x = -(b/a);

theorem :: POLYEQ_1:2
Poly1(0,0,x) = 0;

theorem :: POLYEQ_1:3
b <> 0 implies not ex x st Poly1(0,b,x) = 0;

definition let a,b,c,x be real number;
func Poly2(a,b,c,x) equals
:: POLYEQ_1:def 2

a*x^2+b*x+c;
end;

definition let a,b,c,x be real number;
cluster Poly2(a,b,c,x) -> real;
end;

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

theorem :: POLYEQ_1:4
(for x holds Poly2(a,b,c,x) = Poly2(a',b',c',x)) implies
a = a'& b = b'& c = c';

theorem :: POLYEQ_1:5
a <> 0 & delta(a,b,c) >= 0 implies
(for x holds Poly2(a,b,c,x) = 0 implies
x = (-b+sqrt delta(a,b,c))/(2*a) or x = (-b-sqrt delta(a,b,c))/(2*a));

theorem :: POLYEQ_1:6
a <> 0 & delta(a,b,c) = 0 &
Poly2(a,b,c,x) = 0 implies x = -(b/(2*a));

theorem :: POLYEQ_1:7
a <> 0 & delta(a,b,c) < 0 implies
not ex x st Poly2(a,b,c,x) = 0;

theorem :: POLYEQ_1:8
b <> 0 & (for x holds Poly2(0,b,c,x) = 0) implies x = -(c/b);

theorem :: POLYEQ_1:9
Poly2(0,0,0,x) = 0;

theorem :: POLYEQ_1:10
c <> 0 implies not ex x st Poly2(0,0,c,x) = 0;

definition let a,x,x1,x2 be real number;
func Quard(a,x1,x2,x) equals
:: POLYEQ_1:def 3

a*((x-x1)*(x-x2));
end;

definition let a,x,x1,x2 be real number;
cluster Quard(a,x1,x2,x) -> real;
end;

definition let a,x,x1,x2 be Real;
redefine func Quard(a,x1,x2,x) -> Real;
end;

theorem :: POLYEQ_1:11
a <> 0 &
(for x holds Poly2(a,b,c,x) = Quard(a,x1,x2,x)) implies
b/a = -(x1+x2) & c/a = x1*x2;

begin :: Polynomial of Degree 3

definition let a,b,c,d,x be real number;
func Poly3(a,b,c,d,x) equals
:: POLYEQ_1:def 4
a*(x |^ 3)+ b*x^2 +c*x +d;
end;

definition let a,b,c,d,x be real number;
cluster Poly3(a,b,c,d,x) -> real;
end;

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

theorem :: POLYEQ_1:12
(for x holds Poly3(a,b,c,d,x) = Poly3(a',b',c',d',x))
implies
a = a' & b = b' & c = c' & d = d';

definition let a,x,x1,x2,x3 be real number;
func Tri(a,x1,x2,x3,x) equals
:: POLYEQ_1:def 5

a*((x-x1)*(x-x2)*(x-x3));
end;

definition let a,x,x1,x2,x3 be real number;
cluster Tri(a,x1,x2,x3,x) -> real;
end;

definition let a,x,x1,x2,x3 be Real;
redefine func Tri(a,x1,x2,x3,x) -> Real;
end;

theorem :: POLYEQ_1:13
a <> 0 &
(for x holds Poly3(a,b,c,d,x) = Tri(a,x1,x2,x3,x)) implies
b/a = -(x1+x2+x3) & c/a = x1*x2 +x2*x3 +x1*x3 & d/a = -x1*x2*x3;

theorem :: POLYEQ_1:14
(y+h) |^ 3 = y |^ 3+((3*h)*y^2+(3*h^2)*y)+h |^ 3;

theorem :: POLYEQ_1:15
a <> 0 & Poly3(a,b,c,d,x) = 0 implies
(for a1,a2,a3,h,y st y = (x+b/(3*a)) & h = -b/(3*a) &
a1 = b/a & a2 = c/a & a3 = d/a holds
y |^ 3 + ((3*h+a1)*y^2+(3*h^2+2*(a1*h)+a2)*y)
+ ((h |^ 3+a1*h^2)+(a2*h+a3)) = 0);

theorem :: POLYEQ_1:16
a <> 0 & Poly3(a,b,c,d,x) = 0 implies
(for a1,a2,a3,h,y st y = (x+b/(3*a)) & h = -b/(3*a)
& a1 = b/a & a2 = c/a & a3 = d/a holds
y |^ 3 + 0*y^2 + ((3*a*c-b^2)/(3*a^2))*y
+ (2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2)) = 0);

theorem :: POLYEQ_1:17
(y |^ 3)+0*y^2+((3*a*c-b^2)/(3*a^2))*y
+ (2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2)) = 0 implies
(for p,q st p = (3*a*c-b^2)/(3*a^2) &
q = 2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2) holds Poly3(1,0,p,q,y) = 0)
;

theorem :: POLYEQ_1:18
Poly3(1,0,p,q,y) = 0 implies
(for u,v st y = u+v & 3*v*u+p = 0 holds u |^ 3 + v |^ 3 = -q
& (u |^ 3)*(v |^ 3) = (-p/3) |^ 3);

theorem :: POLYEQ_1:19
Poly3(1,0,p,q,y) = 0 implies
(for u,v st y = u+v & 3*v*u+p = 0 holds
y = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) +
3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) or
y = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) +
3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) or
y = 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) +
3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)));

theorem :: POLYEQ_1:20
b <> 0 & delta(b,c,d) > 0 &
Poly3(0,b,c,d,x) = 0 implies
x = (-c+sqrt delta(b,c,d))/(2*b) or x = (-c-sqrt delta(b,c,d))/(2*b);

theorem :: POLYEQ_1:21
a <> 0 & p = c/a & q = d/a &
Poly3(a,0,c,d,x) = 0 implies (for u,v st x = u+v & 3*v*u+p = 0
holds
x = 3-root(-d/(2*a)+sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3))
+3-root(-d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) or
x = 3-root(-d/(2*a)+sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3))
+3-root(-d/(2*a)+sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) or
x = 3-root(-d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3))
+3-root(-d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)));

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

theorem :: POLYEQ_1:23
a <> 0 & c/a < 0 &
Poly3(a,0,c,0,x) = 0 implies x = 0 or x = sqrt -c/a or x = -sqrt(-c/a);
```