:: Solving Roots of Polynomial Equations of Degree 2 and 3 with
:: Real Coefficients
:: by Liang Xiquan
::
:: Received May 18, 2000
:: Copyright (c) 2000-2026 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;
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;