:: Solving Complex Roots of Polynomial Equation of Degree 2 and 3 with :: Complex Coefficients :: by Yuzhong Ding and Xiquan Liang :: :: Received January 26, 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, RELAT_1, ARYTM_3, SQUARE_1, COMPLEX1, ARYTM_1, XCMPLX_0, POLYEQ_1, CARD_1, FUNCT_3, XXREAL_0, NEWTON, POWER, NAT_1, SIN_COS, COMPTRIG, FUNCT_1, POLYEQ_3; notations SUBSET_1, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, REAL_1, COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, QUIN_1, POWER, NAT_1, SIN_COS, COMPTRIG; constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, QUIN_1, PREPOWER, POWER, POLYEQ_1, BINARITH, SIN_COS, COMPTRIG, VALUED_1, BINOP_2, NAT_D, XREAL_0, ABIAN, NEWTON, XCMPLX_0; registrations XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON, POLYEQ_1, VALUED_0, RELSET_1, POWER, SIN_COS, QUIN_1, ORDINAL1, CARD_1; requirements ARITHM, SUBSET, REAL, NUMERALS; begin reserve a,b,c,d,a9,b9,c9,d9,y,x1,u,v for Real, s,t,h,z,z1,z2,z3,s1,s2,s3 for Complex; definition let z be Element of COMPLEX; redefine func z^2 -> Element of COMPLEX equals :: POLYEQ_3:def 1 (Re z)^2-(Im z)^2 + 2*(Re z*Im z)*; end; definition ::$CD let a,b,c,z; redefine func Polynom (a,b,c,z) -> Element of COMPLEX; end; theorem :: POLYEQ_3:1 a <> 0 & delta(a,b,c) >=0 & Polynom(a,b,c,z) = 0 implies z= (-b+ sqrt delta(a,b,c))/(2*a) or z= (-b-sqrt delta(a,b,c))/(2*a) or z= -b/(2*a); theorem :: POLYEQ_3:2 a <> 0 & delta(a,b,c) < 0 & Polynom(a,b,c,z) = 0 implies z= -b/(2 *a)+(sqrt (-delta(a,b,c))/(2*a))* or z= -b/(2*a)+(-sqrt (-delta(a,b,c))/(2*a ))*; theorem :: POLYEQ_3:3 b <> 0 & (for z holds Polynom(0,b,c,z) = 0) implies z = -c/b; theorem :: POLYEQ_3:4 for a,b,c being Real,z,z1,z2 being Complex st a <> 0 & for z being Complex holds Polynom(a,b,c,z) = Quard(a,z1,z2,z) holds b/a =-(z1+ z2) & c/a = z1*z2; definition let z be Complex; func z^3 -> Element of COMPLEX equals :: POLYEQ_3:def 3 z^2*z; end; definition let a,b,c,d,z be Complex; redefine func Polynom(a,b,c,d,z) equals :: POLYEQ_3:def 4 a*z^3 + b*z^2 + c*z + d; end; theorem :: POLYEQ_3:5 Re z^3 = (Re z)|^3 - 3*Re z*(Im z)^2 & Im z^3 = -(Im z)|^ 3+3*( Re z)^2*Im z; theorem :: POLYEQ_3:6 (for z being Complex holds Polynom(a,b,c,d,z) = Polynom(a9,b9, c9,d9,z ) ) implies a = a9 & b = b9 & c = c9 & d = d9; theorem :: POLYEQ_3:7 b<>0 & delta(b,c,d)>=0 & Polynom(0,b,c,d,z)=0 implies z = (-c+sqrt delta(b,c,d))/(2*b) or z = (-c-sqrt delta(b,c,d))/(2*b) or z = -c/(2*b); theorem :: POLYEQ_3:8 b<>0 & delta(b,c,d)<0 & Polynom(0,b,c,d,z)=0 implies z = -c/(2*b)+( sqrt (-delta(b,c,d))/(2*b))* or z = -c/(2*b)+(-sqrt (-delta(b,c,d))/(2*b))* ; theorem :: POLYEQ_3:9 a<>0 & 4*a*c <= 0 & Polynom(a,0,c,0,z)=0 implies z = (sqrt -4*a*c)/(2* a) or z = (-sqrt -4*a*c)/(2*a) or z = 0; theorem :: POLYEQ_3:10 a<>0 & delta(a,b,c)>=0 & Polynom(a,b,c,0,z)=0 implies z = (-b+sqrt delta(a,b,c))/(2*a) or z = (-b-sqrt delta(a,b,c))/(2*a) or z = -b/(2*a) or z = 0; theorem :: POLYEQ_3:11 a<>0 & delta(a,b,c)<0 & Polynom(a,b,c,0,z)=0 implies z= -b/(2*a)+(sqrt (-delta(a,b,c))/(2*a))* or z= -b/(2*a)+(-sqrt (-delta(a,b,c))/(2*a))* or z = 0; theorem :: POLYEQ_3:12 y^2 = a implies y = sqrt a or y = -sqrt a; theorem :: POLYEQ_3:13 a<>0 & Im z = 0 & Polynom(a,0,c,d,z)=0 implies for u,v st Re z = u+v & 3*v*u+c/a=0 holds z = 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 z = 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 z = 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_3:14 a<>0 & Im z <> 0 & Polynom(a,0,c,d,z)=0 implies for u,v st Re z = u+v & 3*v*u+c/(4*a)=0 holds z=3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) + 3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3))+ sqrt(3*(3-root(d/(16*a)+ sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) + 3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12* a)) |^ 3)))^2+c/a)* or z=3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) +3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) -sqrt(3*(3-root(d/(16*a)+ sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) +3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a )) |^ 3)))^2+c/a)* or z=2*(3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3 )))+ sqrt(3*(2*(3-root(d/(16*a)+sqrt((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)* or z=2*(3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3))) -sqrt(3*(2*(3 -root(d/(16*a)+sqrt((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)* or z=2*(3-root (d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)))+ sqrt(3*(2*(3-root(d/(16*a)-sqrt ((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)* or z=2*(3-root(d/(16*a)-sqrt((d/( 16*a))^2+(c/(12*a)) |^ 3))) -sqrt(3*(2*(3-root(d/(16*a)-sqrt((d/(16*a))^2 +(c/( 12*a)) |^ 3))))^2+c/a)*; theorem :: POLYEQ_3:15 a<>0 & Polynom(a,b,c,d,z)=0 & Im z=0 implies for u,v,x1 st x1=Re z + b /(3*a) & Re z=u+v-b/(3*a) & 3*u*v+(3*a*c-b^2)/(3*a^2)=0 holds z =3-root(-(b/(3* a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) - sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3)) -b/(3*a)+0* or z =3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3 *a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/ (3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2)) ^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3))-b/(3*a)+0* or z =3-root(-(b/(3*a)) |^ 3-( 3*a*d-b*c)/(6*a^2) -sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c- b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) -sqrt((2*((b/ (3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3))-b/(3*a)+0* ; theorem :: POLYEQ_3:16 z1 <> 0 & Polynom(z1,z2,z) = 0 implies z = -(z2/z1); begin theorem :: POLYEQ_3:17 (for z holds Polynom(z1,z2,z3,z) = Polynom(s1,s2,s3,z)) implies z1 = s1 & z2 = s2 & z3 = s3; theorem :: POLYEQ_3:18 (-a+sqrt (a^2+b^2))/2 >=0 & (a+sqrt (a^2+b^2))/2>=0; theorem :: POLYEQ_3:19 z^2 = s & Im s >= 0 implies z=sqrt (( Re s+sqrt ((Re s)^2+(Im s) ^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z=-sqrt (( Re s+ sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*; theorem :: POLYEQ_3:20 z^2 = s & Im s = 0 & Re s > 0 implies z=sqrt(Re s) or z=-sqrt(Re s); theorem :: POLYEQ_3:21 z^2 = s & Im s = 0 & Re s < 0 implies z= sqrt (-Re s)* or z= -sqrt (-Re s)*; theorem :: POLYEQ_3:22 z^2 = s & Im s <0 implies z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2) + (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*; theorem :: POLYEQ_3:23 z^2 = s implies z=sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ ( sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z=-sqrt (( Re s+sqrt ((Re s) ^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z= sqrt ( ( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2 ))* or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*; theorem :: POLYEQ_3:24 z1<>0 & Polynom(z1,z2,0,z)=0 implies z=-(z2/z1) or z=0; theorem :: POLYEQ_3:25 z1<>0 & Polynom(z1,0,z3,z)=0 implies for s st s=-(z3/z1) holds z = sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s )^2))/2))* or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+ sqrt ((Re s)^2+(Im s)^2))/2))* or z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/ 2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z=-sqrt (( Re s+sqrt (( Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*; theorem :: POLYEQ_3:26 z1<>0 & Polynom(z1,z2,z3,z)=0 implies for h,t st h=(z2/(2*z1))^2 -z3/z1 & t=z2/(2*z1) holds z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t or z=-sqrt (( Re h+sqrt ((Re h)^2+( Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t or z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2)) *-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t; theorem :: POLYEQ_3:27 z|^ 3=z*z*z & z|^ 3=z^2*z & z|^ 3 = z^3; theorem :: POLYEQ_3:28 z1<>0 & Polynom(z1,z2,0,0,z)=0 implies z=-z2/z1 or z=0; theorem :: POLYEQ_3:29 z1<>0 & Polynom(z1,0,z3,0,z)=0 implies for s st s=-(z3/z1) holds z=0 or z=sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+( Im s)^2))/2))* or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2) )/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))* or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*; theorem :: POLYEQ_3:30 z1<>0 & Polynom(z1,z2,z3,0,z)=0 implies for s,h,t st h=(z2/(2*z1))^2- z3/z1 & t=z2/(2*z1) holds z=0 or z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t or z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h) ^2))/2))*-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+ sqrt ((Re h)^2+(Im h)^2))/2))*-t; theorem :: POLYEQ_3:31 for x being Real, n be Nat holds (cos x + sin x*) |^ n = cos (n*x) + sin (n*x)*; theorem :: POLYEQ_3:32 for z being Element of COMPLEX for n being Element of NAT holds z|^ n = (|.z.| to_power n)*cos (n*Arg z) + (|.z.| to_power n)*sin ( n*Arg z)*; theorem :: POLYEQ_3:33 for n,k be Element of NAT,x be Real st n <> 0 holds (cos((x+2*PI *k)/n) + sin((x+2*PI*k)/n)*)|^ n = cos x + (sin x)*; theorem :: POLYEQ_3:34 for z be Complex for n,k be Element of NAT st n <> 0 holds z = ((n-root |.z.|)*cos((Arg z+2*PI*k)/n) + (n-root |.z.|)*sin((Arg z+2* PI*k)/n)*)|^ n; theorem :: POLYEQ_3:35 for z be Element of COMPLEX, n be non zero Element of NAT, k be Element of NAT holds (n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin(( Arg z+2*PI*k)/n)* is CRoot of n,z; theorem :: POLYEQ_3:36 for z be Complex, v be CRoot of 1,z holds v = z; theorem :: POLYEQ_3:37 for n be non zero Nat, v be CRoot of n,0 holds v = 0; theorem :: POLYEQ_3:38 for n be non zero Element of NAT, z be Complex for v be CRoot of n,z st v = 0 holds z = 0; theorem :: POLYEQ_3:39 for n be non zero Element of NAT, k be Element of NAT holds cos(2*PI* k/n) + sin(2*PI*k/n)* is CRoot of n,1; theorem :: POLYEQ_3:40 for z,s being Element of COMPLEX, n being Element of NAT st s<>0 & z<> 0 & n>=1 & s|^ n=z|^ n holds |.s.| = |.z.|;