Copyright (c) 2003 Association of Mizar Users
environ
vocabulary SQUARE_1, ABSVALUE, RELAT_1, FUNCT_3, POWER, POLYEQ_1, ARYTM_1,
ARYTM_3, POLYEQ_2, GROUP_1, ARYTM;
notation ORDINAL1, XCMPLX_0, XREAL_0, ABSVALUE, SQUARE_1, NEWTON, POWER,
POLYEQ_1, QUIN_1;
constructors REAL_1, NAT_1, SQUARE_1, PREPOWER, POLYEQ_1, QUIN_1, SERIES_1,
MEMBERED;
clusters XREAL_0, NEWTON, SQUARE_1, QUIN_1, MEMBERED;
requirements REAL, SUBSET, NUMERALS, ARITHM;
theorems AXIOMS, REAL_1, SQUARE_1, PREPOWER, QUIN_1, POLYEQ_1, POWER,
ABSVALUE, ASYMPT_1, NEWTON, XCMPLX_0, XCMPLX_1;
begin
Lm1: 4 = 2 * 2;
definition let a,b,c,d,e,x be real number;
func Four(a,b,c,d,e,x) equals :Def1:
a*(x |^ 4)+b*(x |^ 3)+c*(x^2)+d*x+e;
correctness;
end;
definition let a,b,c,d,e,x be real number;
cluster Four(a,b,c,d,e,x) -> real;
coherence
proof
a*(x |^ 4)+b*(x |^ 3)+c*(x^2)+d*x+e = Four(a,b,c,d,e,x)
by Def1;
hence thesis;
end;
end;
theorem
for a,c,e,x being real number st a <> 0 &
e <> 0 & c^2 - (4*a*e) > 0 holds
Four(a,0,c,0,e,x) = 0 implies
x <> 0 &
(x = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
x = sqrt((-c - sqrt delta(a,c,e))/(2*a)) or
x = - sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
x = - sqrt((-c - sqrt delta(a,c,e))/(2*a)))
proof
let a,c,e,x be real number;
assume that
A1: a <> 0 and
A2: e <> 0 and
A3: c ^2 -(4*a*e) > 0;
assume
A4: Four(a,0,c,0,e,x) = 0;
then A5: a*(x|^ 4)+0*(x|^ 3)+c*x^2+0*x+e = 0 by Def1;
A6: now assume x = 0;
then a*(0 |^ 4)+0*(0 |^ 3)+c*0^2+0*0+ e = 0 by A4,Def1;
then a*0 +0*(0 |^ 3)+ e = 0 by NEWTON:16,SQUARE_1:60;
hence contradiction by A2;
end;
set y = x^2;
per cases by A6,AXIOMS:21;
suppose
A7: x > 0;
x|^ 4 = x to_power (2+2) by POWER:47
.= (x to_power 2)*(x to_power 2) by A7,POWER:32
.= x^2*(x to_power 2) by POWER:53
.= x^2*x^2 by POWER:53;
then a*y^2+c*y + e = 0 by A5,SQUARE_1:def 3;
then A8: Poly2 (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,A8,POLYEQ_1:5;
then abs x = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
abs x = sqrt((-c - sqrt delta(a,c,e))/(2*a))
by SQUARE_1:91;
hence thesis by A7,ABSVALUE:def 1;
suppose
A9: x < 0;
then A10: 0 < - x by REAL_1:66;
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then x|^ 4 = (-x) to_power (2+2) by POWER:47
.= ((-x) to_power 2)*((-x) to_power 2) by A10,POWER:32
.= (-x)^2*((-x) to_power 2) by POWER:53
.= (-x)^2*(-x)^2 by POWER:53
.= x^2*(-x)^2 by SQUARE_1:61
.= x^2*x^2 by SQUARE_1:61;
then a*y^2+c*y + e = 0 by A5,SQUARE_1:def 3;
then A11: Poly2(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,A11,POLYEQ_1:5;
then abs x = sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
abs x = sqrt((-c - sqrt delta(a,c,e))/(2*a))
by SQUARE_1:91;
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 A9,ABSVALUE:def 1;
then x = (-1)* sqrt((-c + sqrt delta(a,c,e))/(2*a)) or
x = (-1)*sqrt((-c - sqrt delta(a,c,e))/(2*a)) by XCMPLX_1:181;
hence thesis by A6,XCMPLX_1:180;
end;
theorem Th2:
for a,b,c,x,y being real number st a <> 0 & y = x + 1/x holds
Four(a,b,c,b,a,x) = 0 implies
x <> 0 & a*y^2 + b*y + c - 2*a = 0
proof
let a,b,c,x,y be real number;
assume that
A1: a <> 0 and
A2: y = x + 1/x;
assume Four(a,b,c,b,a,x) = 0;
then A3: a*(x|^ 4)+b*(x|^ 3)+c*x^2+b*x+a = 0 by Def1;
A4: x <> 0
proof assume x = 0;
then a*(0 to_power 4)+b*(0|^ 3)+ a = 0
by A3,POWER:47,SQUARE_1:60;
then a*0+b*(0|^ 3)+ a = 0 by POWER:def 2;
then a*0+b*0+ a = 0 by NEWTON:16;
hence contradiction by A1;
end;
then A5: (x>0 or x<0) & x^2 > 0 by AXIOMS:21,SQUARE_1:74;
A6: x|^ 4 = x to_power (2+2) by POWER:47;
A7: now per cases by A4,AXIOMS:21;
case
A8: x > 0;
then A9: x|^ 4 = (x to_power 2)*(x to_power 2) by A6,POWER:32
.= x^2*(x to_power 2) by POWER:53
.= x^2*x^2 by POWER:53;
x|^ 3 = (x to_power(2+1)) by POWER:47
.= (x to_power 2)*(x to_power 1) by A8,POWER:32;
then x|^ 3 = (x to_power 2)*x by POWER:30
.= x^2*x by POWER:53;
then (a*(x^2*x^2)+b*(x^2*x)+c*x^2)+(b*x+a) = 0
by A3,A9,XCMPLX_1:1;
then (a*(x^2*x^2)+b*(x^2*x)+c*x^2) = 0-(b*x+a) by XCMPLX_1:26;
then A10: -(b*x+a) = (a*(x^2*x^2)+b*(x^2*x)+c*x^2) by XCMPLX_1:150
.= a*(x^2*x^2)+(b*(x*x^2)+c*x^2) by XCMPLX_1:1
.= (a*x^2)*x^2+(b*(x*x^2)+c*x^2) by XCMPLX_1:4
.= (a*x^2)*x^2+((b*x)*x^2+c*x^2) by XCMPLX_1:4
.= (a*x^2)*x^2+(b*x+c)*x^2 by XCMPLX_1:8;
set m = (a*x^2)+(b*x+c);
set n = -(b*x+a);
m*x^2 = n*1 by A10,XCMPLX_1:8;
then m/1 = n/x^2 by A5,XCMPLX_1:95;
then (a*x^2)+(b*x+c) = (-(b*x+a))*(1/x^2) by XCMPLX_1:100
.= (-(b*x+a))*(x^2)" by XCMPLX_1:217
.= -((b*x+a)*(x^2)") by XCMPLX_1:175
.= -((b*x)*(x^2)"+a*(x^2)") by XCMPLX_1:8
.= -((b*x)*(x^2)")-a*(x^2)" by XCMPLX_1:161
.= -b*(x*(x^2)")-a*(x^2)" by XCMPLX_1:4;
then a*x^2+a*(x^2)" = -b*(x*(x^2)")-(b*x+c)by XCMPLX_1:35;
then a*(x^2+(x^2)") = -b*(x*(x^2)")-(b*x+c) by XCMPLX_1:8
.= -b*(x*(x^2)")-b*x- c by XCMPLX_1:36
.= -(b*(x*(x^2)")+b*x)- c by XCMPLX_1:161
.= -(b*(x*(x^2)"+x))- c by XCMPLX_1:8;
then a*(x^2+1/x^2) = -(b*(x*(x^2)"+x))- c by XCMPLX_1:217
.= -(b*(x*(1/x^2)+x))- c by XCMPLX_1:217;
then A11: a*(x^2+1/x^2) = -(b*(x*(1/(x*x))+x))- c by SQUARE_1:def 3;
1/(x*x) = (1/x)*(1/x) by XCMPLX_1:103;
then a*(x^2+1/x^2) = -(b*((x*(1/x))*(1/x)+x))- c
by A11,XCMPLX_1:4;
then A12: a*(x^2+1/x^2) = -(b*(1 *(1/x)+x))- c by A8,XCMPLX_1:107;
x*y = x*x +x*(1/x) by A2,XCMPLX_1:8;
then x*y = x^2 +x*(1/x) by SQUARE_1:def 3;
then x*y + 0 = (x^2 + 1) by A4,XCMPLX_1:107;
then x^2 + 1 - x*y = 0 by XCMPLX_1:26;
hence a*(x^2+1/x^2) = -(b*(x+1/x))- c &
x^2 - x*y + 1 = 0 by A12,XCMPLX_1:29;
case
A13: x < 0;
then A14: 0 < - x by REAL_1:66;
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then x|^ 4 = (-x) to_power (2+2) by POWER:47
.= ((-x) to_power 2)*((-x) to_power 2) by A14,POWER:32
.= (-x)^2*((-x) to_power 2) by POWER:53
.= (-x)^2*(-x)^2 by POWER:53
.= x^2*(-x)^2 by SQUARE_1:61;
then A15: x|^ 4 = x^2*x^2 by SQUARE_1:61;
(-x)|^ 3 = ((-x)to_power(2+1)) by POWER:47
.= ((-x) to_power 2)*((-x) to_power 1) by A14,POWER:32;
then A16: (-x)|^ 3 = ((-x) to_power 2)*(-x) by POWER:30;
(-x) to_power 2 = (-x)^2 by POWER:53
.= x^2 by SQUARE_1:61;
then A17: (-x)|^ 3 = -(x^2*x) by A16,XCMPLX_1:175;
3 = 2*1+1;
then (-x)|^ 3 +(x|^ 3) = -(x|^ 3)+(x|^ 3) by POWER:2
.= -(x|^ 3)--(x|^ 3) by XCMPLX_1:151
.= -((x|^ 3)+-(x|^ 3)) by XCMPLX_1:161
.= (x|^ 3)-(x|^ 3) by XCMPLX_1:163;
then (-x)|^ 3 +(x|^ 3) = 0 by XCMPLX_1:14;
then (x|^ 3)+(-x)|^ 3-((-x)|^ 3) = -((-x)|^ 3) by XCMPLX_1:150;
then x|^ 3 = -((-x)|^ 3) by XCMPLX_1:26;
then (a*(x^2*x^2)+b*(x^2*x)+c*x^2)+(b*x+a) = 0
by A3,A15,A17,XCMPLX_1:1;
then (a*(x^2*x^2)+b*(x^2*x)+c*x^2) = 0-(b*x+a) by XCMPLX_1:26
.= -(b*x+a) by XCMPLX_1:150;
then a*(x^2*x^2)+(b*(x*x^2)+c*x^2) = -(b*x+a) by XCMPLX_1:1;
then (a*x^2)*x^2+(b*(x*x^2)+c*x^2) = -(b*x+a) by XCMPLX_1:4;
then (a*x^2)*x^2+((b*x)*x^2+c*x^2) = -(b*x+a) by XCMPLX_1:4;
then A18: (a*x^2)*x^2+(b*x+c)*x^2 = -(b*x+a) by XCMPLX_1:8;
set m = (a*x^2)+(b*x+c);
set n = -(b*x+a);
m*x^2 = n*1 by A18,XCMPLX_1:8;
then m/1 = n/x^2 by A5,XCMPLX_1:95;
then m = n*(1/x^2) by XCMPLX_1:100
.= n*(x^2)" by XCMPLX_1:217
.= -((b*x+a)*(x^2)") by XCMPLX_1:175
.= -((b*x)*(x^2)"+a*(x^2)") by XCMPLX_1:8
.= -((b*x)*(x^2)")-a*(x^2)" by XCMPLX_1:161
.= -b*(x*(x^2)")-a*(x^2)" by XCMPLX_1:4;
then a*x^2+a*(x^2)" = -b*(x*(x^2)")-(b*x+c) by XCMPLX_1:35;
then a*(x^2+(x^2)") = -b*(x*(x^2)")-(b*x+c) by XCMPLX_1:8
.= -b*(x*(x^2)")-b*x- c by XCMPLX_1:36
.= -(b*(x*(x^2)")+b*x)- c by XCMPLX_1:161
.= -(b*(x*(x^2)"+x))- c by XCMPLX_1:8;
then a*(x^2+1/x^2) = -(b*(x*(x^2)"+x))- c by XCMPLX_1:217
.= -(b*(x*(1/x^2)+x))- c by XCMPLX_1:217;
then a*(x^2+1/x^2) = -(b*(x*(1/(x*x))+x))- c by SQUARE_1:def 3
.= -(b*(x*((1/x)*(1/x))+x))- c by XCMPLX_1:103
.= -(b*((x*(1/x))*(1/x)+x))- c by XCMPLX_1:4;
then A19: a*(x^2+1/x^2) = -(b*((1)*(1/x)+x))- c by A13,XCMPLX_1:107;
x*y = x*x +x*(1/x) by A2,XCMPLX_1:8
.= x*x + 1 by A13,XCMPLX_1:107;
then x*y + 0 = x^2 + 1 by SQUARE_1:def 3;
then x^2 + 1 - x*y = 0 by XCMPLX_1:26;
hence a*(x^2+1/x^2) = -(b*(x+1/x))- c &
x^2 - x*y + 1 = 0 by A19,XCMPLX_1:29;
end;
set h = (- 2 -(1/x^2));
y^2 = x^2+2*x*(1/x)+(1/x)^2 by A2,SQUARE_1:63
.= x^2+2*(x*(1/x))+(1/x)^2 by XCMPLX_1:4
.= x^2+ 2*1 +(1/x)^2 by A4,XCMPLX_1:107
.= x^2+ 2 +(1^2/x^2) by SQUARE_1:69
.= x^2-(- 2 -(1/x^2)) by SQUARE_1:59,XCMPLX_1:157;
then y^2 + h = h - h +x^2 by XCMPLX_1:30
.= x^2 by XCMPLX_1:25;
then (y^2 - 2) - (1/x^2) + (1/x^2) = x^2+(1/x^2) by XCMPLX_1:158;
then (y^2 - 2) - ((1/x^2) - (1/x^2)) = x^2+(1/x^2) by XCMPLX_1:37;
then (y^2 - 2) - 0 = x^2 + (1/x^2) by XCMPLX_1:14;
then a*y^2 - 2*a = -(b*y)- c by A2,A7,XCMPLX_1:40;
then a*y^2 -(-(b*y)) = 2*a - c by XCMPLX_1:24;
then a*y^2 + b*y = (2*a - c) by XCMPLX_1:151;
then a*y^2 + b*y - (2*a - c) = 0 by XCMPLX_1:14;
then a*y^2 + b*y + (c - 2*a) = 0 by XCMPLX_1:38;
hence thesis by A4,XCMPLX_1:29;
end;
theorem
for a,b,c,x,y being real number st a <> 0 &
b^2-4*a*c + 8*a^2 > 0 & y = x + 1/x holds
Four(a,b,c,b,a,x) = 0 implies
(for y1,y2 being real number st
y1 = (-b+sqrt(b^2-4*a*c+8*a^2))/(2*a) &
y2 = (-b-sqrt(b^2-4*a*c+8*a^2))/(2*a) holds
x <> 0 &
(x = (y1 + sqrt delta(1,(-y1),1))/2 or
x = (y2 + sqrt delta(1,(-y2),1))/2 or
x = (y1 - sqrt delta(1,(-y1),1))/2 or
x = (y2 - sqrt delta(1,(-y2),1))/2))
proof
let a,b,c,x,y be real number;
assume that
A1: a <> 0 and
A2: b^2-4*a*c+8*a^2 > 0 and
A3: y = x + 1/x and
A4: Four(a,b,c,b,a,x) = 0;
let y1,y2 be real number;
assume
A5: 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);
A6: x <> 0 & a*y^2+ b*y + c - 2*a = 0 by A1,A3,A4,Th2;
then A7: x <> 0 & a*y^2+ b*y + (c - 2*a) = 0 by XCMPLX_1:29;
set f = c - 2*a;
b^2 - 4*a*f = b^2 - (4*a*c - 4*a*(2*a)) by XCMPLX_1:40
.= b^2 - 4*a*c + 4*a*(2*a) by XCMPLX_1:37
.= b^2 - 4*a*c + (4*(-(-2*a)))*a by XCMPLX_1:4
.= b^2 - 4*a*c + ((4*2)*a)*a by XCMPLX_1:4
.= b^2 - 4*a*c + 8*(a*a) by XCMPLX_1:4;
then A8: b^2 - 4*a*f = b^2 - 4*a*c + 8*a^2 by SQUARE_1:def 3;
then A9: delta(a,b,f) > 0 by A2,QUIN_1:def 1;
x <> 0 & Poly2(a,b,f,y) = 0 by A7,POLYEQ_1:def 2;
then A10: x <> 0 & (y = (-b + sqrt delta(a,b,f))/(2*a) or
y = (-b - sqrt delta(a,b,f))/(2*a)) by A1,A9,POLYEQ_1:5;
x*y = x*x +x*(1/x) by A3,XCMPLX_1:8
.= x^2 +(x*(1/x)) by SQUARE_1:def 3;
then x*y + 0 = (x^2 + 1) by A6,XCMPLX_1:107;
then A11: 0 = (x^2 + 1) - x*y by XCMPLX_1:26;
delta(1,(-y),1) = (-y)^2 -4*1*1 by QUIN_1:def 1
.= y^2 -4*1 by SQUARE_1:61
.= (x^2 +2*x*(1/x) +(1/x)^2)-4 by A3,SQUARE_1:63
.= (x^2 + (2*(x*(1/x))) +(1/x)^2)-4 by XCMPLX_1:4
.= (x^2 +2*1 +(1/x)^2) -4 by A6,XCMPLX_1:107
.= (x^2 + (2 +(1/x)^2)) -4 by XCMPLX_1:1
.= x^2 + ((2 +(1/x)^2)-4) by XCMPLX_1:29
.= x^2 + ((2 -(2+2) +(1/x)^2)) by XCMPLX_1:29
.= x^2 + (-2*1 +(1/x)^2)
.= x^2 + (-2*(x*(1/x)) +(1/x)^2) by A6,XCMPLX_1:107
.= x^2 + (-2*x*(1/x) +(1/x)^2) by XCMPLX_1:4
.= (x^2 + -2*x*(1/x)) +(1/x)^2 by XCMPLX_1:1
.= (x^2 --( -2*x*(1/x))) +(1/x)^2 by XCMPLX_1:151
.= ( x - (1/x) )^2 by SQUARE_1:64;
then A12: delta(1,-y,1) >= 0 by SQUARE_1:72;
1*x^2+(-y*x) + 1 = 0 by A11,XCMPLX_1:155;
then 1*x^2+((-y)*x) + 1 = 0 by XCMPLX_1:175;
then Poly2 (1,-y,1,x) = 0 by POLYEQ_1:def 2;
then A13: x = (-(-y) + sqrt delta(1,(-y),1))/(2*1) or
x = (-(-y) - sqrt delta(1,(-y),1))/(2*1) by A12,POLYEQ_1:5;
y = y1 or y = y2 by A5,A8,A10,QUIN_1:def 1;
hence thesis by A1,A3,A4,A13,Th2;
end;
theorem Th4:
for x being real number holds
x|^ 3 = x^2*x & (x|^ 3)*x = x|^ 4 & x^2*x^2 = x|^ 4
proof
let x be real number;
per cases by REAL_1:def 5;
suppose
A1: x = 0;
0|^ 4 = 0^2*(0*0) by NEWTON:16;
hence thesis by A1,NEWTON:16,SQUARE_1:def 3;
suppose
A2: x > 0;
x^2 = x to_power 2 by POWER:53;
then A3: x^2*x = (x to_power 2)*(x to_power 1) by POWER:30
.= x to_power (2 + 1) by A2,POWER:32
.= x|^ 3 by POWER:47;
(x|^ 3)*x = (x|^ 3)*(x to_power 1) by POWER:30
.= (x to_power 3)*(x to_power 1) by POWER:47;
then A4: (x|^ 3)*x = x to_power (3 + 1) by A2,POWER:32;
then x^2*(x*x) = x to_power 4 by A3,XCMPLX_1:4;
then x^2*x^2 = x to_power 4 by SQUARE_1:def 3;
hence thesis by A3,A4,POWER:47;
suppose x<0;
then A5: -x>0 by REAL_1:66;
(-x)|^ 3 = (-x) to_power (2+1) by POWER:47
.= ((-x) to_power 2)*((-x) to_power 1) by A5,POWER:32;
then A6: (-x)|^ 3 = ((-x) to_power 2)*(-x) by POWER:30;
A7: (-x) to_power 2 = (-x)^2 by POWER:53
.= x^2 by SQUARE_1:61;
then A8: (-x)|^ 3 = -x^2*x by A6,XCMPLX_1:175;
3 = 2*1+1;
then (-x)|^ 3 = -(x|^ 3) by POWER:2;
then (-x)|^ 3 + (x|^ 3) = -(x|^ 3)--(x|^ 3) by XCMPLX_1:151
.= -((x|^ 3)+-(x|^ 3)) by XCMPLX_1:161
.= (x|^ 3)-(x|^ 3) by XCMPLX_1:163;
then (x|^ 3)+ (-x)|^ 3 = 0 by XCMPLX_1:14;
then (x|^ 3)+ ((-x)|^ 3 - (-x)|^ 3) = 0 - (-x)|^ 3 by XCMPLX_1:29;
then (x|^ 3)+ 0 = 0 - (-x)|^ 3 by XCMPLX_1:14;
then A9: x|^ 3 = -((-x)|^ 3) by XCMPLX_1:150;
(-x)|^ 4 = x|^ 4 by Lm1,POWER:1;
then x|^ 4 = (-x) to_power (3+1) by POWER:47
.= ((-x) to_power 3)*((-x) to_power 1) by A5,POWER:32
.= ((-x)|^ 3)*((-x) to_power 1) by POWER:47;
then A10: x|^ 4 = ((-x)|^ 3)*(-x) by POWER:30;
3 = 2*1+1;
then (-x)|^ 3 = -(x|^ 3) by POWER:2;
then (x|^ 3)*x = x|^ 4 by A10,XCMPLX_1:177;
then x|^ 4 = x^2*(x*x) by A8,A9,XCMPLX_1:4;
hence thesis by A6,A7,A9,A10,SQUARE_1:def 3,XCMPLX_1:176,179;
end;
theorem Th5:
for x,y being real number st x+y <> 0 holds
(x+y)|^ 4 = (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*x
+ (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*y
proof
let x,y be real number;
assume
A1: x+y <> 0;
per cases by A1,AXIOMS:21;
suppose A2: x+y>0;
(x+y)|^ 4 = (x+y) to_power (3+1) by A1,POWER:46
.= ((x+y) to_power 3)*((x+y) to_power 1) by A2,POWER:32
.= ((x+y) to_power 3)*(x+y) by POWER:30;
then (x+y)|^ 4 = ((x+y)|^ 3)*(x+y) by A1,POWER:46
.= (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*(x+y) by POLYEQ_1:14;
hence thesis by XCMPLX_1:8;
suppose x+y<0;
then A3: -(x+y)>0 by REAL_1:66;
(-(x+y))|^ 4 = (x+y)|^ 4 by Lm1,POWER:1;
then (x+y)|^ 4 = (-(x+y)) to_power (3+1) by POWER:47
.= ((-(x+y)) to_power 3)*((-(x+y)) to_power 1) by A3,POWER:32
.= ((-(x+y))|^ 3)*((-(x+y)) to_power 1) by POWER:47;
then A4: (x+y)|^ 4 = ((-(x+y))|^ 3)*(-(x+y)) by POWER:30;
3 = 2*1+1;
then (x+y)|^ 4 = (-((x+y)|^ 3))*(-(x+y)) by A4,POWER:2
.= ((x+y)|^ 3)*(x+y) by XCMPLX_1:177
.= (x|^ 3 +((3*y)*x^2+(3*y^2)*x)+y|^ 3)*(x+y) by POLYEQ_1:14;
hence thesis by XCMPLX_1:8;
end;
theorem
for x,y being real number st x+y <> 0 holds
(x+y)|^ 4 = x|^ 4+((4*y)*(x|^ 3)+6*y^2*x^2+4*(y|^ 3)*x)+y|^ 4
proof
let x,y be real number;
assume
A1: x+y<>0;
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;
set s = u+(4*y)*q;
set k = (3*y^2)*x^2+p*x;
set m = q*y+(3*y^2)*x^2;
set ss = ((4*y)*q+(6*y^2)*x^2);
A2: (x+y)|^ 4 = g+h by A1,Th5;
A3: g = (x|^ 3)*x +((3*y)*x^2+(3*y^2)*x)*x+(y|^ 3)*x by XCMPLX_1:9;
h = (x|^ 3)*y +((3*y)*x^2+(3*y^2)*x)*y+((y|^ 3)*y) by XCMPLX_1:9
.= (x|^ 3)*y +((3*y)*x^2+(3*y^2)*x)*y+(y|^ 4) by Th4;
then (x+y)|^ 4 = (x|^ 4) +((3*y)*x^2+(3*y^2)*x)*x+(y|^ 3)*x
+((x|^ 3)*y +((3*y)*x^2+(3*y^2)*x)*y+(y|^ 4))
by A2,A3,Th4;
then (x+y)|^ 4 = u +((3*y)*x^2--(3*y^2)*x)*x+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by XCMPLX_1:151
.= 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 XCMPLX_1:40
.= 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 XCMPLX_1:4
.= u +((3*y)*q-(-(3*y^2)*x)*x)+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by Th4
.= u +((3*y)*q-(-(((3*y^2)*x)*x)))+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v)by XCMPLX_1:175
.= u +((3*y)*q-(-((3*y^2)*(x*x))))+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by XCMPLX_1:4
.= u +((3*y)*q-(-((3*y^2)*x^2)))+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by SQUARE_1:def 3
.= u +((3*y)*q+((3*y^2)*x^2))+p*x
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by XCMPLX_1:151
.= u +(((3*y)*q+((3*y^2)*x^2))+p*x)
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by XCMPLX_1:1
.= u +((3*y)*q+(((3*y^2)*x^2)+p*x))
+(q*y +((3*y)*x^2+(3*y^2)*x)*y+v) by XCMPLX_1:1
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +((((3*y)*x^2)+((3*y^2)*x)+0)*y)+v) by XCMPLX_1:1
.= u + (3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y+(((3*y)*x^2)*y+((3*y^2)*x)*y+0*y)+v) by XCMPLX_1:9
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +((3*y*y*x^2)+(3*y^2)*x*y)+v) by XCMPLX_1:4
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +(((3*(y*y))*x^2)+(3*y^2)*x*y)+v) by XCMPLX_1:4
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +(((3*y^2)*x^2)+(3*y^2)*x*y)+v) by SQUARE_1:def 3;
then A4: (x+y)|^ 4 = u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +(((3*y^2)*x^2)+(3*y^2*y*x))+v) by XCMPLX_1:4;
y|^ 3 = y^2*y & (y|^ 3)*y = y|^ 4 & y^2*y^2 = y|^ 4 by Th4;
then (x+y)|^ 4 = u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +(((3*y^2)*x^2)+(3*p*x))+v) by A4,XCMPLX_1:4
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+((q*y +(3*y^2)*x^2+(3*p*x))+v) by XCMPLX_1:1
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+((q*y +(3*y^2)*x^2)+((3*p*x)+v)) by XCMPLX_1:1
.= u +(3*y)*q+(((3*y^2)*x^2)+p*x)
+(q*y +(3*y^2)*x^2)+((3*p*x)+v) by XCMPLX_1:1
.= (u +(3*y)*q)+k--m+((3*p*x)+v) by XCMPLX_1:151
.= (u +(3*y)*q)-(-m)+k+((3*p*x)+v) by XCMPLX_1:29
.= (u +(3*y)*q)+m+k+((3*p*x)+v) by XCMPLX_1:151
.= (u +((3*y)*q+m))+k+((3*p*x)+v) by XCMPLX_1:1
.= (u +(((3*y)*q+y*q+0*q)+(3*y^2)*x^2))+k+((3*p*x)+v) by XCMPLX_1:1
.= (u +((3*y+1*y+0*y)*q+(3*y^2)*x^2))+k+((3*p*x)+v) by XCMPLX_1:9
.= (u +((3+1+0)*y*q+(3*y^2)*x^2))+k+((3*p*x)+v) by XCMPLX_1:9
.= ((u +4*y*q)+(3*y^2)*x^2)+k+((3*p*x)+v) by XCMPLX_1:1
.= ((u+4*y*q)+((3*y^2)*x^2+k))+((3*p*x)+v) by XCMPLX_1:1
.= s+(((3*y^2)*x^2+(3*y^2)*x^2+0*x^2)+p*x) +((3*p*x)+v) by XCMPLX_1:1
.= s+((3*y^2+3*y^2+0*y^2)*x^2+p*x)+((3*p*x)+v) by XCMPLX_1:9
.= s+((3+3+0)*y^2*x^2+p*x)+((3*p*x)+v) by XCMPLX_1:9
.= s+(((6*y^2)*x^2+p*x)+((3*p*x)+v)) by XCMPLX_1:1
.= s+((6*y^2)*x^2+(p*x+((3*p*x)+v))) by XCMPLX_1:1
.= s+((6*y^2)*x^2+((p*x+(3*p)*x+0*x)+v)) by XCMPLX_1:1
.= s+((6*y^2)*x^2+((1*p+3*p+0*p)*x+v)) by XCMPLX_1:9
.= s+((6*y^2)*x^2+((1+3+0)*p*x+v)) by XCMPLX_1:9
.= (s+(6*y^2)*x^2)+(4*p*x+v) by XCMPLX_1:1
.= (u+((4*y)*q+(6*y^2)*x^2))+(4*p*x+v) by XCMPLX_1:1
.= u+(ss+(4*p*x+v)) by XCMPLX_1:1
.= u+((ss+4*p*x)+v) by XCMPLX_1:1;
hence thesis by XCMPLX_1:1;
end;
theorem Th7:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x)) implies
a5=b5 & a1-a2+a3-a4 = b1-b2+b3-b4 & a1+a2+a3+a4 = b1+b2+b3+b4
proof
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be real number;
assume
A1: for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x);
then Four(a1,a2,a3,a4,a5,0) = Four(b1,b2,b3,b4,b5,0);
then a1*(0|^ 4)+a2*(0|^ 3)+a3*0^2+a4*0+a5=Four(b1,b2,b3,b4,b5,0)
by Def1;
then A2: a1*(0|^ 4)+a2*(0|^ 3)+a3*0^2+a5
= b1*(0|^ 4)+b2*(0|^ 3)+b3*0+b4*0+b5 by Def1,SQUARE_1:60;
A3: 0|^ 3 =0 by NEWTON:16;
A4: 0|^ 4 = 0 by NEWTON:16;
Four(a1,a2,a3,a4,a5,1) = Four(b1,b2,b3,b4,b5,1) by A1;
then a1*(1|^ 4)+a2*(1|^ 3)+a3*1^2+a4*1+a5 = Four(b1,b2,b3,b4,b5,1)
by Def1;
then A5: a1*(1|^ 4)+a2*(1|^ 3)+a3*1+a4*1+a5
= b1*(1|^ 4)+b2*(1|^ 3)+b3*1+b4*1+b5 by Def1,SQUARE_1:59;
A6: 1|^ 3 = 1 by NEWTON:15;
A7: 1|^ 4 = 1 by NEWTON:15;
set m=a1+a2+a3+a4;
set n= b1+b2+b3+b4;
m-n=b5-b5 by A2,A3,A4,A5,A6,A7,SQUARE_1:60,XCMPLX_1:33;
then m-n+n=0+n by XCMPLX_1:14;
then n-n+m=0+n by XCMPLX_1:30;
then A8: 0+m=0+n by XCMPLX_1:14;
set x=-1;
Four(a1,a2,a3,a4,a5,-1) = Four(b1,b2,b3,b4,b5,-1) by A1;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2+a4*(-1)+a5
= Four(b1,b2,b3,b4,b5,-1) by Def1;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2+a4*(-1)+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+b4*(-1)+b5 by Def1;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2+(-(a4*1))+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+(b4*(-1))+b5 by XCMPLX_1:175
.= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+(-(b4*1))+b5 by XCMPLX_1:175;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2+(-a4-0)+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+(-b4)+b5;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2-a4-0+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+(-b4)+b5 by XCMPLX_1:158;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*(-1)^2-a4+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2+(-b4-0)+b5
.= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2-b4-0+b5 by XCMPLX_1:158
.= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2-b4+b5;
then a1*(-1)|^ 4+a2*(-1)|^ 3+a3*1^2-a4+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*(-1)^2-b4+b5 by SQUARE_1:61;
then A9: a1*(-1)|^ 4+a2*(-1)|^ 3+a3*1-a4+a5
= b1*(-1)|^ 4+b2*(-1)|^ 3+b3*1-b4+b5 by SQUARE_1:59,61;
x|^ 3=x^2*x & (x|^ 3)*x=x|^ 4 & x^2*x^2 = x|^ 4 by Th4;
then (-1)|^ 3=1^2*(-1) by SQUARE_1:61;
then a1*(-1)|^ 4+-a2*1+a3-a4+a5
= b1*(-1)|^ 4+b2*(-1)+b3-b4+b5 by A9,SQUARE_1:59,XCMPLX_1:175;
then a1*(-1)|^ 4+(-a2*1)+a3-a4+a5
= b1*(-1)|^ 4+(-b2*1)+b3-b4+b5 by XCMPLX_1:175;
then a1*(-1)|^ 4+(-a2-0)+a3-a4+a5
= b1*(-1)|^ 4+(-b2-0)+b3-b4+b5;
then A10: a1*(-1)|^ 4-a2-0+a3-a4+a5
= b1*(-1)|^ 4+(-b2-0)+b3-b4+b5 by XCMPLX_1:158
.= b1*(-1)|^ 4-b2-0+b3-b4+b5 by XCMPLX_1:158;
A11: 1|^ 4 = 1 by NEWTON:15;
4=2*2;
then (-1)|^ 4=1 by A11,POWER:1;
then a1*1-a2+a3-a4+(a5-a5) = b1*1-b2+b3-b4+b5-a5 by A10,XCMPLX_1:29;
then a1*1-a2+a3-a4+0 = b1*1-b2+b3-b4+b5-a5 by XCMPLX_1:14;
then a1*1-a2+a3-a4 = b1*1-b2+b3-b4+(b5-b5) by A2,A3,A4,SQUARE_1:60,
XCMPLX_1:29;
then a1*1-a2+a3-a4 = b1*1-b2+b3-b4+0 by XCMPLX_1:14;
hence thesis by A2,A3,A4,A8,SQUARE_1:60;
end;
theorem Th8:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x)=Four(b1,b2,b3,b4,b5,x)) implies
a1-b1=b3-a3 & a2-b2=b4-a4
proof
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be real number;
assume
A1: for x being real number holds
Four(a1,a2,a3,a4,a5,x)=Four(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;
then (a1-a2+(a3-a4))+(a1+a2+a3+a4)=(b1-b2+b3-b4)+(b1+b2+b3+b4)
by XCMPLX_1:29;
then (a1-a2+(a3-a4))+((a1+a2)+a3+a4)=(b1-b2+(b3-b4))
+((b1+b2)+b3+b4) by XCMPLX_1:29;
then (a1-a2+(a3-a4))+((a1+a2)+(a3+a4))=(b1-b2+(b3-b4))
+((b1+b2)+b3+b4) by XCMPLX_1:1;
then (a1-a2+(a3-a4))+((a1+a2)+(a3+a4))=(b1-b2+(b3-b4))
+((b1+b2)+(b3+b4)) by XCMPLX_1:1;
then (a1-a2+(a3-a4))+(a1+a2)+(a3+a4)=(b1-b2+(b3-b4))
+((b1+b2)+(b3+b4)) by XCMPLX_1:1;
then (a1-a2+(a3-a4))+(a1+a2)+(a3+a4)=(b1-b2+(b3-b4))
+(b1+b2)+(b3+b4) by XCMPLX_1:1;
then ((a3-a4)-a2+a1)+(a1+a2)+(a3+a4)=(b1-b2+(b3-b4))
+(b1+b2)+(b3+b4) by XCMPLX_1:30;
then ((a3-a4)-a2+a1)+(a1+a2)+(a3+a4)=((b3-b4)-b2+b1)
+(b1+b2)+(b3+b4) by XCMPLX_1:30;
then ((a3-a4)-(a2-a1))+(a1+a2)+(a3+a4)
=((b3-b4)-b2+b1)+(b1+b2)+(b3+b4) by XCMPLX_1:37;
then ((a3-a4)-(a2-a1))+(a1+a2)+(a3+a4)
=((b3-b4)-(b2-b1))+(b1+b2)+(b3+b4) by XCMPLX_1:37;
then ((a3-a4)+(-(a2-a1)))+(a1+a2)+(a3+a4)
=((b3-b4)-(b2-b1))+(b1+b2)+(b3+b4) by XCMPLX_0:def 8;
then ((a3-a4)+(-(a2-a1)))+(a1+a2)+(a3+a4)
=((b3-b4)+(-(b2-b1)))+(b1+b2)+(b3+b4) by XCMPLX_0:def 8;
then (a3-a4)+((-(a2-a1))+(a1+a2))+(a3+a4)
=(b3-b4)+(-(b2-b1))+(b1+b2)+(b3+b4) by XCMPLX_1:1;
then (a3-a4)+((-(a2-a1))+(a1+a2))+(a3+a4)
=(b3-b4)+((-(b2-b1))+(b1+b2))+(b3+b4) by XCMPLX_1:1;
then (a3-a4)+((-(a2-a1))+a1+a2)+(a3+a4)
=(b3-b4)+((-(b2-b1))+(b1+b2))+(b3+b4) by XCMPLX_1:1;
then (a3-a4)+((-(a2-a1))+a1+a2)+(a3+a4)
=(b3-b4)+((-(b2-b1))+b1+b2)+(b3+b4) by XCMPLX_1:1;
then (a3-a4)+(a1-a2+a1+a2)+(a3+a4)
=(b3-b4)+((-(b2-b1))+b1+b2)+(b3+b4) by XCMPLX_1:143;
then (a3-a4)+(a1-a2+a1+a2)+(a3+a4)
=(b3-b4)+(b1-b2+b1+b2)+(b3+b4) by XCMPLX_1:143;
then (a3-a4)+(a1+a1-a2+a2)+(a3+a4)
=(b3-b4)+(b1-b2+b1+b2)+(b3+b4) by XCMPLX_1:29;
then (a3-a4)+(a1+a1-a2+a2)+(a3+a4)
=(b3-b4)+(b1+b1-b2+b2)+(b3+b4) by XCMPLX_1:29;
then (a3-a4)+(a1+a1-(a2-a2))+(a3+a4)
=(b3-b4)+(b1+b1-b2+b2)+(b3+b4) by XCMPLX_1:37;
then (a3-a4)+(a1+a1-(a2-a2))+(a3+a4)
=(b3-b4)+(b1+b1-(b2-b2))+(b3+b4) by XCMPLX_1:37;
then (a3-a4)+(a1+a1-0)+(a3+a4)
=(b3-b4)+(b1+b1-(b2-b2))+(b3+b4) by XCMPLX_1:14;
then (a3-a4)+(a1+a1)+(a3+a4)
=(b3-b4)+(b1+b1-0)+(b3+b4) by XCMPLX_1:14;
then (a3-a4)+(2*a1)+(a3+a4)
=(b3-b4)+(b1+b1)+(b3+b4) by XCMPLX_1:11;
then (a3-a4)+(2*a1)+(a3+a4) =(b3-b4)+(2*b1)+(b3+b4) by XCMPLX_1:11;
then 2*a1+(a3-a4)+a3+a4 =2*b1+(b3-b4)+(b3+b4) by XCMPLX_1:1;
then 2*a1+(a3-a4)+a3+a4 =2*b1+(b3-b4)+b3+b4 by XCMPLX_1:1;
then 2*a1+((a3-a4)+a3)+a4 =2*b1+(b3-b4)+b3+b4 by XCMPLX_1:1
.=2*b1+((b3-b4)+b3)+b4 by XCMPLX_1:1;
then 2*a1+(-a4+a3+a3)+a4 =2*b1+(b3-b4+b3)+b4 by XCMPLX_1:156
.=2*b1+(-b4+b3+b3)+b4 by XCMPLX_1:156;
then 2*a1+(-a4+(a3+a3))+a4 =2*b1+(-b4+b3+b3)+b4 by XCMPLX_1:1
.=2*b1+(-b4+(b3+b3))+b4 by XCMPLX_1:1;
then 2*a1+(-a4+(2*a3))+a4 =2*b1+(-b4+(b3+b3))+b4 by XCMPLX_1:11
.=2*b1+(-b4+(2*b3))+b4 by XCMPLX_1:11;
then 2*a1+((-a4+(2*a3))+a4) =2*b1+(-b4+(2*b3))+b4 by XCMPLX_1:1;
then 2*a1+(-a4+(2*a3)+a4) =2*b1+(-b4+(2*b3)+b4) by XCMPLX_1:1;
then 2*a1+(a4-a4+(2*a3)) =2*b1+((-b4+(2*b3))+b4) by XCMPLX_1:156
.=2*b1+(b4-b4+(2*b3)) by XCMPLX_1:156;
then 2*a1+(0+(2*a3)) = 2*b1+((b4-b4)+(2*b3)) by XCMPLX_1:14
.= 2*b1+(0+(2*b3)) by XCMPLX_1:14;
then 2*(a1+a3) = 2*b1+2*b3 by XCMPLX_1:8
.= 2*(b1+b3) by XCMPLX_1:8;
then 2*(a1+a3)-2*(b1+b3) = 0 by XCMPLX_1:14;
then 2*((a1+a3)-(b1+b3)) = 0 by XCMPLX_1:40;
then (a1+a3)-(b1+b3) = 0 by XCMPLX_1:6;
then A2: a1+a3=b1+b3 by XCMPLX_1:15;
a1-a2+a3-a4=b1-b2+b3-b4 &
a1+a2+a3+a4=b1+b2+b3+b4 by A1,Th7;
then (a1-a2+a3-a4)-((a1+a2)+(a3+a4))=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:1;
then (a1-a2+a3-a4)-(a3+a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:36;
then (a1-a2+a3-(a3+a4)-a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:21;
then (a1-a2+a3-a3-a4-a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:36;
then (a1-a2+(a3-a3)-a4-a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:29;
then (a1-a2+0-a4-a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:14;
then (a1-a2-(a4+a4))-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4)
by XCMPLX_1:36;
then (a1-a2-2*a4)-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:11
;
then (a1-(a2+2*a4))-(a1+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:
36
;
then (a1-(a2+2*a4))-a1-a2=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:36
;
then a1-a1-(a2+2*a4)-a2=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:21
;
then 0-(a2+2*a4)-a2=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:14;
then -(a2+2*a4)-a2=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:150;
then -(-(-2*a4)+a2+a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:161;
then -(-(-2*a4)+(a2+a2))=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:1;
then -(-(-2*a4)+2*a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:11;
then ((-2*a4)-2*a2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:163;
then ((-2*a2)-2*a4)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:144;
then ((2*(-a2))-2*a4) = (b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:175
;
then ((2*(-a2))+(-2*a4))=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_0:def
8
;
then 2*(-a2)+2*(-a4)+2*0=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:175
;
then 2*((-a2)+(-a4)+0)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:9;
then 2*(-(a2+a4))=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:140;
then (a2+a4)*(-2)=(b1-b2+b3-b4)-(b1+b2+b3+b4) by XCMPLX_1:176
.=(b1-b2+b3-b4)-((b1+b2)+(b3+b4)) by XCMPLX_1:1
.=(b1-b2+b3-b4)-(b3+b4)-(b1+b2) by XCMPLX_1:36
.=(b1-b2+b3-(b3+b4)-b4)-(b1+b2) by XCMPLX_1:21
.=(b1-b2+b3-b3-b4-b4)-(b1+b2) by XCMPLX_1:36
.=(b1-b2+(b3-b3)-b4-b4)-(b1+b2) by XCMPLX_1:29
.=(b1-b2+0-b4-b4)-(b1+b2) by XCMPLX_1:14
.=(b1-b2-(b4+b4))-(b1+b2) by XCMPLX_1:36
.=(b1-b2-2*b4)-(b1+b2) by XCMPLX_1:11
.=(b1-(b2+2*b4))-(b1+b2) by XCMPLX_1:36
.=b1-(b1+b2)-(b2+2*b4) by XCMPLX_1:21
.=b1-b1-b2-(b2+2*b4) by XCMPLX_1:36
.=0-b2-(b2+2*b4) by XCMPLX_1:14
.=-b2-(b2+2*b4) by XCMPLX_1:150
.=-b2-b2-2*b4 by XCMPLX_1:36
.=-(b2+b2)-2*b4 by XCMPLX_1:161
.=-2*b2-2*b4 by XCMPLX_1:11
.=-2*b2+-2*b4 by XCMPLX_0:def 8
.=(2*(-b2))+(-2*b4) by XCMPLX_1:175
.=(2*(-b2)+2*(-b4)+2*0) by XCMPLX_1:175
.=2*((-b2)+(-b4)+0) by XCMPLX_1:9
.=2*(-(b2+b4)) by XCMPLX_1:140
.=(b2+b4)*(-2) by XCMPLX_1:176;
then ((a2+a4)*(-2))-((b2+b4)*(-2))=0 by XCMPLX_1:14;
then (-(a2+a4)*2)-((b2+b4)*(-2))=0 by XCMPLX_1:175;
then (-(a2+a4)*2)-(-(b2+b4)*2)=0 by XCMPLX_1:175;
then -(a2+a4)*2+(b2+b4)*2=0 by XCMPLX_1:151;
then -((a2+a4)*2-(b2+b4)*2+0*2)=0 by XCMPLX_1:162;
then -(((a2+a4)-(b2+b4)+0)*2)=0 by XCMPLX_1:44;
then ((a2+a4)-(b2+b4))*2*2"=0*2" by REAL_1:26;
then ((a2+a4)-(b2+b4))*(2*(1/2))=0 by XCMPLX_1:4;
then (a2+a4)=(b2+b4) by XCMPLX_1:15;
hence thesis by A2,XCMPLX_1:33;
end;
theorem Th9:
for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being real number st
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x)) holds
a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5
proof
let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be real number;
assume
A1: for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four(b1,b2,b3,b4,b5,x);
then A2: a1-b1 = b3-a3 by Th8;
A3: a2-b2 = b4-a4 by A1,Th8;
A4: a5 = b5 by A1,Th7;
Four(a1,a2,a3,a4,a5,2) = Four(b1,b2,b3,b4,b5,2) by A1;
then a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2+a5
= Four(b1,b2,b3,b4,b5,2) by Def1;
then a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2+a5
= b1*(2|^ 4)+b2*(2|^ 3)+b3*2^2+b4*2+b5 by Def1;
then a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2+(a5-a5)
= b1*(2|^ 4)+b2*(2|^ 3)+b3*2^2+b4*2+b5-a5 by XCMPLX_1:29;
then a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2+(a5-a5)
= b1*(2|^ 4)+b2*(2|^ 3)+b3*2^2+b4*2+(b5-a5) by XCMPLX_1:29;
then a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2+0
= b1*(2|^ 4)+b2*(2|^ 3)+b3*2^2+b4*2+(b5-a5) by XCMPLX_1:14;
then A5: a1*(2|^ 4)+a2*(2|^ 3)+a3*2^2+a4*2
= b1*(2|^ 4)+b2*(2|^ 3)+b3*2^2+b4*2+0 by A4,XCMPLX_1:14;
A6: 2^2 = 2*2 by SQUARE_1:def 3;
A7: 2|^ 4 = 16 by ASYMPT_1:46,POWER:47;
2|^ 3 = 8 by ASYMPT_1:45,POWER:47;
then (a1*16+a2*8+a3*4+a4*2)- (b1*16+b2*8+b3*4+b4*2) = 0
by A5,A6,A7,XCMPLX_1:14;
then (a1*16+a2*8+a3*4+a4*2)- (b1*16+b2*8+(b3*4+b4*2)) = 0
by XCMPLX_1:1;
then (a1*16+a2*8+(a3*4+a4*2))- ((b1*16+b2*8)+(b3*4+b4*2)) = 0
by XCMPLX_1:1;
then ((a1*16+a2*8)+(a3*4+a4*2))- (b1*16+b2*8)-(b3*4+b4*2) = 0
by XCMPLX_1:36;
then (a1*16+a2*8)- (b1*16+b2*8)+(a3*4+a4*2)- (b3*4+b4*2) = 0
by XCMPLX_1:29;
then (a1*16+a2*8)- b1*16-b2*8+(a3*4+a4*2)- (b3*4+b4*2) = 0
by XCMPLX_1:36;
then a1*16- b1*16+a2*8-b2*8+(a3*4+a4*2)- (b3*4+b4*2) = 0
by XCMPLX_1:29;
then (a1- b1)*16+a2*8-b2*8+(a3*4+a4*2)- (b3*4+b4*2) = 0
by XCMPLX_1:40;
then (a1- b1)*16+(a2*8-b2*8)+(a3*4+a4*2)- (b3*4+b4*2) = 0
by XCMPLX_1:29;
then (a1- b1)*16+(a2-b2)*8+(a3*4+a4*2)- (b3*4+b4*2) = 0 by XCMPLX_1:
40
;
then (a1- b1)*16+(a2-b2)*8+(a3*4+a4*2)- b3*4-b4*2 = 0 by XCMPLX_1:36
;
then (a1- b1)*16+(a2-b2)*8+a3*4+a4*2- b3*4-b4*2 = 0 by XCMPLX_1:1;
then (a1- b1)*16+(a2-b2)*8+a3*4- b3*4+a4*2-b4*2 = 0 by XCMPLX_1:29
;
then (a1- b1)*16+(a2-b2)*8+(a3*4- b3*4)+a4*2-b4*2 = 0 by XCMPLX_1:29
;
then (a1- b1)*16+(a2-b2)*8+(a3- b3)*4+a4*2-b4*2 = 0 by XCMPLX_1:40;
then (a1- b1)*16+(a2-b2)*8+(a3- b3)*4+(a4*2-b4*2) = 0 by XCMPLX_1:29
;
then (a1- b1)*16+(a2-b2)*8+(a3- b3)*4+(a4-b4)*2 = 0 by XCMPLX_1:40;
then (b3- a3)*16+(a2-b2)*8+(a3- b3)*4+(a4-b4)*2 = 0
by A1,Th8;
then (b3- a3)*16+(b4-a4)*8+-(-(a3- b3)*4)+(a4-b4)*2 = 0
by A1,Th8;
then (b3- a3)*16+(b4-a4)*8-(-(a3- b3)*4)+(a4-b4)*2 = 0
by XCMPLX_0:def 8;
then (b3- a3)*16-(-(a3- b3)*4)+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_1:29
;
then (b3- a3)*16+(a3- b3)*4+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_1:151;
then (b3- a3)*16+(-(b3-a3))*4+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_1:143
;
then (b3- a3)*16+-((b3-a3)*4)+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_1:175
;
then (b3- a3)*16-((b3-a3)*4)+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_0:def
8
;
then (b3- a3)*(16-4)+(b4-a4)*8+(a4-b4)*2 = 0 by XCMPLX_1:40;
then (b3- a3)*12+((b4-a4)*8+(a4-b4)*2) = 0 by XCMPLX_1:1;
then (b3- a3)*12+((b4-a4)*8+(-(b4-a4))*2) = 0 by XCMPLX_1:143;
then (b3- a3)*12+((b4-a4)*8+-(b4-a4)*2) = 0 by XCMPLX_1:175;
then (b3- a3)*12+((b4-a4)*8-(b4-a4)*2) = 0 by XCMPLX_0:def 8;
then A8: (b3- a3)*12+(b4-a4)*(8-2) = 0 by XCMPLX_1:40;
A9: 6+0 = 8-2;
Four(a1,a2,a3,a4,a5,-2) = Four(b1,b2,b3,b4,b5,-2) by A1;
then a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)+a5
= Four(b1,b2,b3,b4,b5,-2) by Def1;
then a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)+a5
= b1*(-2)|^ 4+b2*(-2)|^ 3+b3*(-2)^2+b4*(-2)+b5 by Def1;
then a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)+(a5-a5)
= b1*(-2)|^ 4+b2*(-2)|^ 3+b3*(-2)^2+b4*(-2)+b5-a5
by XCMPLX_1:29;
then a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)+(a5-a5)
= b1*(-2)|^ 4+b2*(-2)|^ 3+b3*(-2)^2+b4*(-2)+(b5-a5)
by XCMPLX_1:29;
then a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)+0
= b1*(-2)|^ 4+b2*(-2)|^ 3+b3*(-2)^2+b4*(-2)+(b5-a5)
by XCMPLX_1:14;
then A10: a1*(-2)|^ 4+a2*(-2)|^ 3+a3*(-2)^2+a4*(-2)
= b1*(-2)|^ 4+b2*(-2)|^ 3+b3*(-2)^2+b4*(-2)+0
by A4,XCMPLX_1:14;
A11: (-2)^2 = 4 by A6,SQUARE_1:61;
A12: (-2)|^ 4 = 16 by A7,Lm1,POWER:1;
(-2)|^ 3 = (-2)^2*(-2) by Th4
.= 4*(-2) by A6,SQUARE_1:61
.= -(4*2);
then a1*16+(-(a2*8))+a3*4+a4*(-2) = b1*16+b2*(-8)+b3*4+b4*(-2)
by A10,A11,A12,XCMPLX_1:175;
then a1*16+(-(a2*8))+a3*4+a4*(-2)
= b1*16+(-(b2*8))+b3*4+b4*(-2) by XCMPLX_1:175;
then a1*16+(-(a2*8))+a3*4+(-(a4*2))
= b1*16+(-(b2*8))+b3*4+b4*(-2) by XCMPLX_1:175
.= b1*16+(-(b2*8))+b3*4+(-(b4*2)) by XCMPLX_1:175;
then a1*16-a2*8+a3*4+(-(a4*2))
= b1*16+(-(b2*8))+b3*4+(-(b4*2)) by XCMPLX_0:def 8
.= b1*16-b2*8+b3*4+(-(b4*2)) by XCMPLX_0:def 8;
then a1*16-a2*8+a3*4-a4*2
= b1*16-b2*8+b3*4+(-(b4*2)) by XCMPLX_0:def 8
.= b1*16-b2*8+b3*4-b4*2 by XCMPLX_0:def 8;
then (a1*16-a2*8+a3*4-a4*2)-(b1*16-b2*8+b3*4-b4*2) = 0
by XCMPLX_1:14;
then (a1*16-a2*8+a3*4-a4*2)-(b1*16-b2*8+(b3*4-b4*2)) = 0
by XCMPLX_1:29;
then ((a1*16-a2*8)+(a3*4-a4*2))-((b1*16-b2*8)+(b3*4-b4*2)) = 0
by XCMPLX_1:29;
then ((a1*16-a2*8)+(a3*4-a4*2))-(b1*16-b2*8)-(b3*4-b4*2) = 0
by XCMPLX_1:36;
then (a1*16-a2*8)-(b1*16-b2*8)+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:29;
then ((a1*16-a2*8)-b1*16+b2*8)+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:37;
then (a1*16-b1*16-a2*8+b2*8)+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:21;
then ((a1-b1)*16-a2*8+b2*8)+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:40;
then ((a1-b1)*16-(a2*8-b2*8))+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:37;
then ((a1-b1)*16-(a2-b2)*8)+(a3*4-a4*2)-(b3*4-b4*2) = 0
by XCMPLX_1:40;
then ((a1-b1)*16-(a2-b2)*8)+(a3*4-a4*2)-b3*4+b4*2 = 0 by XCMPLX_1:37
;
then ((a1-b1)*16-(a2-b2)*8)+a3*4-a4*2-b3*4+b4*2 = 0 by XCMPLX_1:29;
then ((a1-b1)*16-(a2-b2)*8)+a3*4-b3*4-a4*2+b4*2 = 0 by XCMPLX_1:21
;
then ((a1-b1)*16-(a2-b2)*8)+(a3*4-b3*4)-a4*2+b4*2 = 0 by XCMPLX_1:29
;
then ((a1-b1)*16-(a2-b2)*8)+(a3-b3)*4-a4*2+b4*2 = 0 by XCMPLX_1:40;
then ((a1-b1)*16-(a2-b2)*8)+(a3-b3)*4-(a4*2-b4*2) = 0 by XCMPLX_1:37
;
then (b3-a3)*16-(b4-a4)*8+(a3-b3)*4-(a4-b4)*2 = 0
by A2,A3,XCMPLX_1:40;
then -(b4-a4)*8+(a3-b3)*4+(b3-a3)*16-(a4-b4)*2 = 0
by XCMPLX_1:156;
then -(b4-a4)*8+((b3-a3)*16+(a3-b3)*4)-(a4-b4)*2 = 0
by XCMPLX_1:1;
then -(b4-a4)*8+((b3-a3)*16+(-(b3-a3))*4)-(a4-b4)*2 = 0
by XCMPLX_1:143;
then -(b4-a4)*8+((b3-a3)*16+-((b3-a3)*4))-(a4-b4)*2 = 0
by XCMPLX_1:175;
then -(b4-a4)*8+((b3-a3)*16-(b3-a3)*4)-(a4-b4)*2 = 0
by XCMPLX_0:def 8;
then -(-(a4-b4))*8+((b3-a3)*16-(b3-a3)*4)-(a4-b4)*2 = 0
by XCMPLX_1:143;
then -(-(a4-b4)*8)+((b3-a3)*16-(b3-a3)*4)-(a4-b4)*2 = 0
by XCMPLX_1:175;
then ((a4-b4)*8-(a4-b4)*2)+((b3-a3)*16-(b3-a3)*4) = 0
by XCMPLX_1:29;
then (a4-b4)*6+((b3-a3)*16-(b3-a3)*4) = 0 by A9,XCMPLX_1:40;
then (a4-b4)*6+(b3-a3)*(16-4) = 0 by XCMPLX_1:40;
then (b3-a3)*12+(-(b4-a4))*6 = 0 by XCMPLX_1:143;
then A13: (b3-a3)*12+-((b4-a4)*6) = 0 by XCMPLX_1:175;
then A14: (b3-a3)*12-(b4-a4)*6 = 0 by XCMPLX_0:def 8;
(b3-a3)*12+(b4-a4)*6+(b3-a3)*12-(b4-a4)*6= 0
by A8,A13,XCMPLX_0:def 8;
then (b3-a3)*12+(b4-a4)*6-(b4-a4)*6+(b3-a3)*12= 0 by XCMPLX_1:29;
then (b3-a3)*12+((b4-a4)*6-(b4-a4)*6)+(b3-a3)*12= 0 by XCMPLX_1:29;
then (b3-a3)*12+0+(b3-a3)*12= 0 by XCMPLX_1:14;
then 2*((b3-a3)*12)= 0 by XCMPLX_1:11;
then (b3-a3)*12= 0 by XCMPLX_1:6;
then A15: b3-a3= 0 by XCMPLX_1:6;
then b3-a3+a3 = a3;
then b3-(a3-a3) = a3 by XCMPLX_1:37;
then A16: b3-0 = a3 by XCMPLX_1:14;
(b3-a3)*12+(b4-a4)*6-((b3-a3)*12-(b4-a4)*6)= 0
by A8,A14;
then (b3-a3)*12+(b4-a4)*6-(b3-a3)*12+(b4-a4)*6= 0 by XCMPLX_1:37;
then (b3-a3)*12-(b3-a3)*12+(b4-a4)*6+(b4-a4)*6= 0 by XCMPLX_1:29;
then 0+(b4-a4)*6+(b4-a4)*6= 0 by XCMPLX_1:14;
then 2*((b4-a4)*6)= 0 by XCMPLX_1:11;
then (b4-a4)*6=0 by XCMPLX_1:6;
then (b4-a4)= 0 by XCMPLX_1:6;
then b4-(a4-a4)= 0+a4 by XCMPLX_1:37;
then A17: b4-0= 0+a4 by XCMPLX_1:14;
then a2-b2+b2 = 0+b2 by A3,XCMPLX_1:14;
then a2-(b2-b2) = b2 by XCMPLX_1:37;
then A18: a2-0 = b2 by XCMPLX_1:14;
a1-b1+b1 = b1 by A2,A15;
then a1-(b1-b1) = b1 by XCMPLX_1:37;
then a1-0 = b1 by XCMPLX_1:14;
hence thesis by A1,A16,A17,A18,Th7;
end;
definition let a1,x1,x2,x3,x4,x be real number;
func Four0(a1,x1,x2,x3,x4,x) equals :Def2:
a1*((x-x1)*(x-x2)*(x-x3)*(x-x4));
correctness;
end;
definition let a1,x1,x2,x3,x4,x be real number;
cluster Four0(a1,x1,x2,x3,x4,x) -> real;
coherence
proof
a1*((x-x1)*(x-x2)*(x-x3)*(x-x4)) = Four0(a1,x1,x2,x3,x4,x)
by Def2;
hence thesis;
end;
end;
theorem Th10:
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being real number st a1 <> 0 holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x))
implies
(a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1
= x^2*x^2-(x1+x2+x3)*(x^2*x)+(x1*x3+x2*x3+x1*x2)*x^2
- (x1*x2*x3)*x-((x-x1)*(x-x2)*(x-x3))*x4
proof
let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be real number;
assume
A1: a1 <> 0;
assume
for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x);
then Four(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 = Four0(a1,x1,x2,x3,x4,x)
by Def1;
then A2: a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5
= a1*((x-x1)*(x-x2)*(x-x3)*(x-x4)) by Def2;
set w = a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5;
set z = ((x-x1)*(x-x2)*(x-x3)*(x-x4));
w/a1*a1-(z*a1) = (z*a1)-(z*a1) by A1,A2,XCMPLX_1:88;
then w/a1*a1-(z*a1) = 0 by XCMPLX_1:14;
then (w/a1-z)*a1 = 0 by XCMPLX_1:40;
then w/a1-z = 0 by A1,XCMPLX_1:6;
then w/a1+-z= 0-0 by XCMPLX_0:def 8;
then w/a1+0= 0--z by XCMPLX_1:35
.= 0+z by XCMPLX_1:151;
then w*a1" = (((x-x1)*(x-x2)*(x-x3))*(x-x4)) by XCMPLX_0:def 9;
then A3: w*a1" = ((x-x1)*(x-x2)*(x-x3))*x
-((x-x1)*(x-x2)*(x-x3))*x4 by XCMPLX_1:40;
set u = ((x-x1)*(x-x2)*(x-x3))*x4;
w*a1" = (((x-x1)*(x-x2))*x-((x-x1)*(x-x2))*x3)*x-u by A3,XCMPLX_1:40
.= ((((x-x1)*x)-((x-x1)*x2))*x-((x-x1)*(x-x2))*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-((x-x1)*x2))*x-((x-x1)*(x-x2))*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-(x*x2-x1*x2))*x-((x-x1)*(x-x2))*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-(x*x2-x1*x2))*x
-((x-x1)*x-(x-x1)*x2)*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-(x*x2-x1*x2))*x
-((x*x-x1*x)-(x-x1)*x2)*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-(x*x2-x1*x2))*x
-((x*x-x1*x)-(x*x2-x1*x2))*x3)*x-u by XCMPLX_1:40
.= (((x*x-x1*x)-x*x2+x1*x2)*x
-((x*x-x1*x)-(x*x2-x1*x2))*x3)*x-u by XCMPLX_1:37
.= (((x^2-x1*x)-x*x2+x1*x2)*x
-((x*x-x1*x)-(x*x2-x1*x2))*x3)*x-u by SQUARE_1:def 3
.= (((x^2-x1*x)-x*x2+x1*x2)*x
-((x^2-x1*x)-(x*x2-x1*x2))*x3)*x-u by SQUARE_1:def 3
.= ((x^2-x1*x-x*x2+x1*x2)*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:37
.= (((x^2-(x1*x+x*x2))+x1*x2)*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:36
.= (((x^2-(x1*x+x*x2)))*x+x1*x2*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:8
.= ((x^2*x-(x1*x+x*x2)*x)+x1*x2*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:40
.= ((x^2*x-(x1*x*x+x*x2*x))+x1*x2*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:8
.= ((x^2*x-(x1*(x*x)+x*x2*x))+x1*x2*x
-((x^2-x1*x)-x*x2+x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x-(x1*x^2+x*x2*x))+x1*x2*x
-(((x^2-x1*x)-x*x2)+x1*x2+0)*x3)*x-u by SQUARE_1:def 3
.= ((x^2*x-(x1*x^2+x*x2*x))+x1*x2*x
-(((x^2-x1*x)*x3-x*x2*x3)+(x1*x2)*x3))*x-u by XCMPLX_1:44
.= (((x^2*x-(x1*x^2+x*x2*x))+x1*x2*x)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3))*x-u by XCMPLX_1:40
.= ((x^2*x-(x1*x^2+x*x2*x))+x1*x2*x)*x
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:40
.= ((x^2*x-(x1*x^2+x*x2*x))*x+x1*x2*x*x)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:8
.= ((x^2*x-(x1*x^2+x*x2*x))*x+x1*x2*(x*x))
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x-(x1*x^2+x*x2*x))*x+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by SQUARE_1:def 3
.= ((x^2*x*x-(x1*x^2+x*x2*x)*x)+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:40
.= ((x^2*(x*x)-(x1*x^2+x*x2*x)*x)+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x^2-(x1*x^2+x*x2*x)*x)+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by SQUARE_1:def 3
.= ((x^2*x^2-(x1*x^2*x+x*x2*x*x))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:8
.= ((x^2*x^2-(x1*x^2*x+x*x2*(x*x)))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x^2-(x1*x^2*x+(x*x2*x^2)))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by SQUARE_1:def 3
.= ((x^2*x^2-(x1*x^2*x+x2*x^2*x+0*x^2*x))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x^2-(x1*(x^2*x)+x2*x^2*x+0*x^2*x))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x^2-(x1*(x^2*x)+x2*(x^2*x)+0*(x^2*x)))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:4
.= ((x^2*x^2-(x1+x2+0)*(x^2*x))+x1*x2*x^2)
-((x^2*x3-x1*x*x3-x*x2*x3)+(x1*x2)*x3)*x-u by XCMPLX_1:9
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3-(x1*x*x3+x*x2*x3))+(x1*x2)*x3)*x-u by XCMPLX_1:36
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3-(x1*x*x3+x*x2*x3))*x+(x1*x2)*x3*x)-u by XCMPLX_1:8
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-(x1*x*x3+x*x2*x3)*x)+(x1*x2)*x3*x)-u
by XCMPLX_1:40
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-(x1*x*x3*x+x*x2*x3*x))+(x1*x2)*x3*x)-u
by XCMPLX_1:8
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-(x1*x*x3*x+x2*x3*x*x))+(x1*x2)*x3*x)-u
by XCMPLX_1:4
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-(x1*x*x3*x+x2*x3*(x*x)))+(x1*x2)*x3*x)-u
by XCMPLX_1:4
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-(x1*x*x3*x+x2*x3*x^2))+(x1*x2)*x3*x)-u
by SQUARE_1:def 3
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-((x1*x3)*x*x+x2*x3*x^2))+(x1*x2)*x3*x)-u
by XCMPLX_1:4
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-((x1*x3)*(x*x)+x2*x3*x^2))+(x1*x2)*x3*x)-u
by XCMPLX_1:4
.= ((x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2)
-((x^2*x3*x-((x1*x3)*x^2+(x2*x3)*x^2))+(x1*x2)*x3*x)-u
by SQUARE_1:def 3
.= (x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2
-((x3*x^2*x-(x1*x3+x2*x3)*x^2)+(x1*x2*x3)*x)-u by XCMPLX_1:8
.= (x^2*x^2-(x1+x2)*(x^2*x))+x1*x2*x^2
-(x3*x^2*x-(x1*x3+x2*x3)*x^2)-(x1*x2*x3)*x-u by XCMPLX_1:36
.= (x^2*x^2-(x1+x2)*(x^2*x))-(x3*x^2*x-(x1*x3+x2*x3)*x^2)
+x1*x2*x^2-(x1*x2*x3)*x-u by XCMPLX_1:29
.= x^2*x^2-(x1+x2)*(x^2*x)-x3*x^2*x+(x1*x3+x2*x3)*x^2
+x1*x2*x^2-(x1*x2*x3)*x-u by XCMPLX_1:37
.= x^2*x^2-(x1+x2)*(x^2*x)-x3*(x^2*x)+(x1*x3+x2*x3)*x^2
+x1*x2*x^2-(x1*x2*x3)*x-u by XCMPLX_1:4
.= x^2*x^2-((x1+x2)*(x^2*x)+x3*(x^2*x))+(x1*x3+x2*x3)*x^2
+x1*x2*x^2-(x1*x2*x3)*x-u by XCMPLX_1:36
.= x^2*x^2-(x1+x2+x3)*(x^2*x)+(x1*x3+x2*x3)*x^2
+x1*x2*x^2-(x1*x2*x3)*x-u by XCMPLX_1:8
.= x^2*x^2-(x1+x2+x3)*(x^2*x)+((x1*x3+x2*x3)*x^2
+(x1*x2)*x^2)-(x1*x2*x3)*x-u by XCMPLX_1:1
.= x^2*x^2-(x1+x2+x3)*(x^2*x)+(x1*x3+x2*x3
+x1*x2)*x^2-(x1*x2*x3)*x-u by XCMPLX_1:8;
hence thesis by XCMPLX_0:def 9;
end;
theorem Th11:
for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being real number st a1 <> 0 holds
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x)) implies
(a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1 = x|^ 4-(x1+x2+x3+x4)*x|^ 3
+((x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4)*x^2
-(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4)*x+(x1*x2*x3*x4)
proof
let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being real number;
assume
A1: a1 <> 0;
assume for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x);
then A2: (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;
set w = a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5;
set v = x^2*x^2-(x1+x2+x3)*(x^2*x)+(x1*x3+x2*x3+x1*x2)*x^2;
w/a1 = (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+x^2*(x3*x4)-(x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
proof
set X = (x1*x2*x3)*x;
w/a1 = v-X-((x-x1)*(x-x2)*((x-x3)*x4)) by A2,XCMPLX_1:4
.= v-X-(((x-x1)*(x-x2))*(x*x4-x3*x4)) by XCMPLX_1:40
.= v-X-((x*x-x*x2-x1*x+x1*x2)*(x*x4-x3*x4)) by XCMPLX_1:47
.= v-X-((x^2-x*x2-x1*x+x1*x2)*(x*x4-x3*x4)) by SQUARE_1:def 3
.= v-X-(((x^2-x*x2-x1*x)+x1*x2)*(x*x4)
-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:40
.= v-X-(((x^2-x*x2-x1*x)*(x*x4)+x1*x2*(x*x4))
-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:8
.= v-X-(((x^2*(x*x4)-x*x2*(x*x4)-x1*x*(x*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:42
.= v-X-((((x^2*x)*x4-x*x2*(x*x4)-x1*x*(x*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-(x*(x*x2)*x4)-x1*x*(x*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-((x*x)*x2*x4)-x1*x*(x*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-(x^2*x2*x4)-(x1*x*(x*x4)))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4))
by SQUARE_1:def 3
.= v-X-((((x^2*x)*x4-(x^2*x2*x4)-(x1*(x*(x*x4))))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-(x^2*x2*x4)-(x1*((x*x)*x4)))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-(x^2*x2*x4)-(x1*(x^2*x4)))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4))
by SQUARE_1:def 3
.= v-X-((((x^2*x)*x4-(x^2*x2*x4)-(x^2*x1*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-((x^2*x2*x4)+(x^2*x1*x4)))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:36
.= v-X-((((x^2*x)*x4-((x^2*(x2*x4))
+(x^2*x1*x4)))+x1*x2*(x*x4))-(x^2-x*x2
-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-((x^2*(x2*x4))
+(x^2*(x1*x4))))+x1*x2*(x*x4))
-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:4
.= v-X-((((x^2*x)*x4-x^2*(x2*x4+x1*x4))
+x1*x2*(x*x4))-(x^2-x*x2-x1*x+x1*x2)*(x3*x4)) by XCMPLX_1:8
.= v-X-(((x^2*x)*x4-x^2*(x2*x4+x1*x4))
+x1*x2*(x*x4))+(x^2-x*x2-x1*x+x1*x2)*(x3*x4) by XCMPLX_1:37
.= v-X-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*(x4*x))+(x^2-x*x2-x1*x+x1*x2)*(x3*x4) by XCMPLX_1:36
.= v-X-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*x4)*x+((x^2-x*x2-x1*x)+x1*x2)*(x3*x4) by XCMPLX_1:4
.= v-X-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*x4)*x+((x^2-x*x2-x1*x)*(x3*x4)+x1*x2*(x3*x4))
by XCMPLX_1:8
.= v-X-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*x4)*x+(x^2-x*x2-x1*x)*(x3*x4)+x1*x2*(x3*x4)
by XCMPLX_1:1
.= v-X-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*x4)*x+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))
+(x1*x2*(x3*x4)) by XCMPLX_1:42
.= (v-(x1*x2*x3)*x)-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
-(x1*x2*x4)*x+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))
+(x1*x2*x3*x4) by XCMPLX_1:4
.= (v-(x1*x2*x3)*x-(x1*x2*x4)*x)
-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))+(x1*x2*x3*x4)
by XCMPLX_1:21
.= (v-((x1*x2*x3)*x+(x1*x2*x4)*x))
-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))+(x1*x2*x3*x4)
by XCMPLX_1:36
.= v-(x1*x2*x3+x1*x2*x4)*x-((x^2*x)*x4-x^2*(x2*x4+x1*x4))
+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))+(x1*x2*x3*x4)
by XCMPLX_1:8
.=(v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-x*x2*(x3*x4)-x1*x*(x3*x4))+(x1*x2*x3*x4)
by XCMPLX_1:21
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-(x*x2*(x3*x4)+x1*x*(x3*x4)))+(x1*x2*x3*x4)
by XCMPLX_1:36
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-(x*(x2*(x3*x4))+x1*x*(x3*x4)))+(x1*x2*x3*x4)
by XCMPLX_1:4
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-((x2*x3*x4)*x+x1*x*(x3*x4)))+(x1*x2*x3*x4)
by XCMPLX_1:4
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-((x2*x3*x4)*x+((x1*(x3*x4))*x)))+(x1*x2*x3*x4)
by XCMPLX_1:4
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-((x2*x3*x4)*x+(x1*x3*x4)*x))+(x1*x2*x3*x4)
by XCMPLX_1:4
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+(x^2*(x3*x4)-(x2*x3*x4+(x1*x3*x4))*x)+(x1*x2*x3*x4)
by XCMPLX_1:8;
hence thesis by XCMPLX_1:29;
end;
then A3: w/a1 = (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
+-(-(x^2*(x3*x4)))-(x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(x1*x2*x3+x1*x2*x4)*x
-(-x^2*(x3*x4))-(x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_0:def 8
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(-x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4)*x-(x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:21
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(-x^2*(x3*x4))
-((x1*x2*x3+x1*x2*x4)*x+(x2*x3*x4+x1*x3*x4)*x)+(x1*x2*x3*x4)
by XCMPLX_1:36
.= (v-((x^2*x)*x4-x^2*(x2*x4+x1*x4)))-(-x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4+(x2*x3*x4+x1*x3*x4))*x+(x1*x2*x3*x4)
by XCMPLX_1:8
.= v-((x^2*x)*x4-x^2*(x2*x4+x1*x4))-(-x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:1
.= v-(x^2*x)*x4+x^2*(x2*x4+x1*x4)-(-x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:37
.= v-(x^2*x)*x4+x^2*(x2*x4+x1*x4)+-(-x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_0:def 8
.= v-(x^2*x)*x4+(x^2*(x2*x4+x1*x4)+x^2*(x3*x4))
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:1
.= (x^2*x^2-(x1+x2+x3)*(x^2*x))+(x1*x3+x2*x3+x1*x2)*x^2
-x4*(x^2*x)+(x2*x4+x1*x4+x3*x4)*x^2
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:8
.= x^2*x^2-(x1+x2+x3)*(x^2*x)-x4*(x^2*x)
+(x1*x3+x2*x3+x1*x2)*x^2+(x2*x4+x1*x4+x3*x4)*x^2
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:29
.= x^2*x^2-((x1+x2+x3)*(x^2*x)+x4*(x^2*x))
+(x1*x3+x2*x3+x1*x2)*x^2+(x2*x4+x1*x4+x3*x4)*x^2
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:36
.= x^2*x^2-((x1+x2+x3)*(x^2*x)+x4*(x^2*x))
+((x1*x3+x2*x3+x1*x2)*x^2+(x2*x4+x1*x4+x3*x4)*x^2)
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:1
.= x^2*x^2-((x1+x2+x3)*(x^2*x)+x4*(x^2*x))
+(x1*x3+x2*x3+x1*x2+(x2*x4+x1*x4+x3*x4))*x^2
-(x1*x2*x3+x1*x2*x4+x2*x3*x4+x1*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_1:8
.= 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+x2*x3*x4+-(-x1*x3*x4))*x+(x1*x2*x3*x4)
by XCMPLX_1:8
.= 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+x2*x3*x4-(-x1*x3*x4))*x+(x1*x2*x3*x4)
by XCMPLX_0:def 8
.= 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)
by XCMPLX_1:155;
set p = (x1*x3+x2*x3+x1*x2+(x2*x4+x1*x4+x3*x4));
p = (((x1*x2+x1*x3)+x2*x3)+(x2*x4+-(-x1*x4)+x3*x4))
by XCMPLX_1:1
.= (((x1*x2+x1*x3)+x2*x3)+(x2*x4-(-x1*x4)+x3*x4)) by XCMPLX_0:def 8
.= (((x1*x2+x1*x3)+x2*x3)+(x2*x4-((-x1*x4)-x3*x4))) by XCMPLX_1:37
.= (((x1*x2+x1*x3)+x2*x3)+(x2*x4+(x3*x4-(-x1*x4)))) by XCMPLX_1:38
.= (((x1*x2+x1*x3)+x2*x3)+(x2*x4+x3*x4-(-x1*x4))) by XCMPLX_1:29
.= (((x1*x2+x1*x3)+x2*x3)+(-(-x1*x4)+x2*x4+x3*x4)) by XCMPLX_1:155
.= ((x1*x2+x1*x3)+(x2*x3+(x1*x4+x2*x4+x3*x4))) by XCMPLX_1:1
.= ((x1*x2+x1*x3)+(x2*x3+(x1*x4+(x2*x4+x3*x4)))) by XCMPLX_1:1
.= ((x1*x2+x1*x3)+((x2*x3+x1*x4)+(x2*x4+x3*x4))) by XCMPLX_1:1
.= ((x1*x2+x1*x3)+((x2*x3+-(-x1*x4)+x2*x4)+x3*x4)) by XCMPLX_1:1
.= ((x1*x2+x1*x3)+((x2*x3-(-x1*x4)+x2*x4)+x3*x4)) by XCMPLX_0:def 8
.= ((x1*x2+x1*x3)+((x2*x3-((-x1*x4)-x2*x4))+x3*x4)) by XCMPLX_1:37
.= ((x1*x2+x1*x3)+((x2*x3+(x2*x4-(-x1*x4)))+x3*x4)) by XCMPLX_1:38
.= ((x1*x2+x1*x3)+((x2*x3+x2*x4-(-x1*x4))+x3*x4)) by XCMPLX_1:29
.= ((x1*x2+x1*x3)+((-(-x1*x4)+x2*x3+x2*x4)+x3*x4)) by XCMPLX_1:155
.= (x1*x2+x1*x3)+(x1*x4+x2*x3+x2*x4)+x3*x4 by XCMPLX_1:1
.= (x1*x2+x1*x3)+(x1*x4+(x2*x3+x2*x4))+x3*x4 by XCMPLX_1:1;
then w/a1 = x^2*x^2-(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 A3,XCMPLX_1:1
.= 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 number st a1 <> 0 &
(for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x)) holds
a2/a1 = -(x1+x2+x3+x4)
& a3/a1 = (x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4
& a4/a1 = -(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4)
& a5/a1 = x1*x2*x3*x4
proof
let a1,a2,a3,a4,a5,x1,x2,x3,x4 be real number;
assume
A1: a1 <> 0;
set b1 = 1;
set b2 = -(x1+x2+x3+x4);
set b3 = (x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4;
set b4 = -(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4);
set b5 = x1*x2*x3*x4;
assume
A2: for x being real number holds
Four(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x);
now let x be real number;
(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 (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 XCMPLX_0:def 8;
then (a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1
= 1*(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 XCMPLX_1:175;
then (a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1
= b1*(x|^ 4)+b2*x|^ 3+b3*x^2
+-(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4)*x+(x1*x2*x3*x4)
by XCMPLX_0:def 8;
then A3: (a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1
= b1*(x|^ 4)+b2*x|^ 3+b3*x^2+b4*x+b5 by XCMPLX_1:175;
set t= b1*(x|^ 4)+b2*x|^ 3+b3*x^2+b4*x+b5;
t = a1"*(a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)
by A3,XCMPLX_0:def 9
.= a1"*((a1*(x|^ 4)+a2*(x|^ 3))+(a3*x^2+a4*x)+a5) by XCMPLX_1:1
.= a1"*((a1*(x|^ 4)+a2*(x|^ 3))+((a3*x^2+a4*x)+a5)) by XCMPLX_1:1
.= a1"*(a1*(x|^ 4)+a2*(x|^ 3))+a1"*((a3*x^2+a4*x)+a5) by XCMPLX_1:8
.= a1"*(a1*(x|^ 4))+a1"*(a2*(x|^ 3))+a1"*((a3*x^2+a4*x)+a5)
by XCMPLX_1:8
.= a1"*(a1*(x|^ 4))+a1"*(a2*(x|^ 3))+(a1"*(a3*x^2+a4*x)+a1"*a5)
by XCMPLX_1:8
.= a1"*(a1*(x|^ 4))+a1"*(a2*(x|^ 3))
+(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5) by XCMPLX_1:8
.= (a1"*a1)*(x|^ 4)+a1"*(a2*(x|^ 3))
+(a1"*(a3*x^2)+a1"*(a4*x)+a1"*a5) by XCMPLX_1:4
.= (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) by XCMPLX_1:4
.= (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)
+((a1"*a3)*x^2+a1"*(a4*x)+a1"*a5) by XCMPLX_1:4
.= (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+(a1"*a4)*x+a1"*a5) by XCMPLX_1:4
.= (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
.= (x|^ 4)+(a2/a1)*(x|^ 3)
+((a3/a1)*x^2+(a4/a1)*x)+(a5/a1) by XCMPLX_1:1
.= 1*(x|^ 4)+(a2/a1)*(x|^ 3)
+(a3/a1)*x^2+(a4/a1)*x+(a5/a1) by XCMPLX_1:1
.= Four(1,a2/a1,a3/a1,a4/a1,a5/a1,x) by Def1;
hence Four(1,a2/a1,a3/a1,a4/a1,a5/a1,x) = Four(b1,b2,b3,b4,b5,x)
by Def1;
end;
hence thesis by Th9;
end;
theorem
for a,k,y being real number st a <> 0 holds
(for x being real number holds x|^ 4+a|^ 4 = k*a*x*(x^2+a^2)) implies
y|^ 4 -k*(y|^ 3)-k*y+1 = 0
proof
let a,k,y be real number;
assume that
A1: a <> 0 and
A2: for x being real number 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*(a*y))*((a*y)^2+a^2) by XCMPLX_1:4
.= k*((a*a)*y)*((a*y)^2+a^2) by XCMPLX_1:4
.= k*(a^2*y)*((a*y)^2+a^2) by SQUARE_1:def 3
.= k*(a^2*y)*(a^2*y^2+a^2*1) by SQUARE_1:68;
then A3: (a*y)|^ 4+a|^ 4 = k*(a^2*y)*(a^2*(y^2+1)) by XCMPLX_1:8;
A4: a|^ 4 <> 0 by A1,PREPOWER:12;
(a*y)|^ 4+a|^ 4 = k*((a^2*y)*(a^2*(y^2+1))) by A3,XCMPLX_1:4
.= k*((a^2*y)*a^2*(y^2+1)) by XCMPLX_1:4
.= k*(((a^2*a^2)*y)*(y^2+1)) by XCMPLX_1:4
.= (k*(((a|^ 4)*y)*(y^2+1))) by Th4
.= ((k*((a|^ 4)*y))*(y^2+1)) by XCMPLX_1:4
.= (((a|^ 4)*(k*y))*(y^2+1)) by XCMPLX_1:4;
then (a*y)|^ 4+a|^ 4 = (a|^ 4)*((k*y)*(y^2+1)) by XCMPLX_1:4;
then (a|^ 4)*(y|^ 4)+(a|^ 4)*1 = (a|^ 4)*((k*y)*(y^2+1)) by NEWTON:12;
then (a|^ 4)*((y|^ 4)+1)-(a|^ 4)*((k*y)*(y^2+1))
=(a|^ 4)*((k*y)*(y^2+1))-(a|^ 4)*((k*y)*(y^2+1)) by XCMPLX_1:8
.= 0 by XCMPLX_1:14;
then (a|^ 4)*((y|^ 4)+1-(k*y)*(y^2+1)) = 0 by XCMPLX_1:40;
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 by XCMPLX_1:4;
then (((1/(a|^ 4))*(a|^ 4))*((y|^ 4)+1-(k*y)*(y^2+1))) = 0
by XCMPLX_1:217;
then 1*((y|^4)+1-(k*y)*(y^2+1)) = 0 by A4,XCMPLX_1:107;
then ((y|^4)-((k*y)*(y^2+1))+1) = 0 by XCMPLX_1:29;
then ((y|^4)-((k*y)*y^2+(k*y)*1)+1) = 0 by XCMPLX_1:8;
then ((y|^4)-(k*(y*y^2)+k*y)+1) = 0 by XCMPLX_1:4;
then (y|^4)-k*(y^2*y)-k*y+1 = 0 by XCMPLX_1:36;
hence thesis by Th4;
end;