:: Solving Roots of Polynomial Equations of Degree 2 and 3 with
:: Real Coefficients
::  by Liang Xiquan
::
:: Received May 18, 2000
:: Copyright (c) 2000-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, NUMBERS, XREAL_0, XCMPLX_0, RELAT_1, ARYTM_3, REAL_1,
      CARD_1, ARYTM_1, SQUARE_1, FUNCT_3, XXREAL_0, NEWTON, POWER, PREPOWER,
      POLYEQ_1, ABIAN, ORDINAL1;
 notations SUBSET_1,ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1,
      SQUARE_1, NEWTON, PREPOWER, POWER, QUIN_1, XXREAL_0, ABIAN;
 constructors REAL_1, SQUARE_1, NAT_1, MEMBERED, QUIN_1, NEWTON, PREPOWER,
      POWER, ABIAN;
 registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON;
 requirements NUMERALS, SUBSET, REAL, ARITHM, BOOLE;
 equalities SQUARE_1;
 theorems SQUARE_1, PREPOWER, POWER, QUIN_1, NEWTON, XCMPLX_0, XCMPLX_1,
      XREAL_1, XXREAL_0, ABIAN;

begin :: Polynomial of Degree 1 and 2

reserve a, a9, a1, a2, a3, b, b9, c, c9, d, d9, h, p, q, x, x1, x2, x3, u, v,
  y, z for Real;

definition
  let a, b, x be Complex;
  func Polynom (a,b,x) -> number equals
  a*x+b;
  coherence;
end;

registration
  let a, b, x be Complex;
  cluster Polynom(a,b,x) -> complex;
  coherence;
end;

registration
  let a, b, x be Real;
  cluster Polynom(a,b,x) -> real;
  coherence;
end;

theorem
  for a, b, x being Complex holds a <> 0 & Polynom(a,b,x) = 0
  implies x = -(b/a)
proof
  let a, b, x be Complex;
  assume that
A1: a <> 0 and
A2: Polynom(a,b,x) = 0;
  a"*(-b) = a"*(a*x) by A2
    .= (a"*a)*x;
  then 1*x = a"*(-b) by A1,XCMPLX_0:def 7;
  then x = -(a"*b);
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  for x being Complex holds Polynom(0,0,x) = 0;

theorem
  for b being Complex holds b <> 0 implies not ex x being Complex
 st Polynom(0,b,x) = 0;

definition
  let a,b,c,x be Complex;
  func Polynom(a,b,c,x) -> number equals
  a*x^2+b*x+c;
  coherence;
end;

registration
  let a,b,c,x be Real;
  cluster Polynom(a,b,c,x) -> real;
  coherence;
end;

registration
  let a,b,c,x be Complex;
  cluster Polynom(a,b,c,x) -> complex;
  coherence;
end;

theorem Th4:
  for a, b, c, a9, b9, c9 being Complex holds (for x being
  Real holds Polynom(a,b,c,x) = Polynom(a9,b9,c9,x)) implies a = a9& b =
  b9& c = c9
proof
  let a, b, c, a9, b9, c9 be Complex;
  assume
A1: for x being Real holds Polynom(a,b,c,x) = Polynom(a9,b9,c9,x);
  then
A2: Polynom(a,b,c,-1) = Polynom(a9,b9,c9,-1);
  Polynom(a,b,c,0) = Polynom(a9,b9,c9,0) & Polynom(a,b,c,1) = Polynom(a9,
  b9,c9,1) by A1;
  hence thesis by A2;
end;

theorem Th5:
  a <> 0 & delta(a,b,c) >= 0 implies for x holds Polynom(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)
proof
  assume that
A1: a <> 0 and
A2: delta(a,b,c)>=0;
  now
    set e = a*c;
    let y;
    set t = a^2*y^2+(a*b)*y;
    assume Polynom(a,b,c,y) = 0;
    then a*(a*y^2+b*y+c) = a*0;
    then a*(a*y^2)+a*(b*y)+a*c = 0;
    then
A3: t +b^2/4-b^2*4" = -(4*e)*4";
A4: delta(a,b,c) = b^2-4*a*c by QUIN_1:def 1;
A5: now
      assume ((a*y+b/2) -sqrt((b^2-4*(a*c))/4)) =0;
      then (a*y+b/2) = sqrt(b^2-4*(a*c))/2 by A2,A4,SQUARE_1:20,30;
      then a*y = -(b*2" - sqrt(b^2-4*(a*c))*2" )
        .= ((-b)*2" +(sqrt delta(a,b,c)*2")) by A4;
      then y = ((-b)*2" +(sqrt delta(a,b,c)*2")) /a by A1,XCMPLX_1:89
        .= ((-b)*2" +(sqrt delta(a,b,c)*2"))*a" by XCMPLX_0:def 9
        .= (-b +sqrt delta(a,b,c))*(2"*a")
        .= (-b +sqrt delta(a,b,c))*(2*a)" by XCMPLX_1:204;
      hence y = (-b +sqrt delta(a,b,c))/(2*a) by XCMPLX_0:def 9;
    end;
A6: now
      assume (a*y+b/2) +sqrt((b^2-4*(a*c))/4) = 0;
      then (a*y+b/2) = - sqrt((b^2-4*(a*c))/4);
      then a*y+b/2 = -sqrt(b^2-4*(a*c))/2 by A2,A4,SQUARE_1:20,30;
      then a*y = -(b*2" + sqrt(b^2-4*(a*c))*2" )
        .= ((-b)*2" -(sqrt delta(a,b,c)*2")) by A4;
      then y = ((-b)*2" -(sqrt delta(a,b,c)*2")) /a by A1,XCMPLX_1:89
        .= ((-b)*2" -(sqrt delta(a,b,c)*2"))*a" by XCMPLX_0:def 9
        .= (-b -sqrt delta(a,b,c))*(2"*a")
        .= (-b -sqrt delta(a,b,c))*(2*a)" by XCMPLX_1:204;
      hence y = (-b -sqrt delta(a,b,c))/(2*a) by XCMPLX_0:def 9;
    end;
    (b^2-4*(a*c))/4 >= 0/4 by A2,A4,XREAL_1:72;
    then (a*y+b/2)^2 = (sqrt((b^2-4*(a*c))/4))^2 by A3,SQUARE_1:def 2;
    then
    ((a*y+b/2) - sqrt((b^2-4*(a*c))/4))* ((a*y+b/2) + sqrt((b^2-4*(a*c))/
    4)) = 0;
    hence y = (-b+sqrt delta(a,b,c))/(2*a) or y = (-b-sqrt delta(a,b,c))/(2*a)
    by A5,A6,XCMPLX_1:6;
  end;
  hence thesis;
end;

theorem
  for a, b, c, x being Complex holds a <> 0 & delta(a,b,c) = 0 &
  Polynom(a,b,c,x) = 0 implies x = -(b/(2*a))
proof
  let a, b, c, x be Complex;
  assume that
A1: a <> 0 and
A2: delta(a,b,c) = 0;
  set y = x;
  set t = a^2*y^2+(a*b)*y;
A3: b^2-4*a*c = delta(a,b,c) by QUIN_1:def 1;
  assume Polynom(a,b,c,y) = 0;
  then a*(a*y^2+b*y+c) = 0;
  then t +a*c = 0;
  then (a*y)^2+ 2*((a*y)*b*2") + (b/2)^2 = 0 by A2,A3;
  then (a*y+b/2)^2 = 0;
  then a*y+b/2 = 0 by XCMPLX_1:6;
  then y = (- b*2")/a by A1,XCMPLX_1:89
    .= (-1)*(b*2")*a" by XCMPLX_0:def 9
    .= -(b*(2"*a"))*1
    .= -(b*(2*a)") by XCMPLX_1:204;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  delta(a,b,c) < 0 implies not ex x st Polynom(a,b,c,x) = 0
proof
  set e = a*c;
  assume delta(a,b,c) < 0;
  then (b^2-4*a*c) < 0 by QUIN_1:def 1;
  then
A1: (b^2-4*(a*c))*4" < 0 by XREAL_1:132;
  given y such that
A2: Polynom(a,b,c,y) = 0;
  set t = a^2*y^2+(a*b)*y;
  a*(a*y^2+b*y+c) = a*0 by A2;
  then t +b^2/4-(b^2*4"-(4*e)*4") = 0;
  then
A3: (a*y+b/2)^2 = (b^2-4*(a*c))*4";
  then (a*y+b/2) > 0 by A1,XREAL_1:133;
  hence contradiction by A3,A1,XREAL_1:133;
end;

theorem
  for b, c being Complex holds b <> 0 & (for x being Real
  holds Polynom(0,b,c,x) = 0) implies x = -(c/b)
proof
  let b, c be Complex;
  assume
A1: b <> 0;
  set y = x;
  assume for x being Real holds Polynom(0,b,c,x) = 0;
  then Polynom(0,b,c,y) = 0;
  then y = (-c)/b by A1,XCMPLX_1:89
    .= ((-1)*c)*b" by XCMPLX_0:def 9
    .= (-1)*(c*b")
    .= (-1)*(c/b) by XCMPLX_0:def 9;
  hence thesis;
end;

theorem
  for x being Complex holds Polynom(0,0,0,x) = 0;

theorem
  for c being Complex holds c <> 0 implies not ex x being Complex
 st Polynom(0,0,c,x) = 0;

definition
  let a,x,x1,x2 be Complex;
  func Quard(a,x1,x2,x) -> number equals
  a*((x-x1)*(x-x2));
  coherence;
end;

registration
  let a,x,x1,x2 be Real;
  cluster Quard(a,x1,x2,x) -> real;
  coherence;
end;

theorem
  for a, b, c being Complex holds a <> 0 & (for x being Real
 holds Polynom(a,b,c,x) = Quard(a,x1,x2,x)) implies b/a = -(x1+x2) & c/a
  = x1*x2
proof
  let a, b, c be Complex;
  assume
A1: a <> 0;
  assume
A2: for x being Real holds Polynom(a,b,c,x) = Quard(a,x1,x2,x);
  now
    let z be Real;
    set h = z-x1, t = z-x2;
    set e = h*t-z^2;
    Polynom(a,b,c,z) = Quard(a,x1,x2,z) by A2;
    then a*(h*t-z^2) = (b*z+c);
    then e = (b*z+c)/a by A1,XCMPLX_1:89
      .= a"*(b*z+c) by XCMPLX_0:def 9
      .= a"*(b*z)+a"*c;
    then z*z-z*x2-x1*z+x1*x2 = z^2+(a"*b)*z+a"*c;
    then z^2-(x1+x2)*z+x1*x2 = z^2+(b/a)*z+a"*c by XCMPLX_0:def 9
      .= z^2+(b/a)*z+(c/a) by XCMPLX_0:def 9;
    hence Polynom(1,-(x1+x2),x1*x2,z) = Polynom(1,b/a,c/a,z);
  end;
  hence thesis by Th4;
end;

begin :: Polynomial of Degree 3

definition
  let a,b,c,d,x be Complex;
  func Polynom(a,b,c,d,x) -> number equals
  a*(x |^ 3)+ b*x^2 +c*x +d;
  coherence;
end;

registration
  let a,b,c,d,x be Complex;
  cluster Polynom(a,b,c,d,x) -> complex;
  coherence;
end;

registration
  let a,b,c,d,x be Real;
  cluster Polynom(a,b,c,d,x) -> real;
  coherence;
end;

3 = 2*1 + 1;
then

Lm1: 3 is odd by ABIAN:1;

theorem Th12:
  (for x holds Polynom(a,b,c,d,x) = Polynom(a9,b9,c9,d9,x))
  implies a = a9 & b = b9 & c = c9 & d = d9
proof
  (-1) |^ 3 = - (1 |^ (2+1)) by Lm1,POWER:2
    .= - ((1 |^ 2)*1);
  then
A1: (0 |^ 3) = 0 & (-1) |^ 3 = - 1 by NEWTON:11;
A2: 2 |^ 3 = 2 |^ (2+1) .= (2 |^ (1+1))*2 by NEWTON:6
    .= ((2 |^ 1)*2)*2 by NEWTON:6
    .= (2 |^ 1)*(2*2);
  assume
A3: for x holds Polynom(a,b,c,d,x) = Polynom(a9,b9,c9,d9,x);
  then
A4: Polynom(a,b,c,d,2) = Polynom(a9,b9,c9,d9,2);
  Polynom(a,b,c,d,1) = Polynom(a9,b9,c9,d9,1) by A3;
  then a*1 + b*1 +c*1 +d = Polynom(a9,b9,c9,d9,1);
  then
A5: a + b +c +d = a9*1+ b9*1 +c9*1 +d9
    .= a9+ b9 +c9 +d9;
  Polynom(a,b,c,d,0) = Polynom(a9,b9,c9,d9,0) & Polynom(a,b,c,d,-1) =
  Polynom( a9,b9,c9,d9,-1) by A3;
  hence thesis by A5,A1,A4,A2;
end;

definition
  let a,x,x1,x2,x3 be Complex;
  func Tri(a,x1,x2,x3,x) -> number equals
  a*((x-x1)*(x-x2)*(x-x3));
  coherence;
end;

registration
  let a,x,x1,x2,x3 be Real;
  cluster Tri(a,x1,x2,x3,x) -> real;
  coherence;
end;

theorem
  a <> 0 & (for x holds Polynom(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
proof
  assume
A1: a <> 0;
  set t3 = d/a;
  set t2 = c/a;
  set t1 = b/a;
  set d9 = -x1*x2*x3;
  set c9 = x1*x2+x2*x3+x1*x3;
  set b9 = -(x1+x2+x3);
  assume
A2: for x holds Polynom(a,b,c,d,x) = Tri(a,x1,x2,x3,x);
  now
    let x;
    set t = a*(x |^ 3)+ b*x^2 +c*x +d;
    set r8 = ((x-x1)*(x-x2)*(x-x3));
    x |^ 3 = x |^ (2+1) .= (x |^ (1+1))*x by NEWTON:6
      .= ((x |^ 1)*x)*x by NEWTON:6;
    then
A3: x |^ 3 = (x*x)*x;
    Polynom(a,b,c,d,x) = Tri(a,x1,x2,x3,x)by A2;
    then
A4: t/a = r8 by A1,XCMPLX_1:89;
    a"*t = (a"*a)*(x |^ 3)+ (a"*b)*x^2 +a"*(c*x +d)
      .= 1*(x |^ 3)+ (a"*b)*x^2 +((a"*c)*x +a"*d) by A1,XCMPLX_0:def 7
      .= 1*(x |^ 3)+ t1*x^2 +((a"*c)*x +a"*d) by XCMPLX_0:def 9
      .= 1*(x |^ 3)+ t1*x^2 + (t2*x +a"*d) by XCMPLX_0:def 9
      .= 1*(x |^ 3)+ t1*x^2 + (t2*x + t3) by XCMPLX_0:def 9
      .= Polynom(1,t1,t2,t3,x);
    hence Polynom(1,t1,t2,t3,x) = Polynom(1,b9, c9,d9,x) by A4,A3,
XCMPLX_0:def 9;
  end;
  hence thesis by Th12;
end;

theorem Th14:
  (y+h) |^ 3 = y |^ 3+((3*h)*y^2+(3*h^2)*y)+h |^ 3
proof
  (y+h) |^ 3 = (y+h) |^ (2+1);
  then
A1: (y+h) |^ 3 = ((y+h) |^ (1+1))*(y+h) by NEWTON:6
    .= ((y+h) |^ 1*(y+h))*(y+h) by NEWTON:6
    .= ((y+h) |^ 1)*(y+h)^2
    .= ((y+h) to_power 1)*(y^2+2*y*h+h^2) by POWER:41
    .= (y+h)*(y^2+2*y*h+h^2) by POWER:25
    .= y*y^2+((3*h)*y^2+((2+1)*h^2)*y)+h*h^2;
  y |^ 3 = y |^ (2+1) .= (y |^ (1+1))*y by NEWTON:6
    .= (((y |^ 1)*y))*y by NEWTON:6
    .= (y |^ 1)*y^2;
  then
A2: y |^ 3 = (y to_power 1)*y^2by POWER:41;
  h |^ 3 = h |^ (2+1) .= (h |^ (1+1))*h by NEWTON:6
    .= (((h |^ 1)*h))*h by NEWTON:6
    .= (h |^ 1)*h^2
    .= (h to_power 1)*h^2 by POWER:41
    .= h*h^2 by POWER:25;
  hence thesis by A1,A2,POWER:25;
end;

theorem Th15:
  a <> 0 & Polynom(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
proof
  assume
A1: a <> 0;
  assume
A2: Polynom(a,b,c,d,x) = 0;
  let a1,a2,a3,h,y;
  assume that
A3: y = x+ b/(3*a) & h = -b/(3*a) and
A4: a1 = b/a & a2 = c/a & a3 = d/a;
  0 = a"*(a*(x |^ 3)+ b*x^2 +(c*x +d)) by A2
    .= (a"*a)*(x |^ 3)+ a"*(b*x^2) +a"*(c*x +d)
    .= 1*(x |^ 3)+ a"*(b*x^2) +a"*(c*x +d) by A1,XCMPLX_0:def 7
    .= (x |^ 3)+ (a"*b)*x^2 +(a"*c)*x +a"*d
    .= (x |^ 3)+ (b/a)*x^2 +(a"*c)*x +a"*d by XCMPLX_0:def 9
    .= (x |^ 3)+ (b/a)*x^2 +(c/a)*x +a"*d by XCMPLX_0:def 9
    .= (x |^ 3)+ a1*x^2 + a2*x + a3 by A4,XCMPLX_0:def 9;
  then
  0 = y |^ 3 +((3*h)*y^2+(3*h^2)*y)+h |^ 3 + (a1*y^2+2*(a1*h)*y+a1*h^2) +
  a2*(y+h) + a3 by A3,Th14
    .= y |^ 3 +((3*h)*y^2+(3*h^2)*y)+(2*(a1*h)*y+a1*y^2) +(a2*y + ((h |^ 3 +
  a1*h^2)+(a2*h + a3)));
  hence thesis;
end;

theorem
  a <> 0 & Polynom(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
proof
  assume
A1: a <> 0;
  then
A2: 3*a <> 0;
  assume
A3: Polynom(a,b,c,d,x) = 0;
  let a1,a2,a3,h,y;
  assume that
A4: y = (x + b/(3*a)) and
A5: h = -b/(3*a) and
A6: a1 = b/a and
A7: a2 = c/a and
A8: a3 = d/a;
  set p0 = 3*h+a1;
A9: p0 = -(3*(b/(3*a)))+a1 by A5
    .= -(3*((3*a)"*b))+a1 by XCMPLX_0:def 9
    .= -(3*((3"*a")*b))+a1 by XCMPLX_1:204
    .= -(((3*3")*a")*b)+a1
    .= -(b/a)+a1 by XCMPLX_0:def 9;
  set q2 = (h |^ 3 +a1*h^2)+(a2*h + a3);
A10: q2 = 2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2)
  proof
    set t = 3*a;
    set a6 = b/t;
A11: b/a = (3*b)/t by XCMPLX_1:91;
A12: a6 |^ 3 = a6 |^ (2+1) .= (a6 |^ (1+1))*a6 by NEWTON:6
      .= (a6 |^ 1)*a6*a6 by NEWTON:6
      .= (a6 |^ 1)*a6^2
      .= (a6 to_power 1)*a6^2 by POWER:41;
    q2 = ((-b/t) |^ 3 +b/a*(-b/t)^2) +(-(c/a*(b/t)) + d/a) by A5,A6,A7,A8
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(-(b*c)/(t*a) + d/a) by XCMPLX_1:76
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(-(b*c)/(3*a^2) + 1*(d/a))
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(-(b*c)/(3*a^2) + (t/t)*(d/a)) by A2,
XCMPLX_1:60
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) + ((t/t)*(d/a))- (b*c)/(3*a^2)
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) + ((t*d)/(t*a))- (b*c)/(3*a^2) by
XCMPLX_1:76
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(t*d)*(3*a^2)"-(b*c)/(3*a^2) by
XCMPLX_0:def 9
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(t*d)*(3*a^2)"-(b*c)*(3*a^2)" by
XCMPLX_0:def 9
      .= ((-b/t) |^ 3 +b/a*(-b/t)^2) +(t*d-b*c)*(3*a^2)"
      .= (-b/t) |^ (2+1) +b/a*(b/t)^2 +(t*d-b*c)/(3*a^2) by XCMPLX_0:def 9
      .= ((-b/t) |^ (1+1))*(-b/t) +b/a*(b/t)^2 +( t*d-b*c)/(3*a^2) by NEWTON:6
      .= ((-b/t) |^ 1)*(-b/t)*(-b/t) +b/a*(b/t)^2+( t*d-b*c)/(3*a^2) by
NEWTON:6
      .= ((-b/t) |^ 1)*(-b/t)^2 +b/a*(b/t)^2 +( t*d-b*c)/(3*a^2)
      .= ((-b/t) to_power 1)*(-b/t)^2 +b/a*(b/t)^2 +( t*d-b*c)/(3*a^2) by
POWER:41
      .= (-b/t)*(b/t)^2 +b/a*(b/t)^2 +(t*d-b*c)/(3*a^2) by POWER:25
      .= (-b/t)*(b^2/t^2) +b/a*(b/t)^2 +(t*d-b*c)/(3*a^2) by XCMPLX_1:76
      .= ((-b/t)*(b^2/t^2) +b/a*(b^2/t^2)) +(t*d-b*c)/(3*a^2) by XCMPLX_1:76
      .= (( b/a -b/t)*(b^2/t^2)) +(t*d-b*c)/(3*a^2)
      .= (((3*b)*t" -1*b/t)*(b^2/t^2)) +( t*d-b*c)/(3*a^2) by A11,
XCMPLX_0:def 9
      .= (((3*b)*t" -1*b*t")*(b^2/t^2)) +( t*d-b*c)/(3*a^2) by XCMPLX_0:def 9
      .= 2*((b*t")*(b^2/t^2)) +(t*d-b*c)/(3*a^2)
      .= 2*((b/t)*(b^2/t^2)) +(t*d-b*c)/(3*a^2) by XCMPLX_0:def 9
      .= 2*((b/t)*(b/t)^2) +(t*d-b*c)/(3*a^2) by XCMPLX_1:76;
    hence thesis by A12,POWER:25;
  end;
  set p2 = (3*h^2+2*(a1*h)+a2);
A13: p2 = (3*a*c-b^2)/(3*a^2)
  proof
    set t = ((3*a)"*b);
A14: (3*a)/(3*a) = 1 by A2,XCMPLX_1:60;
    p2 = (3*(b/(3*a))^2+2*(a1*-b/(3*a))+a2) by A5
      .= (3*((3*a)"*b)^2+2*(a1*-b/(3*a))+a2) by XCMPLX_0:def 9
      .= ((3*(3*a)")*b)*t+2*(a1*-b/(3*a))+a2
      .= (3*(3"*a")*b)*t+2*(a1*-b/(3*a))+a2 by XCMPLX_1:204
      .= (b/a)*((3*a)"*b)+2*(a1*-b/(3*a))+a2 by XCMPLX_0:def 9
      .= (b/a)*(b/(3*a))+2*(a1*-b/(3*a))+a2 by XCMPLX_0:def 9
      .= (b*b)/(a*(3*a))+2*(a1*-b/(3*a))+a2 by XCMPLX_1:76
      .= b^2/(3*a^2)-2*(b/a*(b/(3*a))) +c/a by A6,A7
      .= b^2/(3*a^2)-2*((b*b)/(a*(3*a))) +c/a by XCMPLX_1:76
      .= -b^2/(3*a^2) +((3*a)/(3*a))*(c/a) by A14
      .= -b^2/(3*a^2) +(3*a*c)/(3*a*a) by XCMPLX_1:76
      .= (3*a*c)/(3*a^2)-b^2/(3*a^2)
      .= (3*a*c)*(3*a^2)"-b^2/(3*a^2) by XCMPLX_0:def 9
      .= (3*a*c)*(3*a^2)"-b^2*(3*a^2)" by XCMPLX_0:def 9
      .= ((3*a*c)-b^2)*(3*a^2)";
    hence thesis by XCMPLX_0:def 9;
  end;
  y |^ 3 +(p0*y^2+p2*y) + q2 = 0 by A1,A3,A4,A5,A6,A7,A8,Th15;
  hence thesis by A6,A9,A13,A10;
end;

theorem
  (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 Polynom(1,0,p,q,y) = 0;

theorem Th18:
  Polynom(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
proof
  assume
A1: Polynom(1,0,p,q,y) = 0;
  let u,v;
  assume that
A2: y = u+v and
A3: 3*v*u+p = 0;
  (u+v) |^ 3 = u |^ 3+((3*v)*u^2+(3*v^2)*u)+v |^ 3 by Th14
    .= u |^ 3+(3*v*u)*(u+v)+v |^ 3;
  then 0 = (u |^ 3+v |^ 3)+((3*v*u + p )*(u+v)) + q by A1,A2;
  hence u |^ 3+v |^ 3 = - q by A3;
  3*(v*u) = - p by A3;
  hence thesis by NEWTON:7;
end;

theorem Th19:
  Polynom(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))
proof
  set e1 = 1;
  assume
A1: Polynom(1,0,p,q,y) = 0;
  set e3 = (-p/3) |^ 3;
  set e2 = q;
  let u,v;
  assume that
A2: y = u+v and
A3: 3*v*u+p = 0;
  set z2 = v |^ 3;
  set z1 = u |^ 3;
A4: now
    let z;
    thus (z-z1)*(z-z2)= z^2-(z1+z2)*z+z1*z2
      .= z^2-(-q)*z+z1*z2 by A1,A2,A3,Th18
      .= z^2+q*z+(-p/3) |^ 3 by A1,A2,A3,Th18;
  end;
A5: z1+ z2 = -q by A1,A2,A3,Th18;
  then e2^2 = (z1+z2)^2 by SQUARE_1:3;
  then
A6: e2^2-(4*e1*e3) = -(-(z1^2+2*z1*z2+z2^2))-4*(z1*z2) by A1,A2,A3,Th18
    .= (z1-z2)^2;
  then
A7: (e2^2-4*e1*e3)>= 0 by XREAL_1:63;
  then
A8: delta(e1,e2,e3) >= 0 by QUIN_1:def 1;
  (z1-z1)*(z1-z2)= 0*(z1-z2);
  then
A9: Polynom(e1,e2,e3,z1) = 0 by A4;
  (z2-z1)*(z2-z2) = (z2-z1)*0;
  then
A10: Polynom(e1,e2,e3,z2) = 0 by A4;
A11: z2*z1 = (-p/3) |^ 3 by A1,A2,A3,Th18;
  now
    per cases by A9,A8,Th5;
    case
A12:  z1 = (-e2+sqrt delta(e1,e2,e3))/(2*e1);
A13:  (p/3) |^ 3 = (p/3) |^ (2+1) .= ((p/3) |^ (1+1))*(p/3) by NEWTON:6
        .= ((((p/3) |^ 1)*(p/3)))*(p/3) by NEWTON:6
        .= ((p/3) |^ 1)*(p/3)^2
        .= ((p/3) to_power 1)*(p/3)^2by POWER:41
        .= (p/3)*(p/3)^2 by POWER:25;
A14:  (q^2-4*(-p/3) |^ 3)>= 0 by A6,XREAL_1:63;
A15:  (-p/3) |^ 3 = (-p/3) |^ (2+1) .= ((-p/3) |^ (1+1))*(-p/3) by NEWTON:6
        .= ((((-p/3) |^ 1)*(-p/3)))*(-p/3) by NEWTON:6
        .= ((-p/3) |^ 1)*(-p/3)^2;
      then
A16:  (-p/3) |^ 3 = ((-p/3) to_power 1)*(-p/3)^2 by POWER:41
        .= (-p/3)*(p/3)^2 by POWER:25
        .= -((p/3)*(p/3)^2);
A17:  z1 = (-e2+sqrt(e2^2-4*e1*e3))/(2*e1) by A12,QUIN_1:def 1
        .= (-q)/2 +sqrt(q^2-4*(-p/3) |^ 3)/sqrt 4 by SQUARE_1:20,XCMPLX_1:62
        .= (-q)/2 +sqrt((q^2-4*(-p/3) |^ 3)/4) by A14,SQUARE_1:30
        .= (-q)/2 +sqrt(q^2/4-1*(-p/3) |^ 3);
A18:  now
        per cases by XXREAL_0:1;
        case
A19:      u >0;
          then
A20:      (-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A17,A16,A13,PREPOWER:6;
          then u = 3 -Root (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A17,A16,A13,A19,
PREPOWER:def 2;
          hence u = 3-root(-q/2 +sqrt(q^2 /4+(p/3) |^ 3)) by A20,POWER:def 1;
        end;
        case
A21:      u =0;
          then
A22:      -q/2 +sqrt(q^2/4+(p/3) |^ 3) = 0 by A17,A16,A13,NEWTON:11;
          then 3 -Root (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) = 0 by PREPOWER:def 2;
          hence u = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A21,A22,POWER:def 1
;
        end;
        case
          u <0;
          then
A23:      -u > 0 by XREAL_1:58;
          set r = (-q/2 +sqrt(q^2/4+(p/3) |^ 3));
A24:      (3-root (-1)) = -1 by Lm1,POWER:8;
          (-u) |^ 3 = (-u) |^ (2+1) .= ((-u) |^ (1+1))*(-u) by NEWTON:6
            .= ((((-u) |^ 1)*(-u)))*(-u) by NEWTON:6
            .= ((-u) |^ 1)*(-u)^2;
          then (-u) |^ 3 = ((-u) to_power 1)*(-u)^2by POWER:41;
          then
A25:      (-u) |^ 3 = (-u)*u^2 by POWER:25
            .= -((u)*u^2);
          u |^ 3 = u |^ (2+1) .= (u |^ (1+1))*u by NEWTON:6
            .= ((u |^ 1)*u)*u by NEWTON:6
            .= (u |^ 1)*(u*u);
          then
A26:      u |^ 3 = (u to_power 1)*u^2 by POWER:41;
          then
A27:      (-u) |^ 3 = -(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A17,A16,A13,A25,
POWER:25;
A28:      (-u) |^ 3 = -(u |^ 3) by A25,A26,POWER:25;
          then
A29:      -(-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A17,A16,A13,A23,PREPOWER:6;
          -(u |^ 3)> 0 by A23,A28,PREPOWER:6;
          then
          (-u) = 3 -Root(-(-q/2 +sqrt(q^2/4+(p/3) |^ 3))) by A17,A16,A13,A23
,A27,PREPOWER:def 2;
          then (-u) = 3-root((-1)*(r)) by A29,POWER:def 1;
          then (-u) = (3-root (-1))*(3-root r) by Lm1,POWER:11;
          hence u = 3-root(-q/2 +sqrt ( q^2/4+(p/3) |^ 3)) by A24;
        end;
      end;
      now
        per cases by A8,A10,Th5;
        case
          z2 = (-e2+sqrt delta(e1,e2,e3))/(2*e1);
          then z2 = (-e2+sqrt(e2^2-4*e1*e3))/(2*e1) by QUIN_1:def 1;
          then z2 = (-q)/2 +sqrt(q^2-4*(-p/3) |^ 3)/sqrt 4 by SQUARE_1:20
,XCMPLX_1:62;
          then
A30:      z2 = (-q)/2 +sqrt((q^2-4*(-p/3) |^ 3)/4) by A7,SQUARE_1:30
            .= (-q)/2 +sqrt(q^2/4-1*(-p/3) |^ 3);
A31:      (-p/3) |^ 3 = ((-p/3) to_power 1)*(-p/3)^2by A15,POWER:41
            .= (-p/3)*(p/3)^2 by POWER:25;
          now
            per cases by XXREAL_0:1;
            case
A32:          v >0;
              then
A33:          (-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A13,A30,A31,PREPOWER:6;
              then v = 3 -Root (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A13,A30,A31
,A32,PREPOWER:def 2;
              hence v = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A33,POWER:def 1
;
            end;
            case
A34:          v=0;
              then (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) = 0 by A13,A30,A31,NEWTON:11;
              hence v = 3-root(-q/2 +sqrt( q^2/4+(p/3) |^ 3)) by A34,POWER:5;
            end;
            case
              v<0;
              then
A35:          -v > 0 by XREAL_1:58;
              then
A36:          (-v) |^ 3 > 0 by PREPOWER:6;
              (-v) |^ 3 = (-v) |^ (2+1);
              then (-v) |^ 3 = ((-v) |^ (1+1))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((((-v) |^ 1)*(-v)))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((-v) |^ 1)*((-v)*(-v));
              then (-v) |^ 3 = ((-v) to_power 1)*(-v)^2by POWER:41;
              then (-v) |^ 3 = (-v)*(-v)^2 by POWER:25;
              then
A37:          (-v) |^ 3 = -(v*v^2);
              v |^ 3 = v |^ (2+1);
              then v |^ 3 = (v |^ (1+1))*v by NEWTON:6;
              then v |^ 3 = ((v |^ 1)*v)*v by NEWTON:6;
              then v |^ 3 = (v |^ 1)*(v*v);
              then
A38:          v |^ 3 = (v to_power 1)*v^2 by POWER:41;
              then
              (-v) |^ 3 = -(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A13,A30,A31,A37,
POWER:25;
              then
A39:          (-v) = 3 -Root(-(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) ) by A35,A36,
PREPOWER:def 2;
              set r = (-q/2 +sqrt(q^2/4+(p/3) |^ 3));
A40:          (3-root (-1)) = -1 by Lm1,POWER:8;
              -(-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A13,A30,A31,A36,A37,A38,
POWER:25;
              then (-v) = 3-root((-1)*(r)) by A39,POWER:def 1;
              then (-v) = (3-root(-1))*(3-root r) by Lm1,POWER:11;
              hence v = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A40;
            end;
          end;
          hence thesis by A2,A18;
        end;
        case
          z2 = (-e2-sqrt delta(e1,e2,e3))/(2*e1);
          then z2 = (-e2-sqrt(e2^2-4*e1*e3))/(2*e1) by QUIN_1:def 1;
          then z2 = (-q)/2 -(sqrt(q^2-4*(-p/3) |^ 3))/2;
          then
A41:      z2 = -q/2 -sqrt((q^2-4*(-p/3) |^ 3)/4) by A7,SQUARE_1:20,30
            .= -q/2 -sqrt(q^2/4-1*(-p/3) |^ 3);
          now
            per cases by XXREAL_0:1;
            case
A42:          v>0;
              then (-q/2 -sqrt(q^2/4+(p/3) |^ 3))> 0 by A16,A13,A41,PREPOWER:6;
              then
A43:          v = 3 -Root (-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A16,A13,A41,A42,
PREPOWER:def 2;
              (-q/2 -sqrt(q^2/4+(p/3) |^ 3))> 0 by A16,A13,A41,A42,PREPOWER:6;
              hence v = 3-root (-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A43,
POWER:def 1;
            end;
            case
A44:          v=0;
              then
A45:          (-q/2 -sqrt(q^2/4+(p/3) |^ 3)) = 0 by A16,A13,A41,NEWTON:11;
              hence v = 3 -Root (-q/2 -sqrt (q^2/4+(p/3) |^ 3)) by A44,
PREPOWER:def 2;
              hence v = 3-root (-q/2 -sqrt(q ^2 /4+(p/3) |^ 3))by A45,
POWER:def 1;
            end;
            case
              v<0;
              then
A46:          -v > 0 by XREAL_1:58;
              set r = (-q/2 -sqrt(q^2/4+(p/3) |^ 3));
A47:          (3-root (-1)) = -1 by Lm1,POWER:8;
              v |^ 3 = v |^ (2+1);
              then v |^ 3 = (v |^ (1+1))*v by NEWTON:6;
              then
A48:          v |^ 3 = ((v |^ 1)*v)*v by NEWTON:6;
              (-v) |^ 3 = (-v) |^ (2+1);
              then (-v) |^ 3 = ((-v) |^ (1+1))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((((-v) |^ 1)*(-v)))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((-v) |^ 1)*((-v)*(-v));
              then
A49:          (-v) |^ 3 = ((-v) to_power 1)*(-v)^2 by POWER:41
                .= (-v)*v^2 by POWER:25
                .= -(v*v^2);
              (-v) |^ 3 = -(v |^ 3) by A49,A48;
              then
A50:          -(-q/2 -sqrt(q^2/4+(p/3) |^ 3))> 0 by A16,A13,A41,A46,PREPOWER:6;
              (-v) |^ 3 = -(-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A16,A13,A41,A49
,A48;
              then (-v) = 3 -Root(-(-q/2 -sqrt(q^2/4+(p/3) |^ 3)) ) by A46,A50,
PREPOWER:def 2;
              then (-v) = 3-root((-1)*(r)) by A50,POWER:def 1;
              then (-v) = (3-root (-1))*(3-root r) by Lm1,POWER:11;
              hence v = 3-root(-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A47;
            end;
          end;
          hence thesis by A2,A18;
        end;
      end;
      hence thesis;
    end;
    case
A51:  z1 = (-e2-sqrt delta(e1,e2,e3))/(2*e1);
      (-p/3) |^ 3 = (-p/3) |^ (2+1);
      then (-p/3) |^ 3 = ((-p/3) |^ (1+1))*(-p/3) by NEWTON:6;
      then (-p/3) |^ 3 = ((((-p/3) |^ 1)*(-p/3)))*(-p/3) by NEWTON:6;
      then (-p/3) |^ 3 = ((-p/3) |^ 1)*((-p/3)*(-p/3));
      then (-p/3) |^ 3 = ((-p/3) to_power 1)*(-p/3)^2 by POWER:41;
      then (-p/3) |^ 3 = (-p/3)*(-p/3)^2 by POWER:25;
      then
A52:  (-p/3) |^ 3 = -((p/3)*(p/3)^2);
      z1 = (-e2-sqrt(e2^2-4*e1*e3))/(2*e1) by A51,QUIN_1:def 1;
      then
A53:  z1= ((-q)*2") -(sqrt(q^2-4*(-p/3) |^ 3))/2
        .= -q/2 -sqrt((q^2-4*(-p/3) |^ 3)/4) by A7,SQUARE_1:20,30
        .= -q/2 -sqrt(q^2/4-1*(-p/3) |^ 3);
      hence z1 = -q/2 -sqrt(q^2/4-(-p/3) |^ 3);
      (p/3) |^ 3 = (p/3) |^ (2+1);
      then (p/3) |^ 3 = ((p/3) |^ (1+1))*(p/3) by NEWTON:6;
      then (p/3) |^ 3 = ((((p/3) |^ 1)*(p/3)))*(p/3) by NEWTON:6;
      then (p/3) |^ 3 = ((p/3) |^ 1)*((p/3)*(p/3));
      then (p/3) |^ 3 = ((p/3) to_power 1)*(p/3)^2by POWER:41;
      then
A54:  (-p/3) |^ 3 = -((p/3) |^ 3) by A52,POWER:25;
A55:  now
        per cases by XXREAL_0:1;
        case
A56:      u >0;
          then (-q/2 -sqrt(q^2/4+(p/3) |^ 3))> 0 by A53,A54,PREPOWER:6;
          then
A57:      u = 3 -Root (-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A53,A54,A56,
PREPOWER:def 2;
          (-q/2 -sqrt(q^2 /4+(p/3) |^ 3))> 0 by A53,A54,A56,PREPOWER:6;
          hence u = 3-root (-q/2 - sqrt(q^2/4+(p/3) |^ 3)) by A57,POWER:def 1;
        end;
        case
A58:      u =0;
          then (-q/2 -sqrt(q^2/4+(p/3) |^ 3)) = 0 by A53,A54,NEWTON:11;
          hence u = 3-root(-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A58,POWER:5;
        end;
        case
          u <0;
          then
A59:      -u > 0 by XREAL_1:58;
          then
A60:      (-u) |^ 3 > 0 by PREPOWER:6;
          (-u) |^ 3 = (-u) |^ (2+1);
          then (-u) |^ 3 = ((-u) |^ (1+1))*(-u) by NEWTON:6;
          then (-u) |^ 3 = ((((-u) |^ 1)*(-u)))*(-u) by NEWTON:6;
          then (-u) |^ 3 = ((-u) |^ 1)*((-u)*(-u));
          then (-u) |^ 3 = ((-u) to_power 1)*(-u)^2 by POWER:41;
          then (-u) |^ 3 = (-u)*(-u)^2 by POWER:25;
          then
A61:      (-u) |^ 3 = -(u*u^2);
          u |^ 3 = u |^ (2+1);
          then u |^ 3 = (u |^ (1+1))*u by NEWTON:6;
          then u |^ 3 = ((u |^ 1)*u)*u by NEWTON:6;
          then u |^ 3 = (u |^ 1)*(u*u);
          then
A62:      u |^ 3 = (u to_power 1)*u^2 by POWER:41;
          then -(-q/2 -sqrt(q^2/4+(p/3) |^ 3))> 0 by A53,A54,A60,A61,POWER:25;
          then
A63:      3 -Root(-(-q/2 -sqrt(q^2/4+(p/3) |^ 3))) = 3-root(-(-q/2 -sqrt
          (q^2/4+(p/3) |^ 3))) by POWER:def 1;
          set r = (-q/2 -sqrt(q^2/4+(p/3) |^ 3));
          (-u) |^ 3 = -(-q/2 -sqrt(q^2/4+(p/3) |^ 3)) by A53,A54,A61,A62,
POWER:25;
          then (-u) = 3-root((-1)*(r)) by A59,A60,A63,PREPOWER:def 2;
          then
A64:      (-u) = (3-root (-1))*(3-root r) by Lm1,POWER:11;
          (3-root (-1)) = -1 by Lm1,POWER:8;
          hence u = 3-root(-q / 2 -sqrt(q^2/4+(p/3) |^ 3)) by A64;
        end;
      end;
      now
        per cases by A8,A10,Th5;
        case
A65:      z2 = (-e2+sqrt delta(e1,e2,e3))/(2*e1);
          (-p/3) |^ 3 = (-p/3) |^ (2+1);
          then (-p/3) |^ 3 = ((-p/3) |^ (1+1))*(-p/3) by NEWTON:6;
          then (-p/3) |^ 3 = ((((-p/3) |^ 1)*(-p/3)))*(-p/3) by NEWTON:6;
          then (-p/3) |^ 3 = ((-p/3) |^ 1)*((-p/3)*(-p/3));
          then (-p/3) |^ 3 = ((-p/3) to_power 1)*(-p/3)^2by POWER:41;
          then (-p/3) |^ 3 = (-p/3)*(-p/3)^2 by POWER:25;
          then
A66:      (-p/3) |^ 3 = -((p/3)*(p/3)^2);
          (p/3) |^ 3 = (p/3) |^ (2+1);
          then (p/3) |^ 3 = ((p/3) |^ (1+1))*(p/3) by NEWTON:6;
          then (p/3) |^ 3 = ((((p/3) |^ 1)*(p/3)))*(p/3) by NEWTON:6;
          then (p/3) |^ 3 = ((p/3) |^ 1)*((p/3)*(p/3));
          then (p/3) |^ 3 = ((p/3) to_power 1)*(p/3)^2by POWER:41;
          then
A67:      (-p/3) |^ 3 = -((p/3) |^ 3) by A66,POWER:25;
          z2 = (-e2+sqrt(e2^2-4*e1*e3))/(2*e1) by A65,QUIN_1:def 1;
          then z2 = (-q)/2 +sqrt(q^2-4*(-p/3) |^ 3)/sqrt 4 by SQUARE_1:20
,XCMPLX_1:62;
          then
A68:      z2 = (-q)/2 +sqrt((q^2-4*(-p/3) |^ 3)/4) by A7,SQUARE_1:30
            .= (-q)/2 +sqrt(q^2/4-1*(-p/3) |^ 3);
          now
            per cases by XXREAL_0:1;
            case
A69:          v >0;
              then
A70:          (-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A68,A67,PREPOWER:6;
              then v = 3 -Root (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A68,A67,A69,
PREPOWER:def 2;
              hence v = 3-root(-q/2 + sqrt(q^2/4+(p/3) |^ 3)) by A70,
POWER:def 1;
            end;
            case
A71:          v=0;
              then (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) = 0 by A68,A67,NEWTON:11;
              hence v = 3-root(-q/2 +sqrt(q^2/ 4+(p/3) |^ 3)) by A71,POWER:5;
            end;
            case
              v<0;
              then
A72:          -v > 0 by XREAL_1:58;
              then
A73:          (-v) |^ 3 > 0 by PREPOWER:6;
              (-v) |^ 3 = (-v) |^ (2+1);
              then (-v) |^ 3 = ((-v) |^ (1+1))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((((-v) |^ 1)*(-v)))*(-v) by NEWTON:6;
              then (-v) |^ 3 = ((-v) |^ 1)*((-v)*(-v));
              then (-v) |^ 3 = ((-v) to_power 1)*(-v)^2by POWER:41;
              then (-v) |^ 3 = (-v)*(-v)^2 by POWER:25;
              then
A74:          (-v) |^ 3 = -(v*v^2);
              v |^ 3 = v |^ (2+1);
              then v |^ 3 = (v |^ (1+1))*v by NEWTON:6;
              then v |^ 3 = ((v |^ 1)*v)*v by NEWTON:6;
              then v |^ 3 = (v |^ 1)*(v*v);
              then
A75:          v |^ 3 = (v to_power 1)*v^2 by POWER:41;
              then
A76:          -(-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A68,A67,A73,A74,POWER:25;
              set r = (-q/2 +sqrt(q^2/4+(p/3) |^ 3));
A77:          (3-root (-1)) = -1 by Lm1,POWER:8;
              v |^ 3 = v*v^2 by A75,POWER:25;
              then (-v) = 3 -Root(-(-q/2 +sqrt(q^2/4+(p/3) |^ 3))) by A68,A67
,A72,A73,A74,PREPOWER:def 2;
              then (-v) = 3-root((-1)*(r)) by A76,POWER:def 1;
              then (-v) = (3-root(-1))*(3-root r) by Lm1,POWER:11;
              hence v = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A77;
            end;
          end;
          hence thesis by A2,A55;
        end;
        case
A78:      z2 = (-e2-sqrt delta(e1,e2,e3))/(2*e1);
          e2^2 = (z1+z2)^2 by A5,SQUARE_1:3;
          then
A79:      e2^2-(4*e1*e3) = (z1-z2)^2 by A11;
          (-p/3) |^ 3 = (-p/3) |^ (2+1)
            .= ((-p/3) |^ (1+1))*(-p/3) by NEWTON:6
            .= ((((-p/3) |^ 1)*(-p/3)))*(-p/3) by NEWTON:6
            .= ((-p/3) |^ 1)*((-p/3)*(-p/3));
          then (-p/3) |^ 3 = ((-p/3) to_power 1)*(-p/3)^2by POWER:41
            .= (-p/3)*(p/3)^2 by POWER:25;
          then
A80:      (-p/3) |^ 3 = -((p/3)*(p/3)^2);
          (p/3) |^ 3 = (p/3) |^ (2+1) .= ((p/3) |^ (1+1))*(p/3) by NEWTON:6
            .= ((((p/3) |^ 1)*(p/3)))*(p/3) by NEWTON:6
            .= ((p/3) |^ 1)*(p/3)^2;
          then (p/3) |^ 3 = ((p/3) to_power 1)*(p/3)^2by POWER:41;
          then
A81:      (-p/3) |^ 3 = -((p/3) |^ 3) by A80,POWER:25;
          z2 = (-e2-sqrt(e2^2-4*e1*e3))/(2*e1) by A78,QUIN_1:def 1;
          then
A82:      z2 = (-q)/2 +sqrt((q^2-4*(-p/3) |^ 3)/4) by A51,A78,A79,SQUARE_1:17
            .= (-q)/2 +sqrt(q^2/4-1*(-p/3) |^ 3);
          now
            per cases by XXREAL_0:1;
            case
A83:          v >0;
              then
A84:          (-q/2 +sqrt(q^2/4+(p/3) |^ 3))> 0 by A82,A81,PREPOWER:6;
              then v = 3 -Root (-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A82,A81,A83,
PREPOWER:def 2;
              hence v = 3-root(-q/2 +sqrt (q^2/4+(p/3) |^ 3)) by A84,
POWER:def 1;
            end;
            case
A85:          v=0;
              then v |^ 3 = 0 by NEWTON:11;
              hence
              v = 3-root(-q/2 +sqrt(q ^2/4+(p/3) |^ 3)) by A82,A81,A85,POWER:5;
            end;
            case
              v<0;
              then
A86:          -v > 0 by XREAL_1:58;
              then
A87:          (-v) |^ 3 > 0 by PREPOWER:6;
              set r = (-q/2 +sqrt(q^2/4+(p/3) |^ 3));
              v |^ 3 = v |^ (2+1) .= (v |^ (1+1))*v by NEWTON:6
                .= ((v |^ 1)*v)*v by NEWTON:6
                .= (v |^ 1)*v^2;
              then
A88:          v |^ 3 = (v to_power 1)*v^2 by POWER:41;
              (-v) |^ 3 = (-v) |^ (2+1) .= ((-v) |^ (1+1))*(-v) by NEWTON:6
                .= ((((-v) |^ 1)*(-v)))*(-v) by NEWTON:6
                .= ((-v) |^ 1)*(-v)^2
                .= ((-v) to_power 1)*(-v)^2by POWER:41
                .= (-v)*v^2 by POWER:25;
              then
A89:          (-v) |^ 3 = -(v*v^2);
              then
A90:          -(v |^ 3)> 0 by A87,A88,POWER:25;
A91:          (3-root (-1)) = -1 by Lm1,POWER:8;
              (-v) |^ 3 = -(v |^ 3) by A89,A88,POWER:25;
              then (-v) = 3 -Root(-(-q/2 +sqrt(q^2/4+(p/3) |^ 3))) by A82,A81
,A86,A87,PREPOWER:def 2;
              then (-v) = 3-root((-1)*(r)) by A82,A81,A90,POWER:def 1;
              then (-v) = (3-root(-1))*(3-root r) by Lm1,POWER:11;
              hence v = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) by A91;
            end;
          end;
          hence
          y = 3-root(-q/2 +sqrt(q^2/4+(p/3) |^ 3)) +3-root(-q/2 -sqrt(q^2
          /4+(p/3) |^ 3)) by A2,A55;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem
  b <> 0 & delta(b,c,d) > 0 & Polynom(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)
proof
  assume
A1: b <> 0 & delta(b,c,d)>0;
  assume Polynom(0,b,c,d,x) = 0;
  then Polynom(b,c,d,x) = 0;
  hence thesis by A1,Th5;
end;

theorem
  a <> 0 & p = c/a & q = d/a & Polynom(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))
proof
  assume that
A1: a <> 0 and
A2: p = c/a and
A3: q = d/a;
A4: p/3 = c/(3*a) & -q/2 = -d/(2*a) by A2,A3,XCMPLX_1:78;
  assume Polynom(a,0,c,d,x) = 0;
  then a"*(a*(x |^ 3)+c*x +d) = 0;
  then (a"*a)*(x |^ 3)+a"*(c*x +d)= 0;
  then 1*(x |^ 3)+a"*(c*x +d)= 0 by A1,XCMPLX_0:def 7;
  then (x |^ 3)+((a"*c)*x +a"*d) = 0;
  then (x |^ 3)+((c/a)*x +a"*d) = 0 by XCMPLX_0:def 9;
  then (x |^ 3)+((c/a)*x +d/a) = 0 by XCMPLX_0:def 9;
  then
A5: Polynom(1,0,p,q,x) = 0 by A2,A3;
  q^2/4 = d^2/a^2/4 by A3,XCMPLX_1:76;
  then
A6: q^2/4 = d^2/(4*a^2) by XCMPLX_1:78;
  let u,v;
  assume x = u+v & 3*v*u+p = 0;
  hence thesis by A5,A4,A6,Th19;
end;

theorem
  a <> 0 & delta(a,b,c) >= 0 & Polynom(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)
proof
  assume
A1: a <> 0 & delta(a,b,c)>= 0;
  x |^ 3 = x |^ (2+1);
  then x |^ 3 = (x |^ (1+1))*x by NEWTON:6;
  then
A2: x |^ 3 = ((x |^ 1)*x)*x by NEWTON:6;
A3: x |^ 3 = x^2*x by A2;
  assume Polynom(a,b,c,0,x) = 0;
  then (a*x^2 +b*x+c)*x = 0 by A3;
  then x = 0 or Polynom(a,b,c,x) = 0 by XCMPLX_1:6;
  hence thesis by A1,Th5;
end;

theorem
  a <> 0 & c/a < 0 & Polynom(a,0,c,0,x) = 0 implies x = 0 or x = sqrt -c
  /a or x = -sqrt(-c/a)
proof
  assume that
A1: a <> 0 and
A2: c/a < 0;
  x |^ 3 = x |^ (2+1);
  then x |^ 3 = (x |^ (1+1))*x by NEWTON:6;
  then
A3: x |^ 3 = ((x |^ 1)*x)*x by NEWTON:6;
A4: x |^ 3 = x^2*x by A3;
  assume Polynom(a,0,c,0,x) = 0;
  then (a*x^2+c)*x = 0 by A4;
  then
A5: x = 0 or (a*x^2+c) = 0 by XCMPLX_1:6;
  now
    per cases by XXREAL_0:1;
    case
A6:   x > 0;
      x |^ 2 = (x |^ (1+1));
      then x |^ 2 = ((x |^ 1)*x) by NEWTON:6;
      then x |^ 2 = ((x to_power 1)*x) by POWER:41;
      then
A7:   x |^ 2 = x*x by POWER:25;
A8:   (-c/a) > 0 by A2,XREAL_1:58;
      x^2 = (-c)/a by A1,A5,A6,XCMPLX_1:89;
      then x^2 = ((-c)*a") by XCMPLX_0:def 9;
      then x^2 = -(c*a");
      then x^2 = -c/a by XCMPLX_0:def 9;
      then x = 2 -Root (-c/a) by A6,A8,A7,PREPOWER:def 2;
      hence thesis by A8,PREPOWER:32;
    end;
    case
A9:   x < 0;
      (-x) |^ 2 = ((-x) |^ (1+1));
      then (-x) |^ 2 = (((-x) |^ 1)*(-x)) by NEWTON:6;
      then (-x) |^ 2 = (((-x) to_power 1)*(-x)) by POWER:41;
      then
A10:  (-x) |^ 2 = (-x)*(-x) by POWER:25;
      x^2 = (-c)/a by A1,A5,A9,XCMPLX_1:89;
      then x^2 = ((-c)*a") by XCMPLX_0:def 9;
      then x^2 = -(c*a");
      then
A11:  (-x)^2=-c/a by XCMPLX_0:def 9;
A12:  (-c/a) > 0 by A2,XREAL_1:58;
      -x>0 by A9,XREAL_1:58;
      then -x = (2 -Root (-c/a)) by A11,A12,A10,PREPOWER:def 2;
      then -x = sqrt(-c/a) by A12,PREPOWER:32;
      hence thesis;
    end;
    case
      x=0;
      hence thesis;
    end;
  end;
  hence thesis;
end;