:: Solving the Roots of the Special Polynomial Equation with Real
:: Coefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004-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, REAL_1, SUBSET_1, ARYTM_3, CARD_1, XXREAL_0, FUNCT_3,
ARYTM_1, SQUARE_1, RELAT_1, NEWTON, POWER, POLYEQ_1, XCMPLX_0, XREAL_0,
ABIAN, NAT_1;
notations SUBSET_1, ORDINAL1, NUMBERS, REAL_1, SQUARE_1, POWER, POLYEQ_1,
QUIN_1, POLYEQ_2, NEWTON, XCMPLX_0, XXREAL_0, XREAL_0, ABIAN;
constructors REAL_1, SQUARE_1, NAT_1, QUIN_1, NEWTON, PREPOWER, POWER,
POLYEQ_1, POLYEQ_2, ABIAN;
registrations XCMPLX_0, XREAL_0, SQUARE_1, NAT_1, QUIN_1, NEWTON, ORDINAL1,
POWER, INT_1;
requirements SUBSET, NUMERALS, REAL, ARITHM;
equalities SQUARE_1;
theorems SQUARE_1, PREPOWER, QUIN_1, POLYEQ_1, POWER, NEWTON, POLYEQ_2,
XCMPLX_1, XCMPLX_0, XREAL_1, ABIAN;
begin
reserve x,y,a,b,c,p,q for Real;
reserve m,n for Element of NAT;
theorem Th1:
b/a<0 & c/a>0 & delta(a,b,c) >=0 implies (-b+sqrt delta(a,b,c))/(
2*a)>0 & (-b-sqrt delta(a,b,c))/(2*a)>0
proof
assume that
A1: b/a < 0 and
A2: c/a>0 and
A3: delta(a,b,c) >=0;
A4: b^2-4*a*c >= 0 by A3,QUIN_1:def 1;
now
per cases by A1,XREAL_1:143;
case
A5: b<0 & a>0;
A6: 0 <= sqrt( b^2-4*a*c) by A4,SQUARE_1:17,26;
A7: 2*a>0 by A5,XREAL_1:129;
-b>0 by A5,XREAL_1:58;
then -b+sqrt(b^2-4*a*c)>0 +0 by A6;
then
A8: (-b+sqrt(b^2-4*a*c))/(2*a)>0 by A7,XREAL_1:139;
c>0 & 4*a>0 by A2,A5,XREAL_1:129;
then --4*a*c>0 by XREAL_1:129;
then -4*a*c<0;
then b^2+(-4*a*c)<b^2+0 by XREAL_1:8;
then sqrt(b^2-4*a*c)<sqrt(b^2) by A4,SQUARE_1:27;
then sqrt(b^2-4*a*c)<-b by A5,SQUARE_1:23;
then -sqrt(b^2-4*a*c)>-(-b) by XREAL_1:24;
then -sqrt(b^2-4*a*c)+(-b)>-(-b)+(-b) by XREAL_1:8;
then (-b-sqrt(b^2-4*a*c))/(2*a)>0 by A7,XREAL_1:139;
hence thesis by A8,QUIN_1:def 1;
end;
case
A9: b>0 & a<0;
then
A10: a*2<0*2 by XREAL_1:68;
c<0 by A2,A9;
then a*c>0 by A9,XREAL_1:130;
then 4*(a*c)>0 by XREAL_1:129;
then --4*a*c>0;
then -4*a*c<0;
then b^2+(-4*a*c)<b^2+0 by XREAL_1:8;
then sqrt(b^2-4*a*c)<sqrt(b^2) by A4,SQUARE_1:27;
then sqrt(b^2-4*a*c)< b by A9,SQUARE_1:22;
then -b+sqrt(b^2-4*a*c)<0+b+-b by XREAL_1:8;
then
A11: (-b+sqrt(b^2-4*a*c))/(2*a)>0 by A10,XREAL_1:140;
A12: 0 <= sqrt( b^2-4*a*c) by A4,SQUARE_1:17,26;
--b>0 by A9;
then -b+0<0+sqrt( b^2-4*a*c) by A12;
then --(sqrt( b^2-4*a*c)+b)>0 by XREAL_1:62;
then -b-sqrt( b^2-4*a*c)<0;
then (-b-sqrt( b^2-4*a*c))/(2*a)>0 by A10,XREAL_1:140;
hence thesis by A11,QUIN_1:def 1;
end;
end;
hence thesis;
end;
theorem
b/a>0 & c/a>0 & delta(a,b,c) >=0 implies (-b+sqrt delta(a,b,c))/(2*a)<
0 & (-b-sqrt delta(a,b,c))/(2*a)<0
proof
assume that
A1: b/a>0 and
A2: c/a>0 and
A3: delta(a,b,c) >=0;
A4: b^2-4*a*c >=0 by A3,QUIN_1:def 1;
now
per cases by A1,XREAL_1:144;
case
A5: b>0 & a>0;
then c>0 & 4*a>0 by A2,XREAL_1:129;
then --4*a*c>0 by XREAL_1:129;
then -4*a*c<0;
then b^2+(-4*a*c)<b^2+0 by XREAL_1:8;
then sqrt(b^2-4*a*c)<sqrt(b^2) by A4,SQUARE_1:27;
then sqrt(b^2-4*a*c)<b by A5,SQUARE_1:22;
then -b+sqrt(b^2-4*a*c)<0+(b+-b) by XREAL_1:8;
then
A6: (-b+sqrt(b^2-4*a*c))/(2*a)<0 by A5,XREAL_1:129,141;
0 <= sqrt(b^2-4*a*c) by A4,SQUARE_1:17,26;
then 0+0<b+sqrt( b^2-4*a*c) by A5;
then --(b+sqrt( b^2-4*a*c))>0;
then -b-sqrt( b^2-4*a*c)<0;
then (-b-sqrt( b^2-4*a*c))/(2*a)<0 by A5,XREAL_1:129,141;
hence thesis by A6,QUIN_1:def 1;
end;
case
A7: b<0 & a<0;
A8: 0 <= sqrt( b^2-4*a*c) by A4,SQUARE_1:17,26;
A9: a*2<0*2 by A7,XREAL_1:68;
-b>0 by A7,XREAL_1:58;
then 0+0<-b+sqrt( b^2-4*a*c) by A8;
then
A10: (-b+sqrt( b^2-4*a*c))/(2*a)<0 by A9,XREAL_1:142;
c<0 by A2,A7;
then a*c>0 by A7,XREAL_1:130;
then 4*(a*c)>0 by XREAL_1:129;
then --4*a*c>0;
then -4*a*c<0;
then b^2+(-4*a*c)<b^2+0 by XREAL_1:8;
then sqrt(b^2-4*a*c)<sqrt(b^2) by A4,SQUARE_1:27;
then sqrt(b^2-4*a*c)< -b by A7,SQUARE_1:23;
then b+sqrt(b^2-4*a*c)<0+b+-b by XREAL_1:8;
then -(b+sqrt(b^2-4*a*c))>0 by XREAL_1:58;
then (-b-sqrt(b^2-4*a*c))/(2*a)<0 by A9,XREAL_1:142;
hence thesis by A10,QUIN_1:def 1;
end;
end;
hence thesis;
end;
theorem
c/a<0 implies (-b+sqrt delta(a,b,c))/(2*a)>0 & (-b-sqrt delta(a,b,c))/
(2*a)<0 or (-b+sqrt delta(a,b,c))/(2*a)<0 & (-b-sqrt delta(a,b,c))/(2*a)>0
proof
assume
A1: c/a<0;
now
per cases by A1,XREAL_1:143;
case
A2: c>0 & a<0;
then 4*a<4*0 by XREAL_1:68;
then 4*a*c<0*c by A2,XREAL_1:68;
then
A3: -4*a*c>0 by XREAL_1:58;
then b^2+(-4*a*c)>b^2+0 by XREAL_1:8;
then
A4: sqrt(b^2-4*a*c)>sqrt(b^2) by SQUARE_1:27,XREAL_1:63;
A5: 2*a<2*0 by A2,XREAL_1:68;
-4*a*c+b^2>0+0 by A3,XREAL_1:8,63;
then
A6: --sqrt(b^2-4*a*c)>0 by SQUARE_1:17,27;
then
A7: -sqrt(b^2-4*a*c)<0;
now
per cases;
suppose
A8: b>=0;
then -b<=-0;
then -sqrt(b^2-4*a*c)+-b<0+0 by A7;
then -b-sqrt(b^2-4*a*c)<0;
then
A9: -b-sqrt delta(a,b,c)<0 by QUIN_1:def 1;
sqrt(b^2-4*a*c)>b by A4,A8,SQUARE_1:22;
then -b+sqrt(b^2-4*a*c)>0+b+-b by XREAL_1:8;
then (-b+sqrt(b^2-4*a*c))/(2*a)<0 by A5,XREAL_1:142;
hence thesis by A5,A9,QUIN_1:def 1,XREAL_1:140;
end;
suppose
A10: b<0;
then sqrt(b^2-4*a*c)>-b by A4,SQUARE_1:23;
then --(b+sqrt(b^2-4*a*c))>0 by XREAL_1:62;
then -b-sqrt(b^2-4*a*c)<0;
then
A11: (-b-sqrt(b^2-4*a*c))/(2*a)>0 by A5,XREAL_1:140;
-b>0 by A10,XREAL_1:58;
then sqrt(b^2-4*a*c)+(-b)>0+0 by A6;
then sqrt delta(a,b,c)+(-b)>0+0 by QUIN_1:def 1;
hence thesis by A5,A11,QUIN_1:def 1,XREAL_1:142;
end;
end;
hence thesis;
end;
case
A12: c<0 & a>0;
then 4*a>0 by XREAL_1:129;
then 4*a*c<4*a*0 by A12,XREAL_1:68;
then
A13: -4*a*c>0 by XREAL_1:58;
then b^2+(-4*a*c)>b^2+0 by XREAL_1:8;
then
A14: sqrt(b^2-4*a*c)>sqrt(b^2) by SQUARE_1:27,XREAL_1:63;
A15: 2*a>0 by A12,XREAL_1:129;
-4*a*c+b^2>0+0 by A13,XREAL_1:8,63;
then
A16: --sqrt(b^2-4*a*c)>0 by SQUARE_1:17,27;
then
A17: -sqrt(b^2-4*a*c)<0;
now
per cases;
suppose
A18: b>=0;
then -b<=-0;
then -sqrt(b^2-4*a*c)+-b<0+0 by A17;
then -b-sqrt(b^2-4*a*c)<0;
then
A19: -b-sqrt delta(a,b,c)<0 by QUIN_1:def 1;
sqrt(b^2-4*a*c)>b by A14,A18,SQUARE_1:22;
then -b+sqrt(b^2-4*a*c)>0+b+-b by XREAL_1:8;
then (-b+sqrt(b^2-4*a*c))/(2*a)>0 by A15,XREAL_1:139;
hence thesis by A12,A19,QUIN_1:def 1,XREAL_1:129,141;
end;
suppose
A20: b<0;
then sqrt(b^2-4*a*c)>-b by A14,SQUARE_1:23;
then --(b+sqrt(b^2-4*a*c))>0 by XREAL_1:62;
then -b-sqrt(b^2-4*a*c)<0;
then
A21: (-b-sqrt(b^2-4*a*c))/(2*a)<0 by A12,XREAL_1:129,141;
-b>0 by A20,XREAL_1:58;
then sqrt(b^2-4*a*c)+(-b)>0+0 by A16;
then sqrt delta(a,b,c)+(-b)>0 by QUIN_1:def 1;
hence thesis by A15,A21,QUIN_1:def 1,XREAL_1:139;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th4:
a>0 & n is even & n >= 1 & x |^ n = a implies x = n-root a or x = -n-root a
proof
assume that
A1: a>0 and
A2: n is even and
A3: n >= 1;
assume
A4: x |^ n=a;
then A5: x<>0 by A1,A3,NEWTON:11;
now
per cases by A5;
case x>0;
hence thesis by A4,A3,POWER:4;
end;
case x<0;
then
A6: -x>0 by XREAL_1:58;
n-root a=n-root((-x)|^ n) by A2,A4,POWER:1;
then (-1)*n-root a=(-1)*(-x) by A3,A6,POWER:4;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th5:
a <> 0 & Polynom(a,b,0,x) = 0 implies x=0 or x = -(b/a)
proof
assume that
A1: a<>0 and
A2: Polynom(a,b,0,x) = 0;
a*x^2+b*x+0=0 by A2,POLYEQ_1:def 2;
then (a*x+b+0)*x=0;
then a*x+b+-b=0+-b or x=0 by XCMPLX_1:6;
then x=(-b)/a or x=0 by A1,XCMPLX_1:89;
hence thesis by XCMPLX_1:187;
end;
theorem
a <> 0 & Polynom(a,0,0,x) = 0 implies x=0
proof
assume that
A1: a<>0 and
A2: Polynom(a,0,0,x) = 0;
a*x^2+0*x+0=0 by A2,POLYEQ_1:def 2;
then x^2=0 by A1;
hence thesis;
end;
theorem
a <> 0 & n is odd & delta(a,b,c) >= 0 & Polynom(a,b,c,x|^ n)
= 0 implies x = n-root((-b+sqrt delta(a,b,c))/(2*a)) or x = n-root((-b-sqrt
delta(a,b,c))/(2*a))
proof
assume that
A1: a <>0 and
A2: n is odd and
A3: delta(a,b,c)>=0 & Polynom(a,b,c,x|^ n)=0;
x|^ n = (-b+sqrt delta(a,b,c))/(2*a) or x|^ n = (-b-sqrt delta(a,b,c))/(
2*a) by A1,A3,POLYEQ_1:5;
hence thesis by A2,POWER:4;
end;
theorem
a <> 0 & b/a<0 & c/a>0 & n is even & n >= 1 & delta(a,b,c) >= 0 &
Polynom(a,b,c,x|^ n) = 0 implies
x = n-root((-b+sqrt delta(a,b,c))/(2*a)) or
x = -n-root((-b+sqrt delta(a,b,c))/(2*a)) or
x = n-root((-b-sqrt delta(a,b,c))/(2*a)) or
x = -n-root((-b-sqrt delta(a,b,c))/(2*a))
proof
assume that
A1: a <>0 and
A2: b/a<0 & c/a>0 & n is even & n >= 1 and
A3: delta(a,b,c)>=0 and
A4: Polynom(a,b,c,x|^ n)=0;
:: theorem Th4:
:: a>0 & n is even & n >= 1 & x |^ n = a implies x = n-root a or x = -n-root a
now
per cases by A1,A3,A4,POLYEQ_1:5;
suppose
x|^ n = (-b+sqrt delta(a,b,c))/(2*a);
then x = n-root((-b+sqrt delta(a,b,c))/(2*a)) or
x = -n-root((-b+sqrt delta(a,b,c))/(2*a)) by A2,A3,Th1,Th4;
hence thesis;
end;
suppose
x|^ n = (-b-sqrt delta(a,b,c))/(2*a);
then x = n-root((-b-sqrt delta(a,b,c))/(2*a)) or
x = -n-root((-b-sqrt delta(a,b,c))/(2*a)) by A2,A3,Th1,Th4;
hence thesis;
end;
end;
hence thesis;
end;
theorem
a <> 0 & n is odd & Polynom(a,b,0,x|^ n) = 0 implies x=0 or x = n-root -(b/a)
proof
assume that
A1: a<>0 and
A2: n is odd and
A3: Polynom(a,b,0,x|^ n) = 0;
now
per cases by A1,A3,Th5;
suppose
x|^ n = 0;
hence thesis by PREPOWER:5;
end;
suppose
x|^ n = -(b/a);
hence thesis by A2,POWER:4;
end;
end;
hence thesis;
end;
theorem
a <> 0 & b/a<0 & n is even & n >= 1 & Polynom(a,b,0,x|^ n) = 0
implies x=0 or x = n-root -(b/a) or x = -n-root -(b/a)
proof
assume that
A1: a<>0 and
A2: b/a<0 and
A3: n is even & n >= 1 and
A4: Polynom(a,b,0,x|^ n) = 0;
A5: -(b/a)>0 by A2,XREAL_1:58;
now
per cases by A1,A4,Th5;
suppose
x|^ n = 0;
hence thesis by PREPOWER:5;
end;
suppose
x|^ n = -(b/a);
hence thesis by A3,A5,Th4;
end;
end;
hence thesis;
end;
theorem Th11:
a|^3+b|^3 = (a+b)*(a^2-a*b+b^2) & a|^5+b|^5 = (a+b)*(a|^4-a|^3*b
+a|^2*b|^2-a*b|^3+b|^4)
proof
A1: (a+b)*(a|^4-a|^3*b+a|^2*b|^2-a*b|^3+b|^4) =a|^4*a+b*a|^4+0*a|^4-(a|^3*b)
*(a+b)+(a|^2*b|^2)*(a+b) -(a*b|^3)*(a+b)+b|^4*(a+b)
.=a|^4*a|^1+b*a|^4+0*a|^4-(a|^3*b)*(a+b)+(a|^2*b|^2)*(a+b) -(a*b|^3)*(a+
b)+b|^4*(a+b)
.=a|^(4+1)+b*a|^4-(a|^3*b)*(a+b+0)+(a|^2*b|^2)*(a+b) -(a*b|^3)*(a+b)+b|^
4*(a+b) by NEWTON:8
.=(a|^5+b*a|^4)-(a*a|^3*b+b*(a|^3*b))+(a*(a|^2*b|^2) +b*(a|^2*b|^2))-(a*
(a*b|^3)+b*(a*b|^3))+(a*b|^4+b*b|^4)
.=(a|^5+b*a|^4)-(a|^4*b+b*b*a|^3)+((a|^2*a)*b|^2 +b*b|^2*a|^2)-(a*a*b|^3
+b*b|^3*a)+(a*b|^4+b*b|^4) by POLYEQ_2:4
.=(a|^5+b*a|^4)-(a|^4*b+b*b*a|^3)+(a|^2*a*b|^2 +b*b|^2*a|^2)-(a*a*b|^3+b
|^4*a)+(a*b|^4+b*b|^4) by POLYEQ_2:4
.=(a|^5+b*a|^4)-(a|^4*b+b*b*a|^3)+(a|^(2+1)*b|^2 +b|^2*b*a|^2)-(a*a*b|^3
+b|^4*a)+(a*b|^4+b*b|^4) by NEWTON:6
.=(a|^5+b*a|^4)-(a|^4*b+b*b*a|^3)+(a|^3*b|^2 +b|^(2+1)*a|^2)-(a*a*b|^3+b
|^4*a)+(a*b|^4+b|^4*b) by NEWTON:6
.=(a|^5+b*a|^4)-(a|^4*b+b*b*a|^3)+(a|^3*b|^2 +b|^3*a|^2)-(a*a*b|^3+b|^4*
a)+(a*b|^4+b|^(4+1)) by NEWTON:6
.=(a|^5+b*a|^4)-(a|^4*b+b|^1*b*a|^3)+(a|^3*b|^2 +b|^3*a|^2)-(a*a*b|^3+b
|^4*a)+(a*b|^4+b|^(4+1))
.=(a|^5+b*a|^4)-(a|^4*b+b|^1*b*a|^3)+(a|^3*b|^2 +b|^3*a|^2)-(a|^1*a*b|^3
+b|^4*a)+(a*b|^4+b|^(4+1))
.=(a|^5+b*a|^4)-(a|^4*b+b|^(1+1)*a|^3)+(a|^3*b|^2 +b|^3*a|^2)-(a|^1*a*b
|^3+b|^4*a)+(a*b|^4+b|^5) by NEWTON:6
.=(a|^5+a|^2*b|^3)-(a|^2*b|^3+a*b|^4)+(a*b|^4+b|^5) by NEWTON:6
.=a|^5+b|^5;
(a^2-a*b+b^2)*(a+b) =a^2*a+b*a^2-(a*(a*b)+b*(a*b))+(a*b^2+b*b^2+0*b^2)
.=a|^ 3+b*a^2-(a*(a*b)+b*(a*b))+(a*b^2+b*b^2) by POLYEQ_2:4
.=a|^ 3+b*a^2-(a^2*b+b*b*a)+(a*b^2+b|^ 3) by POLYEQ_2:4
.=a|^3+b|^3;
hence thesis by A1;
end;
theorem
a<>0 & b^2-2*a*b-3*a^2>=0 & Polynom(a,b,b,a,x)=0 implies x=-1 or x= (a
-b+sqrt(b^2-2*a*b-3*a^2))/(2*a) or x= (a-b-sqrt(b^2-2*a*b-3*a^2))/(2*a)
proof
assume that
A1: a<>0 & b^2-2*a*b-3*a^2>=0 and
A2: Polynom(a,b,b,a,x)=0;
a*(x|^ 3)+b*x^2+b*x+a=0 by A2,POLYEQ_1:def 4;
then ((x|^ 3)+1)*a+(x^2+x+0)*b=0;
then ((x|^ 3)+1 to_power 3)*a+(x+1)*x*b=0;
then ((x+1)*(x^2-x*1+1^2))*a+(x+1)*x*b=0 by Th11;
then
A3: (x^2*a-x*a+x*b+a)*(x+1)=0;
now
per cases by A3;
case
x+1=0;
hence thesis;
end;
case
A4: a*x^2-(a-b)*x+a=0;
A5: delta(a,-a+b,a) =(-a+b)^2-4*a*a by QUIN_1:def 1
.=(b^2-2*a*b)+(-(4-1))*a^2;
a*x^2+(-a+b)*x+a=0 by A4;
then Polynom(a,-a+b,a,x)=0 by POLYEQ_1:def 2;
then
x= (-(-a+b)+sqrt delta(a,-a+b,a))/(2*a) or x= (-(-a+b)-sqrt delta(a
,-a+b,a))/(2*a) by A1,A5,POLYEQ_1:5;
hence thesis by A5;
end;
end;
hence thesis;
end;
definition
let a,b,c,d,e,f,x be Complex;
func Polynom(a,b,c,d,e,f,x) -> set equals
a*(x|^5)+b*(x|^4)+c*(x|^3)+d*(x^2)+e*x+f;
coherence;
end;
registration
let a,b,c,d,e,f,x be Complex;
cluster Polynom(a,b,c,d,e,f,x) -> complex;
coherence;
end;
registration
let a,b,c,d,e,f,x be Real;
cluster Polynom(a,b,c,d,e,f,x) -> real;
coherence;
end;
theorem
a<>0 & b^2+2*a*b+5*a^2-4*a*c>0 & Polynom(a,b,c,c,b,a,x)=0 implies for
y1,y2 being Real st y1 = (a-b+sqrt(b^2+2*a*b+5*a^2-4*a*c))/(2*a) & y2 = (a-b-
sqrt(b^2+2*a*b+5*a^2-4*a*c))/(2*a) holds x=-1 or 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
assume that
A1: a<>0 & b^2+2*a*b+5*a^2-4*a*c>0 and
A2: Polynom(a,b,c,c,b,a,x)=0;
let y1,y2 be Real;
assume that
A3: y1 = (a-b+sqrt(b^2+2*a*b+5*a^2-4*a*c))/(2*a) and
A4: y2 = (a-b-sqrt(b^2+2*a*b+5*a^2-4*a*c))/(2*a);
A5: 0=(x|^5+1)*a+(x|^4+x+0)*b+(c*(x|^3)+c*(x^2)+0*c) by A2
.=(x|^5+1|^5)*a+(x|^(3+1)+x)*b+(x|^3+x^2)*c
.=(x|^5+1|^5)*a+(x|^3*x+x)*b+(x|^(2+1)+x^2)*c by NEWTON:6
.=(x|^5+1|^5)*a+(x|^3+1+0)*x*b+(x*x|^(1+1)+1*x^2+0*x^2)*c by NEWTON:6
.=(x|^5+1|^5)*a+(x|^3+1+0)*x*b+(x*(x|^1*x)+1*x^2+0*x^2)*c by NEWTON:6
.=(x|^5+1|^5)*a+(x|^3+1+0)*x*b+(x*x^2+1*x^2+0*x^2)*c
.=((x+1)*(x|^4-x|^3*1+x|^2*1|^2-x*1|^3+1|^4))*a +(x|^3+1)*x*b+(x+1+0)*x
^2*c by Th11
.=((x+1)*(x|^4-x|^3+x|^2*1-x*1|^3+1|^4))*a +(x|^3+1)*x*b+(x+1+0)*x^2*c
.=((x+1)*(x|^4-x|^3+x|^2-x*1+1|^4))*a+(x|^3+1)*x*b+(x+1+0)*x^2*c
.=((x+1)*(x|^4-x|^3+x|^2-x+1))*a+(x|^3+1)*x*b+(x+1+0)*x^2*c
.=((x+1)*(x|^4-x|^3+x|^2-x+1))*a+(x|^3+1|^3)*x*b+(x+1)*x^2*c
.=((x+1)*(x|^4-x|^3+x|^2-x+1))*a+((x+1)*(x^2-x*1+1^2))*x*b +(x+1)*x^2*c
by Th11
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x*x*x*b-x*x*b+(b*x)) +(x*x*c))*(x+1)
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^1*x*x*b-x*x*b+(b*x)) +(x*x*c))*(x+1)
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^1*x*x*b-x*x*b+(b*x)) +(x|^1*x*c))*(x+1
)
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^1*x*x*b-x*x*b+(b*x)) +(x|^(1+1)*c))*(x
+1) by NEWTON:6
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^(1+1)*x*b-x*x*b+(b*x)) +(x|^2*c))*(x+1
) by NEWTON:6
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^(2+1)*b-x*x*b+b*x) +(x|^2*c))*(x+1) by
NEWTON:6
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^3*b-x|^1*x*b+b*x) +(x|^2*c))*(x+1)
.=(a*x|^4-a*x|^3+a*x|^2-a*x+a+(x|^3*b-x|^(1+1)*b+b*x) +(x|^2*c))*(x+1)
by NEWTON:6
.=(a*x|^4-(a-b)*x|^3+(a+c-b)*x|^2-(a-b)*x+a)*(x+1);
now
per cases by A5;
case
x+1=0;
hence thesis;
end;
case
A6: a*x|^4-(a-b)*x|^3+(a+c-b)*x|^2-(a-b)*x+a=0;
set y=x+1/x;
0=a*x|^4+(-a+b)*x|^3+(a+c-b)*x|^(1+1)+(-a+b)*x+a by A6
.=a*x|^4+(-a+b)*x|^3+(a+c-b)*(x|^1*x)+(-a+b)*x+a by NEWTON:6
.=a*x|^4+(-a+b)*x|^3+(a+c-b)*x^2+(-a+b)*x+a;
then
A7: Polynom(a,-a+b,a+c-b,-a+b,a,x)=0 by POLYEQ_2:def 1;
y=x+1/x & y1 = (-(-a+b)+sqrt((-a+b)^2-4*a*(a+c-b)+8*a^2))/(2*a) by A3;
hence thesis by A1,A4,A7,POLYEQ_2:3;
end;
end;
hence thesis;
end;
theorem Th14:
x+y=p & x*y=q & p^2-4*q>=0 implies x=(p+sqrt(p^2-4*q))/2 & y=(p-
sqrt(p^2-4*q))/2 or x=(p-sqrt(p^2-4*q))/2 & y=(p+sqrt(p^2-4*q))/2
proof
assume that
A1: x+y=p and
A2: x*y=q and
A3: p^2-4*q>=0;
A4: delta(1,-p,q)=(-p)^2-4*1*q by QUIN_1:def 1
.=p^2-4*q;
1*y^2+(-p)*y+q=0 by A1,A2;
then Polynom(1,-p,q,y)=0 by POLYEQ_1:def 2;
then
A5: y=(-(-p)+sqrt delta(1,-p,q))/(2*1) or y=(-(-p)-sqrt delta(1,-p,q))/(2*1)
by A3,A4,POLYEQ_1:5;
now
per cases by A5;
suppose
A6: y=(p+sqrt delta(1,-p,q))/2;
then x=p*2/2-(p/2+(sqrt delta(1,-p,q))/2) by A1
.=p*2/2-(p/2+(sqrt (p^2-4*q))/2) by A4;
hence thesis by A4,A6;
end;
suppose
A7: y=(p-sqrt delta(1,-p,q))/2;
then x=p-(p-sqrt delta(1,-p,q)+0)/2 by A1
.=p-(p-sqrt (p^2-4*q)+0)/2 by A4;
hence thesis by A4,A7;
end;
end;
hence thesis;
end;
theorem
(x|^ n)+(y|^ n)=p & (x|^ n)*(y|^ n)=q & p^2-4*q>=0 & n is odd
implies x=n-root((p+sqrt(p^2-4*q))/2) & y=n-root((p-sqrt(p^2-4*q))/2) or x=n
-root((p-sqrt(p^2-4*q))/2) & y=n-root((p+sqrt(p^2-4*q))/2)
proof
assume that
A1: (x|^ n)+(y|^ n)=p & (x|^ n)*(y|^ n)=q & p^2-4*q>=0 and
A2: n is odd;
x|^ n=(p+sqrt(p^2-4*q))/2 & y|^ n=(p-sqrt(p^2-4*q))/2 or x|^ n=(p-sqrt(p
^2-4*q))/2 & y|^ n=(p+sqrt(p^2-4*q))/2 by A1,Th14;
hence thesis by A2,POWER:4;
end;
theorem
(x|^ n)+(y|^ n)=p & (x|^ n)*(y|^ n)=q & p^2-4*q>=0 & p>0 & q>0 &
n is even & n >= 1
implies x=n-root((p+sqrt(p^2-4*q))/2)&y=n-root((p-sqrt(p^2-4*q
))/2) or x=-n-root((p+sqrt(p^2-4*q))/2)&y=n-root((p-sqrt(p^2-4*q))/2) or x=n
-root((p+sqrt(p^2-4*q))/2)&y=-n-root((p-sqrt(p^2-4*q))/2) or x=-n-root((p+sqrt(
p^2-4*q))/2)&y=-n-root((p-sqrt(p^2-4*q))/2) or x=n-root((p-sqrt(p^2-4*q))/2)&y=
n-root((p+sqrt(p^2-4*q))/2) or x=-n-root((p-sqrt(p^2-4*q))/2)&y=n-root((p+sqrt(
p^2-4*q))/2) or x=n-root((p-sqrt(p^2-4*q))/2)&y=-n-root((p+sqrt(p^2-4*q))/2) or
x=-n-root((p-sqrt(p^2-4*q))/2)&y=-n-root((p+sqrt(p^2-4*q))/2)
proof
assume
A1: (x|^ n)+(y|^ n)=p & (x|^ n)*(y|^ n)=q;
assume that
A2: p^2-4*q>=0 and
A3: p>0 and
A4: q>0 and
A5: n is even & n >= 1;
--4*q>0 by A4,XREAL_1:129;
then -4*q<0;
then p^2+(-4*q)<p^2+0 by XREAL_1:8;
then sqrt(p^2-4*q)<sqrt(p^2) by A2,SQUARE_1:27;
then sqrt(p^2-4*q)<p by A3,SQUARE_1:22;
then -sqrt(p^2-4*q)>-p by XREAL_1:24;
then -sqrt(p^2-4*q)+p>-p+0+p by XREAL_1:8;
then
A6: (0+p-sqrt(p^2-4*q))/2>0 by XREAL_1:139;
A7: delta(1,(-p),q)=(-p)^2-4*1*q by QUIN_1:def 1
.=p^2-4*q;
then 0 <= sqrt delta(1,(-p),q) by A2,SQUARE_1:17,26;
then -(-p)+sqrt delta(1,-p,q)>0 +0 by A3;
then
A8: (0+p+sqrt(p^2-4*q))/2>0 by A7,XREAL_1:139;
now
per cases by A1,A2,Th14;
suppose
x|^ n=(p+sqrt(p^2-4*q))/2 & y|^ n=(p-sqrt(p^2-4*q))/2;
hence thesis by A5,A8,A6,Th4;
end;
suppose
x|^ n=(p-sqrt(p^2-4*q))/2 & y|^ n=(p+sqrt(p^2-4*q))/2;
hence thesis by A5,A8,A6,Th4;
end;
end;
hence thesis;
end;
theorem
x|^ n+y|^ n=a & x|^ n-y|^ n=b & n is even & n >= 1 & a+b>0 & a-b>0
implies x=n-root((a+b)/2) & y=n-root((a-b)/2) or x=n-root((a+b)/2) & y=-n-root(
(a-b)/2) or x=-n-root((a+b)/2)& y=n-root((a-b)/2) or x=-n-root((a+b)/2) & y=-n
-root((a-b)/2)
proof
assume
A1: x|^ n+y|^ n=a & x|^ n-y|^ n=b;
assume that
A2: n is even & n >= 1 and
A3: a+b>0 & a-b>0;
(a+b)/2>0 & (a-b)/2>0 by A3,XREAL_1:139;
hence thesis by A1,A2,Th4;
end;
theorem
a*x|^ n+b*y|^ n=p & x*y=0 & n is odd & a*b<>0 implies x=0 & y
=n-root(p/b) or x=n-root(p/a) & y=0
proof
assume that
A1: a*x|^ n+b*y|^ n=p and
A2: x*y=0 and
A3: n is odd and
A4: a*b<>0;
consider m being Nat such that
A5: n=2*m+1 by A3,ABIAN:9;
A6: n>0 by A5;
now
per cases by A2;
suppose
A7: x=0;
then a*0 to_power n+b*y|^ n=p by A1;
then a*0 +b*y|^ n=p by A6,POWER:def 2;
then y|^ n=p/b by A4,XCMPLX_1:89;
hence thesis by A3,A7,POWER:4;
end;
suppose
A8: y=0;
then a*x|^ n+b*0 to_power n=p by A1;
then a*x|^ n+b*0=p by A6,POWER:def 2;
then x|^ n=p/a by A4,XCMPLX_1:89;
hence thesis by A3,A8,POWER:4;
end;
end;
hence thesis;
end;
theorem
a*x|^ n+b*y|^ n=p & x*y=0 & n is even & n >= 1 & p/b>0 &p/a>0 &a*b
<>0 implies x=0 & y=n-root(p/b) or x=0 & y=-n-root(p/b) or x=n-root(p/a) & y=0
or x=-n-root(p/a) & y=0
proof
assume that
A1: a*x|^ n+b*y|^ n=p and
A2: x*y=0 and
A3: n is even & n >= 1 and
A4: p/b>0 and
A5: p/a>0 and
A6: a*b<>0;
n>=1 by A3;
then
A7: n>0;
per cases by A2;
suppose
A8: x=0;
then a*0 to_power n+b*y|^ n=p by A1;
then a*0 +b*y|^ n=p by A7,POWER:def 2;
then y|^ n=p/b by A6,XCMPLX_1:89;
hence thesis by A3,A4,A8,Th4;
end;
suppose
A9: y=0;
then a*x|^ n+b*0 to_power n=p by A1;
then a*x|^ n+b*0=p by A7,POWER:def 2;
then x|^ n=p/a by A6,XCMPLX_1:89;
hence thesis by A3,A5,A9,Th4;
end;
end;
theorem
a*x|^ n=p & x*y=q & n is odd & p*a<>0 implies x=n-root(p/a) & y=q*n-root(a/p)
proof
assume that
A1: a*x|^ n=p and
A2: x*y=q and
A3: n is odd and
A4: p*a<>0;
consider m being Nat such that
A5: n=2*m+1 by A3,ABIAN:9;
A6: a<>0 by A4;
then
A7: x|^ n=p/a by A1,XCMPLX_1:89;
then x=n-root(p/a) by A3,POWER:4;
then y*(n-root(p/a)*n-root(a/p))=q*n-root(a/p) by A2;
then y*n-root((p/a)*(a/p))=q*n-root(a/p) by A3,POWER:11;
then y*n-root((p/a)*(a*p"))=q*n-root(a/p) by XCMPLX_0:def 9;
then y*n-root(p/a*a*p")=q*n-root(a/p);
then y*n-root(p*p")=q*n-root(a/p) by A6,XCMPLX_1:87;
then
A8: y*n-root(p/p)=q*n-root(a/p) by XCMPLX_0:def 9;
A9: 2*m+1>=0+1 by XREAL_1:7;
p<>0 by A4;
then y*n-root(1)=q*n-root(a/p) by A8,XCMPLX_1:60;
then y*1=q*n-root(a/p) by A5;
hence thesis by A3,A7,POWER:4;
end;
theorem
a*x|^ n=p & x*y=q & n is even & n >= 1 & p/a>0 &a<>0 implies x=n
-root(p/a) & y=q*n-root(a/p) or x=-n-root(p/a) & y=-q*n-root(a/p)
proof
assume that
A1: a*x|^ n=p and
A2: x*y=q and
A3: n is even & n >= 1 and
A4: p/a>0 and
A5: a<>0;
A6: x|^ n=p/a by A1,A5,XCMPLX_1:89;
(p/a)">0 by A4;
then 1/(p/a)>0 by XCMPLX_1:215;
then
A7: (1*a)/p>0 by XCMPLX_1:77;
A8: p<>0 by A4;
per cases by A3,A4,A6,Th4;
suppose
A9: x=n-root(p/a);
then y*(n-root(p/a)*n-root(a/p))=q*n-root(a/p) by A2;
then y*n-root((p/a)*(a/p))=q*n-root(a/p) by A4,A3,A7,POWER:11;
then y*n-root((p/a)*(a*p"))=q*n-root(a/p) by XCMPLX_0:def 9;
then y*n-root(p/a*a*p")=q*n-root(a/p);
then y*n-root(p*p")=q*n-root(a/p) by A5,XCMPLX_1:87;
then y*n-root(p/p)=q*n-root(a/p) by XCMPLX_0:def 9;
then y*n-root(1)=q*n-root(a/p) by A8,XCMPLX_1:60;
then y*1=q*n-root(a/p) by A3,POWER:6;
hence thesis by A9;
end;
suppose
A10: x=-n-root(p/a);
then y*(n-root(p/a)*n-root(a/p))=-q*n-root(a/p) by A2;
then y*n-root((p/a)*(a/p))=-q*n-root(a/p) by A4,A3,A7,POWER:11;
then y*n-root((p/a)*(a*p"))=-q*n-root(a/p) by XCMPLX_0:def 9;
then y*n-root(p/a*a*p")=-q*n-root(a/p);
then y*n-root(p*p")=-q*n-root(a/p) by A5,XCMPLX_1:87;
then y*n-root(p/p)=-q*n-root(a/p) by XCMPLX_0:def 9;
then y*n-root(1)=-q*n-root(a/p) by A8,XCMPLX_1:60;
then y*1=-q*n-root(a/p) by A3,POWER:6;
hence thesis by A10;
end;
end;
theorem
for a,x being Real st a>0 & a<>1 & a to_power x = 1 holds x=0
proof
let a,x be Real;
assume that
A1: a>0 & a<>1 and
A2: a to_power x = 1;
x=log(a,1) by A1,A2,POWER:def 3;
hence thesis by A1,POWER:51;
end;
theorem
for a,x being Real st a>0 & a<>1 & a to_power x = a holds x=1
proof
let a,x be Real;
assume that
A1: a>0 & a<>1 and
A2: a to_power x = a;
x=log(a,a) by A1,A2,POWER:def 3;
hence thesis by A1,POWER:52;
end;
theorem
for a,b,x being Real st a>0 & a<>1 & x>0 & log(a,x) = 0 holds x = 1
proof
let a,b,x be Real;
assume a>0 & a<>1 & x>0 & log(a,x) = 0;
then a to_power 0 = x by POWER:def 3;
hence thesis by POWER:24;
end;
theorem
for a,b,x being Real st a>0 & a<>1 & x>0 & log(a,x) = 1 holds x = a
proof
let a,b,x be Real;
assume a>0 & a<>1 & x>0 & log(a,x) = 1;
then a to_power 1 = x by POWER:def 3;
hence thesis;
end;