:: Solving the Roots of the Special Polynomial Equation with Real :: Coefficients :: by Yuzhong Ding and Xiquan Liang :: :: Received March 18, 2004 :: Copyright (c) 2004-2021 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; begin reserve x,y,a,b,c,p,q for Real; reserve m,n for Element of NAT; theorem :: POLYEQ_4:1 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; theorem :: POLYEQ_4:2 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; theorem :: POLYEQ_4:3 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; theorem :: POLYEQ_4:4 a>0 & n is even & n >= 1 & x |^ n = a implies x = n-root a or x = -n-root a; theorem :: POLYEQ_4:5 a <> 0 & Polynom(a,b,0,x) = 0 implies x=0 or x = -(b/a); theorem :: POLYEQ_4:6 a <> 0 & Polynom(a,0,0,x) = 0 implies x=0; theorem :: POLYEQ_4:7 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)); theorem :: POLYEQ_4:8 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)); theorem :: POLYEQ_4:9 a <> 0 & n is odd & Polynom(a,b,0,x|^ n) = 0 implies x=0 or x = n-root -(b/a) ; theorem :: POLYEQ_4:10 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); theorem :: POLYEQ_4:11 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); theorem :: POLYEQ_4:12 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); definition let a,b,c,d,e,f,x be Complex; func Polynom(a,b,c,d,e,f,x) -> set equals :: POLYEQ_4:def 1 a*(x|^5)+b*(x|^4)+c*(x|^3)+d*(x^2)+e*x+f; end; registration let a,b,c,d,e,f,x be Complex; cluster Polynom(a,b,c,d,e,f,x) -> complex; end; registration let a,b,c,d,e,f,x be Real; cluster Polynom(a,b,c,d,e,f,x) -> real; end; theorem :: POLYEQ_4:13 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; theorem :: POLYEQ_4:14 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; theorem :: POLYEQ_4:15 (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); theorem :: POLYEQ_4:16 (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); theorem :: POLYEQ_4:17 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); theorem :: POLYEQ_4:18 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; theorem :: POLYEQ_4:19 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; theorem :: POLYEQ_4:20 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) ; theorem :: POLYEQ_4:21 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); theorem :: POLYEQ_4:22 for a,x being Real st a>0 & a<>1 & a to_power x = 1 holds x=0; theorem :: POLYEQ_4:23 for a,x being Real st a>0 & a<>1 & a to_power x = a holds x=1; theorem :: POLYEQ_4:24 for a,b,x being Real st a>0 & a<>1 & x>0 & log(a,x) = 0 holds x = 1; theorem :: POLYEQ_4:25 for a,b,x being Real st a>0 & a<>1 & x>0 & log(a,x) = 1 holds x = a;