:: Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients :: by Xiquan Liang :: :: Received February 3, 2003 :: Copyright (c) 2003-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, RELAT_1, XCMPLX_0, POLYEQ_1, NEWTON, ARYTM_3, SQUARE_1, XREAL_0, CARD_1, ARYTM_1, XXREAL_0, FUNCT_3, POWER, COMPLEX1, POLYEQ_2, ABIAN, REAL_1; notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, INT_1, NEWTON, ABIAN, POWER, COMPLEX1, QUIN_1, XXREAL_0, POLYEQ_1; constructors REAL_1, SQUARE_1, NAT_1, MEMBERED, QUIN_1, NEWTON, PREPOWER, POLYEQ_1, SERIES_1, ABIAN; registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, POWER; requirements REAL, SUBSET, NUMERALS, ARITHM; begin definition let a,b,c,d,e,x be Complex; func Polynom(a,b,c,d,e,x) -> set equals :: POLYEQ_2:def 1 a*(x |^ 4)+b*(x |^ 3)+c*(x^2)+d*x+e; end; registration let a,b,c,d,e,x be Complex; cluster Polynom(a,b,c,d,e,x) -> complex; end; registration let a,b,c,d,e,x be Real; cluster Polynom(a,b,c,d,e,x) -> real; end; theorem :: POLYEQ_2:1 for a,c,e,x being Real st a <> 0 & e <> 0 & c^2 - (4*a*e) > 0 holds Polynom(a,0,c,0,e,x) = 0 implies x <> 0 & (x = sqrt((-c + sqrt delta(a,c, e))/(2*a)) or x = sqrt((-c - sqrt delta(a,c,e))/(2*a)) or x = - sqrt((-c + sqrt delta(a,c,e))/(2*a)) or x = - sqrt((-c - sqrt delta(a,c,e))/(2*a))); theorem :: POLYEQ_2:2 for a,b,c,x,y being Real st a <> 0 & y = x + 1/x holds Polynom(a,b,c,b,a,x) = 0 implies x <> 0 & a*y^2 + b*y + c - 2*a = 0; theorem :: POLYEQ_2:3 for a,b,c,x,y being Real st a <> 0 & b^2-4*a*c + 8*a^2 > 0 & y = x + 1/x holds Polynom(a,b,c,b,a,x) = 0 implies for y1,y2 being Real st y1 = (-b+sqrt(b^2-4*a*c+8*a^2))/(2*a) & y2 = (-b-sqrt(b^2-4*a*c+8*a^2))/(2*a) holds x <> 0 & (x = (y1 + sqrt delta(1,(-y1),1))/2 or x = (y2 + sqrt delta(1,(- y2),1))/2 or x = (y1 - sqrt delta(1,(-y1),1))/2 or x = (y2 - sqrt delta(1,(-y2) ,1))/2); theorem :: POLYEQ_2:4 for x being Real holds x|^ 3 = x^2*x & (x|^ 3)*x = x|^ 4 & x^2*x^2 = x|^ 4; theorem :: POLYEQ_2:5 for x,y being Real st x+y <> 0 holds (x+y)|^ 4 = (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*x + (x|^ 3 + ((3*y)*x^2+(3*y^2)*x) +y|^ 3)*y; theorem :: POLYEQ_2:6 for x,y being Real st x+y <> 0 holds (x+y)|^ 4 = x|^ 4+((4*y)*( x|^ 3)+6*y^2*x^2+4*(y|^ 3)*x)+y|^ 4; theorem :: POLYEQ_2:7 for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real holds (for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(b1,b2,b3,b4,b5,x)) implies a5=b5 & a1-a2+a3-a4 = b1-b2+b3-b4 & a1+a2+a3+a4 = b1+b2+b3+b4; theorem :: POLYEQ_2:8 for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real holds (for x being Real holds Polynom(a1,a2,a3,a4,a5,x)=Polynom(b1,b2,b3,b4,b5,x)) implies a1-b1=b3-a3 & a2-b2=b4-a4; theorem :: POLYEQ_2:9 for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 being Real st (for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Polynom(b1,b2,b3,b4,b5,x)) holds a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5; definition let a1,x1,x2,x3,x4,x be Real; func Four0(a1,x1,x2,x3,x4,x) -> set equals :: POLYEQ_2:def 2 a1*((x-x1)*(x-x2)*(x-x3)*(x-x4)); end; registration let a1,x1,x2,x3,x4,x be Real; cluster Four0(a1,x1,x2,x3,x4,x) -> real; end; theorem :: POLYEQ_2:10 for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being Real st a1 <> 0 holds (for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2 ,x3,x4,x)) implies (a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1 = x^2*x^2-(x1+x2+ x3)*(x^2*x)+(x1*x3+x2*x3+x1*x2)*x^2 - (x1*x2*x3)*x-((x-x1)*(x-x2)*(x-x3))*x4; theorem :: POLYEQ_2:11 for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 being Real st a1 <> 0 holds (for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2 ,x3,x4,x)) implies (a1*(x|^ 4)+a2*(x|^ 3)+a3*x^2+a4*x+a5)/a1 = x|^ 4-(x1+x2+x3+ x4)*x|^ 3 +((x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4)*x^2 -(x1*x2*x3+x1*x2*x4+x1 *x3*x4+x2*x3*x4)*x+(x1*x2*x3*x4); theorem :: POLYEQ_2:12 for a1,a2,a3,a4,a5,x1,x2,x3,x4 being Real st a1 <> 0 & (for x being Real holds Polynom(a1,a2,a3,a4,a5,x) = Four0(a1,x1,x2,x3,x4,x)) holds a2/a1 = -(x1+x2+x3+x4) & a3/a1 = (x1*x2+x1*x3+x1*x4)+(x2*x3+x2*x4)+x3*x4 & a4/a1 = -(x1*x2*x3+x1*x2*x4+x1*x3*x4+x2*x3*x4) & a5/a1 = x1*x2*x3*x4; theorem :: POLYEQ_2:13 for a,k,y being Real st a <> 0 holds (for x being Real holds x|^ 4+a|^ 4 = k*a*x*(x^2+a^2)) implies y|^ 4 -k*(y|^ 3)-k*y+1 = 0;