:: Solving the Roots of the Special Polynomial Equation with Real :: Coefficients :: by Yuzhong Ding and Xiquan Liang :: :: Received March 18, 2004 :: Copyright (c) 2004-2018 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, BOOLE; 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) 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)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)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)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 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,A9,POWER:6; 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;