The abstract of the Mizar article:

Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients

by

Xiquan Liang

Received May 18, 2000

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);