:: Solving Roots of Polynomial Equations of Degree 2 and 3 with :: Real Coefficients :: by Liang Xiquan :: :: Received May 18, 2000 :: Copyright (c) 2000-2017 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, XREAL_0, XCMPLX_0, RELAT_1, ARYTM_3, REAL_1, CARD_1, ARYTM_1, SQUARE_1, FUNCT_3, XXREAL_0, NEWTON, POWER, PREPOWER, POLYEQ_1, ABIAN, ORDINAL1; notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SQUARE_1, NEWTON, PREPOWER, POWER, QUIN_1, XXREAL_0, ABIAN; constructors REAL_1, SQUARE_1, NAT_1, MEMBERED, QUIN_1, NEWTON, PREPOWER, POWER, ABIAN; registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON; requirements NUMERALS, SUBSET, REAL, ARITHM, BOOLE; begin :: Polynomial of Degree 1 and 2 reserve a, a9, a1, a2, a3, b, b9, c, c9, d, d9, h, p, q, x, x1, x2, x3, u, v, y, z for Real; definition let a, b, x be Complex; func Polynom (a,b,x) -> number equals :: POLYEQ_1:def 1 a*x+b; end; registration let a, b, x be Complex; cluster Polynom(a,b,x) -> complex; end; registration let a, b, x be Real; cluster Polynom(a,b,x) -> real; end; theorem :: POLYEQ_1:1 for a, b, x being Complex holds a <> 0 & Polynom(a,b,x) = 0 implies x = -(b/a); theorem :: POLYEQ_1:2 for x being Complex holds Polynom(0,0,x) = 0; theorem :: POLYEQ_1:3 for b being Complex holds b <> 0 implies not ex x being Complex st Polynom(0,b,x) = 0; definition let a,b,c,x be Complex; func Polynom(a,b,c,x) -> number equals :: POLYEQ_1:def 2 a*x^2+b*x+c; end; registration let a,b,c,x be Real; cluster Polynom(a,b,c,x) -> real; end; registration let a,b,c,x be Complex; cluster Polynom(a,b,c,x) -> complex; end; theorem :: POLYEQ_1:4 for a, b, c, a9, b9, c9 being Complex holds (for x being Real holds Polynom(a,b,c,x) = Polynom(a9,b9,c9,x)) implies a = a9& b = b9& c = c9; theorem :: POLYEQ_1:5 a <> 0 & delta(a,b,c) >= 0 implies for x holds Polynom(a,b,c,x) = 0 implies x = (-b+sqrt delta(a,b,c))/(2*a) or x = (-b-sqrt delta(a,b,c))/(2*a); theorem :: POLYEQ_1:6 for a, b, c, x being Complex holds a <> 0 & delta(a,b,c) = 0 & Polynom(a,b,c,x) = 0 implies x = -(b/(2*a)); theorem :: POLYEQ_1:7 delta(a,b,c) < 0 implies not ex x st Polynom(a,b,c,x) = 0; theorem :: POLYEQ_1:8 for b, c being Complex holds b <> 0 & (for x being Real holds Polynom(0,b,c,x) = 0) implies x = -(c/b); theorem :: POLYEQ_1:9 for x being Complex holds Polynom(0,0,0,x) = 0; theorem :: POLYEQ_1:10 for c being Complex holds c <> 0 implies not ex x being Complex st Polynom(0,0,c,x) = 0; definition let a,x,x1,x2 be Complex; func Quard(a,x1,x2,x) -> number equals :: POLYEQ_1:def 3 a*((x-x1)*(x-x2)); end; registration let a,x,x1,x2 be Real; cluster Quard(a,x1,x2,x) -> real; end; theorem :: POLYEQ_1:11 for a, b, c being Complex holds a <> 0 & (for x being Real holds Polynom(a,b,c,x) = Quard(a,x1,x2,x)) implies b/a = -(x1+x2) & c/a = x1*x2; begin :: Polynomial of Degree 3 definition let a,b,c,d,x be Complex; func Polynom(a,b,c,d,x) -> number equals :: POLYEQ_1:def 4 a*(x |^ 3)+ b*x^2 +c*x +d; end; registration let a,b,c,d,x be Complex; cluster Polynom(a,b,c,d,x) -> complex; end; registration let a,b,c,d,x be Real; cluster Polynom(a,b,c,d,x) -> real; end; theorem :: POLYEQ_1:12 (for x holds Polynom(a,b,c,d,x) = Polynom(a9,b9,c9,d9,x)) implies a = a9 & b = b9 & c = c9 & d = d9; definition let a,x,x1,x2,x3 be Complex; func Tri(a,x1,x2,x3,x) -> number equals :: POLYEQ_1:def 5 a*((x-x1)*(x-x2)*(x-x3)); end; registration let a,x,x1,x2,x3 be Real; cluster Tri(a,x1,x2,x3,x) -> real; end; theorem :: POLYEQ_1:13 a <> 0 & (for x holds Polynom(a,b,c,d,x) = Tri(a,x1,x2,x3,x)) implies b/a = -(x1+x2+x3) & c/a = x1*x2 +x2*x3 +x1*x3 & d/a = -x1*x2*x3; theorem :: POLYEQ_1:14 (y+h) |^ 3 = y |^ 3+((3*h)*y^2+(3*h^2)*y)+h |^ 3; theorem :: POLYEQ_1:15 a <> 0 & Polynom(a,b,c,d,x) = 0 implies for a1,a2,a3,h,y st y = (x+b/(3*a)) & h = -b/(3*a) & a1 = b/a & a2 = c/a & a3 = d/a holds y |^ 3 + ((3* h+a1)*y^2+(3*h^2+2*(a1*h)+a2)*y) + ((h |^ 3+a1*h^2)+(a2*h+a3)) = 0; theorem :: POLYEQ_1:16 a <> 0 & Polynom(a,b,c,d,x) = 0 implies for a1,a2,a3,h,y st y = (x+b/( 3*a)) & h = -b/(3*a) & a1 = b/a & a2 = c/a & a3 = d/a holds y |^ 3 + 0*y^2 + (( 3*a*c-b^2)/(3*a^2))*y + (2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2)) = 0; theorem :: POLYEQ_1:17 (y |^ 3)+0*y^2+((3*a*c-b^2)/(3*a^2))*y + (2*((b/(3*a)) |^ 3)+(3*a*d-b* c)/(3*a^2)) = 0 implies for p,q st p = (3*a*c-b^2)/(3*a^2) & q = 2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2) holds Polynom(1,0,p,q,y) = 0; theorem :: POLYEQ_1:18 Polynom(1,0,p,q,y) = 0 implies for u,v st y = u+v & 3*v*u+p = 0 holds u |^ 3 + v |^ 3 = -q & (u |^ 3)*(v |^ 3) = (-p/3) |^ 3; theorem :: POLYEQ_1:19 Polynom(1,0,p,q,y) = 0 implies for u,v st y = u+v & 3*v*u+p = 0 holds y = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) or y = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) or y = 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(p/3 ) |^ 3)); theorem :: POLYEQ_1:20 b <> 0 & delta(b,c,d) > 0 & Polynom(0,b,c,d,x) = 0 implies x = (-c+ sqrt delta(b,c,d))/(2*b) or x = (-c-sqrt delta(b,c,d))/(2*b); theorem :: POLYEQ_1:21 a <> 0 & p = c/a & q = d/a & Polynom(a,0,c,d,x) = 0 implies for u,v st x = u+v & 3*v*u+p = 0 holds x = 3-root(-d/(2*a)+sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) +3-root(-d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) or x = 3-root(-d/(2*a) +sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) +3-root(-d/(2*a)+sqrt((d^2/(4*a^2))+(c/(3* a)) |^ 3)) or x = 3-root(-d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)) +3-root(- d/(2*a)-sqrt((d^2/(4*a^2))+(c/(3*a)) |^ 3)); theorem :: POLYEQ_1:22 a <> 0 & delta(a,b,c) >= 0 & Polynom(a,b,c,0,x) = 0 implies x = 0 or x = (-b+sqrt delta(a,b,c))/(2*a) or x = (-b-sqrt delta(a,b,c))/(2*a); theorem :: POLYEQ_1:23 a <> 0 & c/a < 0 & Polynom(a,0,c,0,x) = 0 implies x = 0 or x = sqrt -c /a or x = -sqrt(-c/a);