Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients

by
Xiquan Liang

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

```environ

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

begin

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

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

theorem :: POLYEQ_2:1
for a,c,e,x being real number st a <> 0 &
e <> 0 & c^2 - (4*a*e) > 0 holds
Four(a,0,c,0,e,x) = 0 implies
x <> 0 &
(x = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
x = sqrt((-c - sqrt delta(a,c,e))/(2*a)) or
x = - sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
x = - sqrt((-c - sqrt delta(a,c,e))/(2*a)));

theorem :: POLYEQ_2:2
for a,b,c,x,y being real number st a <> 0 & y = x + 1/x holds
Four(a,b,c,b,a,x) = 0 implies
x <> 0 & a*y^2 + b*y + c - 2*a = 0;

theorem :: POLYEQ_2:3
for a,b,c,x,y being real number st a <> 0 &
b^2-4*a*c + 8*a^2 > 0 & y = x + 1/x holds
Four(a,b,c,b,a,x) = 0 implies
(for y1,y2 being real number st
y1 = (-b+sqrt(b^2-4*a*c+8*a^2))/(2*a) &
y2 = (-b-sqrt(b^2-4*a*c+8*a^2))/(2*a) holds
x <> 0 &
(x = (y1 + sqrt delta(1,(-y1),1))/2 or
x = (y2 + sqrt delta(1,(-y2),1))/2 or
x = (y1 - sqrt delta(1,(-y1),1))/2 or
x = (y2 - sqrt delta(1,(-y2),1))/2));

theorem :: POLYEQ_2:4
for x being real number holds
x|^ 3 = x^2*x & (x|^ 3)*x = x|^ 4 & x^2*x^2 = x|^ 4;

theorem :: POLYEQ_2:5
for x,y being real number st x+y <> 0 holds
(x+y)|^ 4 = (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*x
+ (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*y;

theorem :: POLYEQ_2:6
for x,y being real number st x+y <> 0 holds
(x+y)|^ 4 = x|^ 4+((4*y)*(x|^ 3)+6*y^2*x^2+4*(y|^ 3)*x)+y|^ 4;

theorem :: POLYEQ_2:7
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x)) implies
a5=b5 & a1-a2+a3-a4 = b1-b2+b3-b4 & a1+a2+a3+a4 = b1+b2+b3+b4;

theorem :: POLYEQ_2:8
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x)=Four(b1,b2,b3,b4,b5,x)) implies
a1-b1=b3-a3 & a2-b2=b4-a4;

theorem :: POLYEQ_2:9
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number st
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x)) holds
a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5;

definition let a1,x1,x2,x3,x4,x be real number;
func Four0(a1,x1,x2,x3,x4,x) equals
:: POLYEQ_2:def 2
a1*((x-x1)*(x-x2)*(x-x3)*(x-x4));
end;

definition let a1,x1,x2,x3,x4,x be real number;
cluster Four0(a1,x1,x2,x3,x4,x) -> real;
end;

theorem :: POLYEQ_2:10
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being real number st a1 <> 0 holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x))
implies
(a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1
= x^2*x^2-(x1+x2+x3)*(x^2*x)+(x1*x3+x2*x3+x1*x2)*x^2
- (x1*x2*x3)*x-((x-x1)*(x-x2)*(x-x3))*x4;

theorem :: POLYEQ_2:11
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being real number st a1 <> 0 holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x)) implies
(a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1 = x|^ 4-(x1+x2+x3+x4)*x|^ 3
+((x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4)*x^2
-(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4)*x+(x1*x2*x3*x4);

theorem :: POLYEQ_2:12
for a1,a2,a3,a4,a5,x1,x2,x3,x4 being real number st a1 <> 0 &
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x)) holds
a2/a1 = -(x1+x2+x3+x4)
& a3/a1 = (x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4
& a4/a1 = -(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4)
& a5/a1 = x1*x2*x3*x4;

theorem :: POLYEQ_2:13
for a,k,y being real number st a <> 0 holds
(for x being real number holds x|^ 4+a|^ 4 = k*a*x*(x^2+a^2)) implies
y|^ 4 -k*(y|^ 3)-k*y+1 = 0;
```