The abstract of the Mizar article:

Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients

by

Xiquan Liang

Received February 3, 2003

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;