:: Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients
:: by Xiquan Liang
::
:: Received February 3, 2003
:: Copyright (c) 2003-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 NUMBERS, RELAT_1, XCMPLX_0, POLYEQ_1, NEWTON, ARYTM_3, SQUARE_1,
XREAL_0, CARD_1, ARYTM_1, XXREAL_0, FUNCT_3, POWER, COMPLEX1, POLYEQ_2,
ABIAN, REAL_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, INT_1, NEWTON,
ABIAN, POWER, COMPLEX1, QUIN_1, XXREAL_0, POLYEQ_1;
constructors REAL_1, SQUARE_1, NAT_1, MEMBERED, QUIN_1, NEWTON, PREPOWER,
POLYEQ_1, SERIES_1, ABIAN;
registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, POWER;
requirements REAL, SUBSET, NUMERALS, ARITHM;
equalities SQUARE_1;
theorems SQUARE_1, PREPOWER, QUIN_1, POLYEQ_1, POWER, ABSVALUE, NEWTON,
XCMPLX_0, XCMPLX_1, COMPLEX1, XREAL_1, XXREAL_0, ABIAN, INT_1;
begin
4 = 2 * 2;
then 2 divides 4 by INT_1:def 3;
then
Lm1: 4 is even by ABIAN:def 1;
3 = 2*1+1;
then
Lm2: 3 is odd by ABIAN:1;
definition
let a,b,c,d,e,x be Complex;
func Polynom(a,b,c,d,e,x) -> set equals
a*(x |^ 4)+b*(x |^ 3)+c*(x^2)+d*x+e;
correctness;
end;
registration
let a,b,c,d,e,x be Complex;
cluster Polynom(a,b,c,d,e,x) -> complex;
coherence;
end;
registration
let a,b,c,d,e,x be Real;
cluster Polynom(a,b,c,d,e,x) -> real;
coherence;
end;
theorem
for a,c,e,x being Real st a <> 0 & e <> 0 & c^2 - (4*a*e) > 0
holds Polynom(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)))
proof
let a,c,e,x be Real;
assume that
A1: a <> 0 and
A2: e <> 0 and
A3: c ^2 -(4*a*e) > 0;
set y = x^2;
assume
A4: Polynom(a,0,c,0,e,x) = 0;
A5: now
assume x = 0;
then a*0 +0*(0 |^ 3)+ e = 0 by A4,NEWTON:11;
hence contradiction by A2;
end;
per cases by A5,XXREAL_0:1;
suppose
A6: x > 0;
x|^ 4 = x to_power (2+2) by POWER:41
.= (x to_power 2)*(x to_power 2) by A6,POWER:27
.= x^2*(x to_power 2) by POWER:46
.= x^2*x^2 by POWER:46;
then a*y^2+c*y + e = 0 by A4;
then
A7: Polynom (a,c,e,y) = 0 by POLYEQ_1:def 2;
delta(a,c,e) >= 0 by A3,QUIN_1:def 1;
then
y = (-c + sqrt delta(a,c,e))/(2*a) or y = (-c - sqrt delta(a,c,e))/(2
*a) by A1,A7,POLYEQ_1:5;
then |.x.| = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or |.x.| = sqrt((-c -
sqrt delta(a,c,e))/(2*a)) by COMPLEX1:72;
hence thesis by A6,ABSVALUE:def 1;
end;
suppose
A8: x < 0;
then
A9: 0 < - x by XREAL_1:58;
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then x|^ 4 = (-x) to_power (2+2) by POWER:41
.= ((-x) to_power 2)*((-x) to_power 2) by A9,POWER:27
.= (-x)^2*((-x) to_power 2) by POWER:46
.= x^2*x^2 by POWER:46;
then a*y^2+c*y + e = 0 by A4;
then
A10: Polynom(a,c,e,y) = 0 by POLYEQ_1:def 2;
(c^2-4*a*e) = delta(a,c,e) by QUIN_1:def 1;
then
y = (-c + sqrt delta(a,c,e))/(2*a) or y = (-c - sqrt delta(a,c,e))/(2
*a) by A1,A3,A10,POLYEQ_1:5;
then |.x.| = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or |.x.| = sqrt((-c -
sqrt delta(a,c,e))/(2*a)) by COMPLEX1:72;
then
(-1)*(-x) = (-1)* sqrt((-c + sqrt delta(a,c,e))/(2*a)) or (-1)*(-x) =
(-1)*sqrt((-c - sqrt delta(a,c,e))/(2*a)) by A8,ABSVALUE:def 1;
hence thesis by A5;
end;
end;
theorem Th2:
for a,b,c,x,y being Real st a <> 0 & y = x + 1/x holds
Polynom(a,b,c,b,a,x) = 0 implies x <> 0 & a*y^2 + b*y + c - 2*a = 0
proof
let a,b,c,x,y be Real;
assume that
A1: a <> 0 and
A2: y = x + 1/x;
assume
A3: Polynom(a,b,c,b,a,x) = 0;
A4: x <> 0
proof
assume x = 0;
then a*(0 to_power 4)+b*(0|^ 3)+ a = 0 by A3;
then a*0+b*(0|^ 3)+ a = 0 by POWER:def 2;
then a*0+b*0+ a = 0 by NEWTON:11;
hence contradiction by A1;
end;
then
A5: x^2 > 0 by SQUARE_1:12;
A6: x|^ 4 = x to_power (2+2) by POWER:41;
A7: now
per cases by A4,XXREAL_0:1;
case
A8: x > 0;
set n = -(b*x+a);
set m = (a*x^2)+(b*x+c);
x|^ 3 = (x to_power(2+1)) by POWER:41
.= (x to_power 2)*(x to_power 1) by A8,POWER:27;
then
A9: x|^ 3 = (x to_power 2)*x
.= x^2*x by POWER:46;
x|^ 4 = (x to_power 2)*(x to_power 2) by A6,A8,POWER:27
.= x^2*(x to_power 2) by POWER:46
.= x^2*x^2 by POWER:46;
then m*x^2 = n*1 by A3,A9;
then m/1 = n/x^2 by A5,XCMPLX_1:94;
then (a*x^2)+(b*x+c) = (-(b*x+a))*(1/x^2) by XCMPLX_1:99
.= (-(b*x+a))*(x^2)" by XCMPLX_1:215
.= -b*(x*(x^2)")-a*(x^2)";
then a*(x^2+(x^2)") = -(b*(x*(x^2)"+x))- c;
then
A10: a*(x^2+1/x^2) = -(b*(x*(x^2)"+x))- c by XCMPLX_1:215
.= -(b*(x*(1/x^2)+x))- c by XCMPLX_1:215;
1/(x*x) = (1/x)*(1/x) by XCMPLX_1:102;
then a*(x^2+1/x^2) = -(b*((x*(1/x))*(1/x)+x))- c by A10;
then
A11: a*(x^2+1/x^2) = -(b*(1 *(1/x)+x))- c by A8,XCMPLX_1:106;
x*y = x*x +x*(1/x) by A2;
then x*y + 0 = (x^2 + 1) by A4,XCMPLX_1:106;
hence a*(x^2+1/x^2) = -(b*(x+1/x))- c & x^2 - x*y + 1 = 0 by A11;
end;
case
A12: x < 0;
set n = -(b*x+a);
set m = (a*x^2)+(b*x+c);
(-x)|^ 3 +(x|^ 3) = -((x|^ 3)+-(x|^ 3)) by Lm2,POWER:2
.= (x|^ 3)-(x|^ 3);
then
A13: x|^ 3 = -((-x)|^ 3);
A14: 0 < - x by A12,XREAL_1:58;
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then
A15: x|^ 4 = (-x) to_power (2+2) by POWER:41
.= ((-x) to_power 2)*((-x) to_power 2) by A14,POWER:27
.= (-x)^2*((-x) to_power 2) by POWER:46
.= x^2*(-x)^2 by POWER:46;
(-x)|^ 3 = ((-x)to_power(2+1)) by POWER:41
.= ((-x) to_power 2)*((-x) to_power 1) by A14,POWER:27;
then
A16: (-x)|^ 3 = ((-x) to_power 2)*(-x);
(-x) to_power 2 = (-x)^2 by POWER:46
.= x^2;
then m*x^2 = n*1 by A3,A15,A16,A13;
then m/1 = n/x^2 by A5,XCMPLX_1:94;
then m = n*(1/x^2) by XCMPLX_1:99
.= n*(x^2)" by XCMPLX_1:215
.= -b*(x*(x^2)")-a*(x^2)";
then a*(x^2+(x^2)") = -(b*(x*(x^2)"+x))- c;
then a*(x^2+1/x^2) = -(b*(x*(x^2)"+x))- c by XCMPLX_1:215
.= -(b*(x*(1/x^2)+x))- c by XCMPLX_1:215;
then a*(x^2+1/x^2) = -(b*(x*((1/x)*(1/x))+x))- c by XCMPLX_1:102
.= -(b*((x*(1/x))*(1/x)+x))- c;
then
A17: a*(x^2+1/x^2) = -(b*((1)*(1/x)+x))- c by A12,XCMPLX_1:106;
x*y = x*x +x*(1/x) by A2
.= x*x + 1 by A12,XCMPLX_1:106;
hence a*(x^2+1/x^2) = -(b*(x+1/x))- c & x^2 - x*y + 1 = 0 by A17;
end;
end;
y^2 = x^2+2*(x*(1/x))+(1/x)^2 by A2
.= x^2+ 2*1 +(1/x)^2 by A4,XCMPLX_1:106
.= x^2+ 2 +(1^2/x^2) by XCMPLX_1:76
.= x^2-(- 2 -(1/x^2));
then a*y^2 - 2*a = -(b*y)- c by A2,A7;
hence thesis by A4;
end;
theorem
for a,b,c,x,y being Real st a <> 0 & b^2-4*a*c + 8*a^2 > 0 & y
= x + 1/x holds Polynom(a,b,c,b,a,x) = 0 implies for y1,y2 being Real 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)
proof
let a,b,c,x,y be Real;
assume that
A1: a <> 0 and
A2: b^2-4*a*c+8*a^2 > 0 and
A3: y = x + 1/x and
A4: Polynom(a,b,c,b,a,x) = 0;
A5: x <> 0 by A1,A3,A4,Th2;
set f = c - 2*a;
a*y^2+ b*y + c - 2*a = 0 by A1,A3,A4,Th2;
then a*y^2+ b*y + (c - 2*a) = 0;
then
A6: Polynom(a,b,f,y) = 0 by POLYEQ_1:def 2;
let y1,y2 be Real;
assume
A7: 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 );
x*y = x^2 +(x*(1/x)) by A3;
then x*y + 0 = (x^2 + 1) by A5,XCMPLX_1:106;
then 1*x^2+((-y)*x) + 1 = 0;
then
A8: Polynom (1,-y,1,x) = 0 by POLYEQ_1:def 2;
delta(1,(-y),1) = (-y)^2 -4*1*1 by QUIN_1:def 1
.= (x^2 + (2*(x*(1/x))) +(1/x)^2)-4 by A3
.= (x^2 +2*1 +(1/x)^2) -4 by A5,XCMPLX_1:106
.= x^2 + (-2*1 +(1/x)^2)
.= x^2 + (-2*(x*(1/x)) +(1/x)^2) by A5,XCMPLX_1:106
.= ( x - (1/x) )^2;
then
A9: x = (-(-y) + sqrt delta(1,(-y),1))/(2*1) or x = (-(-y) - sqrt delta(1,(
-y),1))/(2*1) by A8,POLYEQ_1:5,XREAL_1:63;
A10: b^2 - 4*a*f = b^2 - 4*a*c + 8*a^2;
then delta(a,b,f) > 0 by A2,QUIN_1:def 1;
then y = (-b + sqrt delta(a,b,f))/(2*a) or y = (-b - sqrt delta(a,b,f))/(2*
a) by A1,A6,POLYEQ_1:5;
then y = y1 or y = y2 by A7,A10,QUIN_1:def 1;
hence thesis by A1,A3,A4,A9,Th2;
end;
theorem Th4:
for x being Real holds x|^ 3 = x^2*x & (x|^ 3)*x = x|^ 4 &
x^2*x^2 = x|^ 4
proof
let x be Real;
per cases by XXREAL_0:1;
suppose
x = 0;
hence thesis by NEWTON:11;
end;
suppose
A1: x > 0;
(x|^ 3)*x = (x|^ 3)*(x to_power 1)
.= (x to_power 3)*(x to_power 1);
then
A2: (x|^ 3)*x = x to_power (3 + 1) by A1,POWER:27;
x^2 = x to_power 2 by POWER:46;
then x^2*x = (x to_power 2)*(x to_power 1)
.= x to_power (2 + 1) by A1,POWER:27
.= x|^ 3 by POWER:41;
hence thesis by A2,POWER:41;
end;
suppose
x<0;
then
A3: -x>0 by XREAL_1:58;
(-x)|^ 3 + (x|^ 3) = -((x|^ 3)+-(x|^ 3)) by Lm2,POWER:2
.= (x|^ 3)-(x|^ 3);
then
A4: (x|^ 3)+ ((-x)|^ 3 - (-x)|^ 3) = 0 - (-x)|^ 3;
A5: (-x) to_power 2 = (-x)^2 by POWER:46
.= x^2;
(-x)|^ 3 = (-x) to_power (2+1) by POWER:41
.= ((-x) to_power 2)*((-x) to_power 1) by A3,POWER:27;
then
A6: (-x)|^ 3 = ((-x) to_power 2)*(-x);
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then x|^ 4 = (-x) to_power (3+1) by POWER:41
.= ((-x) to_power 3)*((-x) to_power 1) by A3,POWER:27
.= ((-x)|^ 3)*((-x) to_power 1);
then x|^ 4 = ((-x)|^ 3)*(-x)
.= x^2*(x*x) by A6,A5;
hence thesis by A6,A5,A4;
end;
end;
theorem Th5:
for x,y being Real 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
proof
let x,y be Real;
assume
A1: x+y <> 0;
per cases by A1,XXREAL_0:1;
suppose
A2: x+y>0;
(x+y)|^ 4 = (x+y) to_power (3+1) by POWER:41
.= ((x+y) to_power 3)*((x+y) to_power 1) by A2,POWER:27
.= ((x+y) to_power 3)*(x+y);
then (x+y)|^ 4 = ((x+y)|^ 3)*(x+y)
.= (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*(x+y) by POLYEQ_1:14;
hence thesis;
end;
suppose
x+y<0;
then
A3: -(x+y)>0 by XREAL_1:58;
(-(x+y))|^ 4 = (x+y)|^ 4 by Lm1,POWER:1;
then (x+y)|^ 4 = (-(x+y)) to_power (3+1) by POWER:41
.= ((-(x+y)) to_power 3)*((-(x+y)) to_power 1) by A3,POWER:27
.= ((-(x+y))|^ 3)*((-(x+y)) to_power 1);
then
(x+y)|^ 4 = ((-(x+y))|^ 3)*(-(x+y));
then (x+y)|^ 4 = (-((x+y)|^ 3))*(-(x+y)) by Lm2,POWER:2
.= ((x+y)|^ 3)*(x+y)
.= (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*(x+y) by POLYEQ_1:14;
hence thesis;
end;
end;
theorem
for x,y being Real 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
proof
let x,y be Real;
set g = (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*x;
set h = (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*y;
set p = y|^ 3, q = x|^ 3, u = x|^ 4, v = y|^ 4;
A1: g = (x|^ 3)*x +((3*y)*x^2+(3*y^2)*x)*x+(y|^ 3)*x;
A2: y|^ 3 = y^2*y by Th4;
assume x+y<>0;
then
A3: (x+y)|^ 4 = g+h by Th5;
h = (x|^ 3)*y +((3*y)*x^2+(3*y^2)*x)*y+((y|^ 3)*y)
.= (x|^ 3)*y +((3*y)*x^2+(3*y^2)*x)*y+(y|^ 4) by Th4;
then
(x+y)|^ 4 = u +((3*y)*(x^2*x)-(-(3*y^2)*x)*x)+p*x +(q*y +((3*y)*x^2+(3*y
^2)*x)*y+v) by A3,A1,Th4
.= u +((3*y)*q-(-((3*y^2)*x^2)))+p*x +(q*y +((3*y)*x^2+(3*y^2)*x)*y+v)
by Th4
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x) +(q*y +(((3*y^2)*x^2)+(3*y^2)*x*y)+v);
hence thesis by A2;
end;
theorem Th7:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real holds (for x
being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(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
proof
set x=-1;
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;
A1: 0|^ 3 =0 & 0|^ 4 = 0 by NEWTON:11;
assume
A2: for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(b1
,b2,b3,b4,b5,x);
then
A3: Polynom(a1,a2,a3,a4,a5,-1) = Polynom(b1,b2,b3,b4,b5,-1);
A5: x|^ 3=x^2*x & (x|^ 3)*x=x|^ 4 by Th4;
Polynom(a1,a2,a3,a4,a5,0) = Polynom(b1,b2,b3,b4,b5,0) & Polynom(a1,a2,a3
,a4, a5,1) = Polynom(b1,b2,b3,b4,b5,1) by A2;
hence thesis by A1,A3,A5;
end;
theorem Th8:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real holds (for x
being Real holds Polynom(a1,a2,a3,a4,a5,x)=Polynom(b1,b2,b3,b4,b5,x))
implies a1-b1=b3-a3 & a2-b2=b4-a4
proof
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;
assume for x being Real holds Polynom(a1,a2,a3,a4,a5,x)=Polynom(b1,
b2,b3,b4,b5,x);
then a1-a2+a3-a4=b1-b2+b3-b4 & a1+a2+a3+a4=b1+b2+b3+b4 by Th7;
hence thesis;
end;
theorem Th9:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real st (for x
being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(b1,b2,b3,b4,b5,x))
holds a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5
proof
A1: (-2)|^ 3 = (-2)^2*(-2) by Th4
.= -(4*2);
A2: (-2)|^ 4 = 16 by Lm1,POWER:1,62;
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;
assume
A3: for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(b1
,b2,b3,b4,b5,x);
then
A4: Polynom(a1,a2,a3,a4,a5,-2) = Polynom(b1,b2,b3,b4,b5,-2);
A5: a5 = b5 & Polynom(a1,a2,a3,a4,a5,2) = Polynom(b1,b2,b3,b4,b5,2) by A3,Th7;
a1-b1 = b3-a3 & a2-b2 = b4-a4 by A3,Th8;
hence thesis by A5,A4,A2,A1,POWER:61,62;
end;
definition
let a1,x1,x2,x3,x4,x be Real;
func Four0(a1,x1,x2,x3,x4,x) -> set equals
a1*((x-x1)*(x-x2)*(x-x3)*(x-x4));
correctness;
end;
registration
let a1,x1,x2,x3,x4,x be Real;
cluster Four0(a1,x1,x2,x3,x4,x) -> real;
coherence;
end;
theorem Th10:
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being Real st a1 <> 0
holds (for x being Real holds Polynom(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
proof
let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be Real;
assume
A1: a1 <> 0;
set z = ((x-x1)*(x-x2)*(x-x3)*(x-x4));
set w = a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5;
assume for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,
x1,x2,x3,x4,x);
then Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x);
then w/a1*a1-(z*a1) = (z*a1)-(z*a1) by A1,XCMPLX_1:87;
then (w/a1-z)*a1 = 0;
then w/a1+-z= 0-0 by A1,XCMPLX_1:6;
hence thesis;
end;
theorem Th11:
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being Real st a1 <> 0
holds (for x being Real holds Polynom(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)
proof
let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being Real;
assume
A1: a1 <> 0;
set w = a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5;
assume for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,
x1,x2,x3,x4,x);
then
(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 by A1,Th10;
then
w/a1 = x^2*x^2-(x1+x2+x3+x4)*(x^2*x) +(x1*x3+x2*x3+x1*x2+(x2*x4+x1*x4+x3
*x4))*x^2 -(x1*x2*x3+x1*x2*x4+-(-x1*x3*x4)+x2*x3*x4)*x+(x1*x2*x3*x4);
then
w/a1 = x|^ 4-(x1+x2+x3+x4)*(x^2*x) +((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) by Th4;
hence thesis by Th4;
end;
theorem
for a1,a2,a3,a4,a5,x1,x2,x3,x4 being Real st a1 <> 0 & (for x
being Real holds Polynom(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
proof
set b1 = 1;
let a1,a2,a3,a4,a5,x1,x2,x3,x4 be Real;
assume
A1: a1 <> 0;
set b5 = x1*x2*x3*x4;
set b4 = -(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4);
set b3 = (x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4;
set b2 = -(x1+x2+x3+x4);
assume
A2: for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,
x1,x2,x3,x4,x);
now
let x be Real;
set t= b1*(x|^ 4)+b2*x|^ 3+b3*x^2+b4*x+b5;
(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) by A1,A2,Th11;
then t = a1"*((a1*(x|^ 4)+a2*(x|^ 3))+(a3*x^2+a4*x)+a5) by XCMPLX_0:def 9
.= (a1"*a1)*(x|^ 4)+a1"*(a2*(x|^ 3)) +(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5)
.= (a1/a1)*(x|^ 4)+a1"*(a2*(x|^ 3)) +(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5)
by XCMPLX_0:def 9
.= 1 *(x|^ 4)+a1"*(a2*(x|^ 3)) +(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5) by A1,
XCMPLX_1:60
.= (x|^ 4)+(a1"*a2)*(x|^ 3) +(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5)
.= (x|^ 4)+(a2/a1)*(x|^ 3) +((a1"*a3)*x^2+a1"*(a4*x)+a1"*a5) by
XCMPLX_0:def 9
.= (x|^ 4)+(a2/a1)*(x|^ 3) +((a3/a1)*x^2+(a1"*a4)*x+a1"*a5) by
XCMPLX_0:def 9
.= (x|^ 4)+(a2/a1)*(x|^ 3) +((a3/a1)*x^2+(a4/a1)*x+(a1"*a5)) by
XCMPLX_0:def 9
.= (x|^ 4)+(a2/a1)*(x|^ 3) +((a3/a1)*x^2+(a4/a1)*x+(a5/a1)) by
XCMPLX_0:def 9
.= Polynom(1,a2/a1,a3/a1,a4/a1,a5/a1,x);
hence Polynom(1,a2/a1,a3/a1,a4/a1,a5/a1,x) = Polynom(b1,b2,b3,b4,b5,x);
end;
hence thesis by Th9;
end;
theorem
for a,k,y being Real st a <> 0 holds (for x being Real
holds x|^ 4+a|^ 4 = k*a*x*(x^2+a^2)) implies y|^ 4 -k*(y|^ 3)-k*y+1 = 0
proof
let a,k,y be Real;
assume that
A1: a <> 0 and
A2: for x being Real holds x|^ 4+a|^ 4 = k*a*x*(x^2+a^2);
(a*y)|^ 4+a|^ 4 = k*a*(a*y)*((a*y)^2+a^2) by A2
.= k*(a^2*y)*(a^2*y^2+a^2*1);
then (a*y)|^ 4+a|^ 4 = k*(((a^2*a^2)*y)*(y^2+1))
.= (k*(((a|^ 4)*y)*(y^2+1))) by Th4
.= (((a|^ 4)*(k*y))*(y^2+1));
then (a|^ 4)*(y|^ 4)+(a|^ 4)*1 = (a|^ 4)*((k*y)*(y^2+1)) by NEWTON:7;
then (a|^ 4)"*((a|^ 4)*((y|^ 4)+1-(k*y)*(y^2+1))) = 0;
then (((a|^ 4)"*(a|^ 4))*((y|^ 4)+1-(k*y)*(y^2+1))) = 0;
then
A3: (((1/(a|^ 4))*(a|^ 4))*((y|^ 4)+1-(k*y)*(y^2+1))) = 0 by XCMPLX_1:215;
a|^ 4 <> 0 by A1,PREPOWER:5;
then 1*((y|^4)+1-(k*y)*(y^2+1)) = 0 by A3,XCMPLX_1:106;
then (y|^4)-k*(y^2*y)-k*y+1 = 0;
hence thesis by Th4;
end;