:: 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-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, 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, BOOLE, NUMERALS; equalities POLYEQ_1, SQUARE_1, XCMPLX_0, QUIN_1; theorems COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, COMPTRIG, NAT_1, POWER, SIN_COS, SIN_COS2, XCMPLX_0, XCMPLX_1, XREAL_1; schemes NAT_1, COMPTRIG; 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 (Re z)^2-(Im z)^2 + 2*(Re z*Im z)*; compatibility proof z = Re z +(Im z)* by COMPLEX1:13; hence thesis; end; correctness by XCMPLX_0:def 2; end; definition ::\$CD let a,b,c,z; redefine func Polynom (a,b,c,z) -> Element of COMPLEX; coherence by XCMPLX_0:def 2; end; theorem Th1: 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) proof A1: a = a+0*; set y=Im z; A2: z = Re z + (Im z)* by COMPLEX1:13; set x=Re z; assume that A3: a <> 0 and A4: delta(a,b,c) >= 0; assume Polynom(a,b,c,z) = 0; then (a+0*)*(x^2-y^2+2*(x*y)*)+b*z+c = 0 by A2; then 0 = Re a*Re (x^2-y^2+(2*x*y)*) -Im a*Im (x^2-y^2+2*x*y*)+ (Re a*Im (x^2-y^2+2*x*y*) +Re (x^2-y^2+2*x*y*)*Im a)* +b*z+c by COMPLEX1:82 .=(a*Re (x^2-y^2+2*x*y*)-Im a* Im (x^2-y^2+2*x*y*))+(Re a*Im (x^2- y^2+2*x*y*) +Re (x^2-y^2+2*x*y*)*Im a)* +b*z+c by A1,COMPLEX1:12 .=(a*(x^2-y^2)-Im a* Im (x^2-y^2+2*x*y*))+(Re a*Im (x^2-y^2+2*x*y* ) +Re (x^2-y^2+2*x*y*)*Im a)* +b*z+c by COMPLEX1:12 .=(a*(x^2-y^2)-0*Im (x^2-y^2+2*x*y*) )+(Re a*Im (x^2-y^2+2*x*y*)+ Re (x^2-y^2+2*x*y*) *Im a )* +b*z+c by A1,COMPLEX1:12 .=(a*(x^2-y^2)-0)+(Re a*(2*x*y)+Re (x^2-y^2+2*x*y*) *Im a )* +b*z+ c by COMPLEX1:12 .=(a*(x^2-y^2)-0)+(a*(2*x*y)+Re (x^2-y^2+2*x*y*) *Im a )* +b*z+c by A1,COMPLEX1:12 .=(a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *Im a )* +b*z+c by COMPLEX1:12 .=(a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2)*0)* +b*z+c by A1,COMPLEX1:12; then A5: (a*(x^2-y^2)-0*(2*x*y))+(0+a*(2*x*y))* +(b+0*)*(x+y*)+c = 0 by COMPLEX1:13; then A6: a*(x^2-y^2)+b*x+c+(a*(2*x*y)+b*y)* = 0; then A7: (2*a*x+b)*y = 0 by COMPLEX1:4,12; per cases by A7; suppose A8: y = 0; then Polynom(a,b,c,x)=0 by A5; then Re z=(-b+sqrt delta(a,b,c))/(2*a) & Im z = 0 or Re z= (-b-sqrt delta( a,b,c))/(2*a) & Im z = 0 by A3,A4,A8,POLYEQ_1:5; then z=(-b+sqrt delta(a,b,c))/(2*a)+0* or z= (-b-sqrt delta(a,b,c))/(2* a)+0* by COMPLEX1:13; hence thesis; end; suppose 2*a*x+b = 0; then A9: x= (-b)/(2*a) by A3,XCMPLX_1:89; then a*((b/(2*a))^2-y^2)+b*(-b/(2*a))+c = 0 by A6,COMPLEX1:4,12; then (b/(2*a))^2-y^2 = (-(b*(-b/(2*a))+c))/a-0 by A3,XCMPLX_1:89; then (b/(2*a))^2- (-(b*(-b/(2*a))+c))/a= y^2-0; then y^2 = (b/(2*a))^2+c*a"-((b^2/(2*a))*a"); then y^2 *((2*a)^2)=(b^2/(2*a)^2+c*a"-((b^2/(2*a))*a"))*((2*a)^2) by XCMPLX_1:76 .=b^2/((2*a)^2)*((2*a)^2)+(c*a")*(2*a)^2 -(b^2*(2*a)"*a")*(2*a)^2; then A10: y ^2 *((2*a)^2)=b^2+(c*a")*(2*a)^2-(b^2*((2*a)"*a"))*(2*a)^2 by A3,XCMPLX_1:87 .=b^2+(c*a")*(2*a)^2-(b^2*((2*a)*a)")*(2*a)^2 by XCMPLX_1:204 .=b^2+(c*a")*(2*a)^2-(b^2*(2*(a*a))")*(2*a)^2; set t = (b^2*(2*(a*a))")*(2*a)^2; t*((2*a)^2)" = b^2*(2*(a*a))"*(((2*a)^2)*(1/(2*a)^2)); then t*((2*a)^2)" = b^2*(2*(a*a))"*1 by A3,XCMPLX_1:106; then t*((2*a)^2)"*2" = b^2*(2*a^2)"*2"; then t*((2*a)^2)"*2" = b^2*((2*a^2)"*2"); then t*((2*a)^2)"*2" = b^2*((2*(a^2*2))") by XCMPLX_1:204; then (t*2")/(2*a)^2*(2*a)^2 = b^2/(2*a)^2*(2*a)^2; then t*2" = b^2/(2*a)^2*(2*a)^2 by A3,XCMPLX_1:87; then A11: t/2 = b^2 by A3,XCMPLX_1:87; set t=(c*a")*(2*a)^2; t=(c/a*a)*2*(2*a); then A12: t=c*2*(2*a) by A3,XCMPLX_1:87; -delta(a,b,c) <= 0 by A4; then (y *(2*a))^2 = 0 by A10,A11,A12,XREAL_1:63; then Im z=0 by A3; then z = -b/(2*a)+0* by A9,COMPLEX1:13; hence thesis; end; end; theorem Th2: 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 ))* proof assume that A1: a <> 0 and A2: delta(a,b,c) < 0; A3: a= a+0*; now set t2=(-b^2+c*a*4)/4; let z; set x=Re z; set y=Im z; A4: z = x + y* by COMPLEX1:13; assume Polynom(a,b,c,z) = 0; then (a+0*)*(x^2-y^2+(2*x*y)*)+b*z+c = 0 by A4; then Re a*Re (x^2-y^2+2*x*y*)-Im a*Im (x^2-y^2+(2*x*y)*) +(Re a*Im (x ^2-y^2+2*x*y*)+Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by COMPLEX1:82; then (a*Re (x^2-y^2+2*x*y*)-Im a*Im (x^2-y^2+2*x*y*) )+(Re a*Im (x^2- y^2+2*x*y*)+Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by A3,COMPLEX1:12; then (a*(x^2-y^2)-Im a*Im (x^2-y^2+2*x*y*) )+(Re a*Im (x^2-y^2+2*x*y* )+Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by COMPLEX1:12; then (a*(x^2-y^2)-0*Im (x^2-y^2+2*x*y*) )+(Re a*Im (x^2-y^2+2*x*y*)+ Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by A3,COMPLEX1:12; then (a*(x^2-y^2)-0)+(Re a*(2*x*y)+Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by COMPLEX1:12; then (a*(x^2-y^2)-0)+(a*(2*x*y)+Re (x^2-y^2+2*x*y*) *Im a)*+b*z+c = 0 by A3,COMPLEX1:12; then (a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *Im a)*+b*z+c = 0 by COMPLEX1:12; then (a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *0)*+b*z+c = 0 by A3, COMPLEX1:12; then (a*(x^2-y^2)-0*(2*x*y))+((x^2-y^2)*0+a*(2*x*y))* +(b+0*)*(x+y* )+c = 0 by COMPLEX1:13; then A5: a*(x^2-y^2)+b*x+c+(a*(2*x*y)+b*y)* = 0; then (a*(2*x))*y+b*y = 0 by COMPLEX1:4,12; then A6: (a*2*x)*y = (-b)*y; set t = (b^2*(2*(a*a))")*(2*a)^2; set t1= (x*a+b/2)^2; 0-delta(a,b,c)>0 by A2; then A7: 0+00 by A7; then a*(2*x) = -b by A6,XCMPLX_1:5; then 2*x = (-b)/a by A1,XCMPLX_1:89; then x = 1/a*((-b)/2); then A8: x = (-b)/(2*a) by XCMPLX_1:103; then a*((b/(2*a))^2-y^2)+b*(-b/(2*a))+c = 0 by A5,COMPLEX1:4,12; then (b/(2*a))^2-y^2 = (-(b*(-b/(2*a))+c))/a-0 by A1,XCMPLX_1:89; then (b/(2*a))^2- (-(b*(-b/(2*a))+c))/a= y^2-0; then y^2 = (b/(2*a))^2+c*a"-((b^2/(2*a))*a"); then y^2 *((2*a)^2)=(b^2/(2*a)^2+c*a"-((b^2/(2*a))*a"))*((2*a)^2) by XCMPLX_1:76 .=b^2/((2*a)^2)*((2*a)^2)+(c*a")*(2*a)^2 -(b^2*(2*a)"*a")*(2*a)^2; then A9: y ^2 *((2*a)^2)=b^2+(c*a")*(2*a)^2-(b^2*((2*a)"*a"))*(2*a)^2 by A1,XCMPLX_1:87 .=b^2+(c*a")*(2*a)^2-(b^2*((2*a)*a)")*(2*a)^2 by XCMPLX_1:204 .=b^2+(c*a")*(2*a)^2-(b^2*(2*(a*a))")*(2*a)^2; t*((2*a)^2)" = b^2*(2*(a*a))"*(((2*a)^2)*(1/(2*a)^2)); then t*((2*a)^2)" = b^2*(2*(a*a))"*1 by A1,XCMPLX_1:106; then t*((2*a)^2)"*2" = b^2*(2*a^2)"*2"; then t*((2*a)^2)"*2" = b^2*((2*a^2)"*2"); then t*((2*a)^2)"*2" = b^2*((2*(a^2*2))") by XCMPLX_1:204; then (t*2")/(2*a)^2*(2*a)^2 = b^2/(2*a)^2*(2*a)^2; then t*2" = b^2/(2*a)^2*(2*a)^2 by A1,XCMPLX_1:87; then A10: t/2 = b^2 by A1,XCMPLX_1:87; set t=(c*a")*(2*a)^2; t=(c/a*a)*2*(2*a); then t=c*2*(2*a) by A1,XCMPLX_1:87; then (y *(2*a))^2 =(sqrt (-delta(a,b,c)))^2 by A2,A9,A10,SQUARE_1:def 2; then ((y *(2*a))+(sqrt (-delta(a,b,c))))* ((y *(2*a))-(sqrt (-delta(a,b,c) )))=0; then ((y *(2*a))+(sqrt (-delta(a,b,c))))=0 or ((y *(2*a))-(sqrt (-delta(a, b,c))))=0; then y =(-sqrt (-delta(a,b,c)))/(2*a) or y *(2*a)/(2*a)=sqrt (-delta(a,b,c ))/(2*a) by A1,XCMPLX_1:89; then Re z=-b/(2*a) & Im z=sqrt (-delta(a,b,c))/(2*a) or Re z= -b/(2*a) & Im z= -sqrt (-delta(a,b,c))/(2*a) by A1,A8,XCMPLX_1:89; hence z= -b/(2*a)+(sqrt(-delta(a,b,c))/(2*a))* or z= -b/(2*a)+(-sqrt (- delta(a,b,c))/(2*a))* by COMPLEX1:13; end; hence thesis; end; theorem b <> 0 & (for z holds Polynom(0,b,c,z) = 0) implies z = -c/b proof A1: 0 = 0+0*; assume A2: b <> 0; assume A3: for z holds Polynom(0,b,c,z) = 0; now let z1; Polynom(0,b,c,z1) = 0 by A3; then b*(Re z1+(Im z1)*)+c = 0 by COMPLEX1:13; then A4: (b*Re z1-0+c+(b*Im z1+0)*)= 0+0*; then b*Re z1-0+c = Re 0 by COMPLEX1:12; then b*(Re z1)-0+c = 0 by A1,COMPLEX1:12; then A5: Re z1 =(-c)/b by A2,XCMPLX_1:89; b*Im z1= Im 0 by A4,COMPLEX1:12; then Im z1 = 0 by A1,A2,COMPLEX1:12; then z1 = -c/b+0* by A5,COMPLEX1:13; hence z1 = -c/b; end; hence thesis; end; theorem 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 proof let a,b,c be Real,z,z1,z2 be Complex; assume A1: a <> 0; assume A2: for z being Complex holds Polynom(a,b,c,z) = Quard(a,z1,z2,z); then A3: Polynom(a,b,c,0) = Quard(a,z1,z2,0); Quard(a,z1,z2,1) = Polynom(a,b,c,1) by A2 .=a+b+c; then a+b+c =a+a*(-(z1+z2))+c by A3; hence thesis by A1,A3,XCMPLX_1:203; end; definition let z be Complex; func z^3 -> Element of COMPLEX equals z^2*z; correctness by XCMPLX_0:def 2; end; Lm1: for z be Complex holds z|^2= z*z proof let z be Complex; z|^(1+1) = (z|^1)*z by NEWTON:6 .= z*z; hence thesis; end; definition let a,b,c,d,z be Complex; redefine func Polynom(a,b,c,d,z) equals a*z^3 + b*z^2 + c*z + d; compatibility proof let x be set; Polynom(a,b,c,d,z) = a*(z |^(2+1))+ b*z^2 +c*z +d .= a*((z |^2)*z)+ b*z^2 +c*z +d by NEWTON:6; hence thesis by Lm1; end; end; theorem Th5: Re z^3 = (Re z)|^3 - 3*Re z*(Im z)^2 & Im z^3 = -(Im z)|^ 3+3*( Re z)^2*Im z proof set x = Re z; set y = Im z; Re z + (Im z)* = z by COMPLEX1:13; then z^3 = Re(x^2-y^2+(2*(x*y))*) *Re (x+y*)-Im(x^2-y^2+(2*(x*y))*) *Im (x+y*)+(Re(x^2-y^2+(2*(x*y))*) *Im (x+y*)+ Re (x+y*)*Im (x^2-y ^2+(2*(x*y))*))* by COMPLEX1:82 .= ((x^2-y^2) *Re (x+y*)-Im(x^2-y^2+(2*(x*y))*) *Im (x+y*))+(Re (x^2-y^2+(2*(x*y))*) *Im (x+y*)+ Re (x+y*)*Im (x^2-y^2+(2*(x*y))*)) * by COMPLEX1:12 .= ((x^2-y^2) *Re (x+y*)-(2*(x*y)) *Im (x+y*))+(Re(x^2-y^2+(2*(x*y ))*) *Im (x+y*)+ Re (x+y*)*Im (x^2-y^2+(2*(x*y))*))* by COMPLEX1:12 .= ((x^2-y^2) *Re (x+y*)-(2*(x*y)) *Im (x+y*))+((x^2-y^2) *Im (x+y *)+ Re (x+y*)*Im (x^2-y^2+(2*(x*y))*))* by COMPLEX1:12 .= ((x^2-y^2) *Re (x+y*)-(2*(x*y))*Im (x+y*) )+((x^2-y^2) *Im (x+y *)+Re (x+y*)*(2*(x*y)))* by COMPLEX1:12 .= ((x^2-y^2) *x-(2*(x*y))*Im (x+y*) )+((x^2-y^2) *Im (x+y*)+Re (x +y*)*(2*(x*y)))* by COMPLEX1:12 .= ((x^2-y^2) *x-(2*(x*y))*y )+((x^2-y^2) *Im (x+y*)+Re (x+y*)*(2* (x*y)))* by COMPLEX1:12 .= ((x^2-y^2) *x-(2*(x*y))*y )+((x^2-y^2) *y+Re (x+y*)*(2*(x*y)))* by COMPLEX1:12 .= ((x^2*x-y^2*x+0*x)-2*(x*y)*y)+((x^2-y^2+0)*y+x*(2*(x*y)))* by COMPLEX1:12 .= ((x|^1*x*x-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))* .= ((x|^ (1+1)*x-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))* by NEWTON:6 .= ((x|^(2+1)-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))* by NEWTON:6 .= ((x|^ 3-y^2*x)-2*(x*y)*y)+((x^2*y-y|^ 1*y*y)+x*(2*(x*y)))* .= ((x|^ 3-y^2*x)-2*(x*y)*y)+((x^2*y-y|^ (1+1)*y)+x*(2*(x*y)))* by NEWTON:6 .= ((x|^ 3-y^2*x)-2*(x*(y*y)))+((x^2*y-y|^ (2+1))+x*(2*(x*y)))* by NEWTON:6 .= (x|^ 3-3*x*y^2 )+(-y|^ 3+3*x^2*y)*; hence thesis by COMPLEX1:12; end; theorem (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 proof assume A1: for z being Complex holds Polynom(a,b,c,d,z) = Polynom(a9,b9, c9,d9,z); then A2: Polynom(a,b,c,d,0) = Polynom(a9,b9,c9,d9,0); A3: Polynom(a,b,c,d,1) = Polynom(a9,b9,c9,d9,1) & Polynom(a,b,c,d,-1) = Polynom( a9,b9,c9,d9,-1) by A1; A4: Polynom(a,b,c,d,2) = Polynom(a9,b9,c9,d9,2) by A1; hence a = a9 by A2,A3; thus b = b9 by A2,A3; thus c = c9 by A2,A3,A4; thus thesis by A2; end; theorem 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) proof assume that A1: b<>0 & delta(b,c,d)>=0 and A2: Polynom(0,b,c,d,z)=0; Polynom(b,c,d,z)=0 by A2; hence thesis by A1,Th1; end; theorem 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))* proof assume that A1: b<>0 & delta(b,c,d)<0 and A2: Polynom(0,b,c,d,z)=0; Polynom(b,c,d,z)=0 by A2; hence thesis by A1,Th2; end; theorem 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 proof assume that A1: a<>0 & 4*a*c <= 0 and A2: Polynom(a,0,c,0,z)=0; (a*z^2+c)*z = 0 by A2; then Polynom(a,0,c,z) = 0 or z = 0; then z = (-0+sqrt delta(a,0,c))/(2*a) or z = (-0-sqrt delta(a,0,c))/(2*a) or z = 0 or z = 0/(2*a) by A1,Th1; hence thesis; end; theorem 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 proof assume that A1: a<>0 & delta(a,b,c)>=0 and A2: Polynom(a,b,c,0,z)=0; (a*z^2+b*z+c)*z = 0 by A2; then Polynom(a,b,c,z) = 0 or z = 0; hence thesis by A1,Th1; end; theorem 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 proof assume that A1: a<>0 & delta(a,b,c)<0 and A2: Polynom(a,b,c,0,z)=0; (a*z^2+b*z+c)*z = 0 by A2; then Polynom(a,b,c,z) = 0 or z = 0; hence thesis by A1,Th2; end; theorem Th12: y^2 = a implies y = sqrt a or y = -sqrt a proof assume A1: y^2 = a; then A2: a >= 0 by XREAL_1:63; Polynom(1,0,-a,y) =0 by A1; then y=(-0+sqrt delta(1,0,-a))/(2*1) or y=(-0-sqrt delta(1,0,-a))/(2*1) by A2 ,POLYEQ_1:5; then y=(sqrt (4*a))/2 or y=(0-sqrt (4*a))/2; then y= sqrt a * 2 /2 or y=(-(2 * sqrt a))/2 by A2,SQUARE_1:20,29; hence thesis; end; theorem 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)) proof assume A1: a <> 0; set y=Im z; set x=Re z; assume that A2: Im z = 0 and A3: Polynom(a,0,c,d,z)=0; A4: a = a+0*; 0 = a*(Re z^3+(Im z^3)*)+0*z^2+c*z+d by A3,COMPLEX1:13 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*) +0*z^2+c*z+d by Th5 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*) +c*z+d by Th5 .= (a+0*)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) +c*(Re z+Im z*) +d by COMPLEX1:13 .=Re a *Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)-Im a *Im((x|^ 3 - 3*x *y^2)+(-y|^ 3+3*x^2*y)*)+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a)* +c*(Re z+Im z*)+d by COMPLEX1:82 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)* ))+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+( -y|^ 3+3*x^2*y)*)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a*(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*x *y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a*(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*x *y^2)+(-y|^ 3+3*x^2*y)*)+ (x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y )+ (x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y)+ ( x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0*(-y|^ 3+3*x^2*y))+( Re a*(-y|^ 3+3*x^2*y)+(x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*0 )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .= a*(x|^ 3 - 0)+c*x+d+(a*(-0))* by A2,NEWTON:11 .= a*x|^ 3 +c*x+d; then a"*(a*x|^ 3+c*x+d) = a"*0; then x|^ 3*(a/a)+a"*c*x+a"*d = 0; then A5: Polynom(1,0,c/a,d/a,x) = 0 by A1,XCMPLX_1:88; A6: (d/a)^2/4 =1/4*(d^2/a^2) by XCMPLX_1:76 .=d^2/(a^2*4) by XCMPLX_1:103; let u,v; assume A7: Re z=u+v & 3*v*u+c/a=0; A8: -(d/a)/2 = -1/2*(d/a) .= -d/(a*2) by XCMPLX_1:103; A9: (c/a)/3 =1/3*(c/a) .=c/(a*3) by XCMPLX_1:103; z = Re z+(Im z)* by COMPLEX1:13 .= x by A2; hence thesis by A7,A5,A8,A6,A9,POLYEQ_1:19; end; theorem 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)* proof assume A1: a <> 0; set y=Im z; set x=Re z; assume that A2: Im z <> 0 and A3: Polynom(a,0,c,d,z)=0; A4: a = a+0*; A5: 0 = a*(Re z^3+(Im z^3)*)+0*z^2+c*z+d by A3,COMPLEX1:13 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*) +c*z+d by Th5 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*) +c*z+d by Th5 .= (a+0*)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) +c*(Re z+(Im z)* )+d by COMPLEX1:13 .=Re a *Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)-Im a *Im((x|^ 3 - 3*x *y^2)+(-y|^ 3+3*x^2*y)*)+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a)* +c*(Re z+Im z *)+d by COMPLEX1:82 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)* ))+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+( -y|^ 3+3*x^2*y)*)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3* x*y^2)+(-y|^ 3+3*x^2*y)*)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a ) * +c*(Re z+Im z *)+d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3* x*y^2)+(-y|^ 3+3*x^2*y)*)+ (x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+ d by COMPLEX1:12 .=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y )+ (x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y)+ ( x|^ 3 - 3*x*y^2)*Im a)* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0*(-y|^ 3+3*x^2*y))+( Re a*(-y|^ 3+3*x^2*y)+(x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*Im a )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*0 )* +c*(Re z+Im z *)+d by A4,COMPLEX1:12 .= a*(x|^ 3 - 3*x*y^2)+c*x+d+(a*(-y|^ 3+3*x^2*y) +c*y+0)*; then a*(-y|^(2+1)+3*x^2*y)+c*y = 0 by COMPLEX1:4,12; then a*(-y|^2*y+3*x^2*y)+c*y = 0 by NEWTON:6; then (a*(-y|^2+3*x^2)+c+0)*y = 0; then (a*(y|^2))+(-a*(y|^2)+(a*(3*x^2)+c))=(a*(y|^2))+0 by A2,XCMPLX_1:6; then y|^(1+1) = (a*(3*x^2)+c)/a by A1,XCMPLX_1:89; then y|^1*y = (a*(3*x^2)+c)/a by NEWTON:6; then A6: y^2 = (3*x^2)*a/a+c/a+0/a; then A7: z = x+y* & y^2 = 3*x^2+c/a+0*a" by A1,COMPLEX1:13,XCMPLX_1:89; set q = -d/(8*a); set pp = c/(4*a); let u,v; set m = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3)); set n = 3-root(-q/2-sqrt(q^2/4+(pp/3) |^ 3)); A8: (c/(4*a))/3=1/3*(c/(4*a)) .=c/(a*4*3) by XCMPLX_1:103 .=c/(a*(4*3)); -q/2=1/2*(d/(8*a)); then A9: -q/2=d/(a*8*2) by XCMPLX_1:103; a*(-y|^ 3+3*x^2*y) +c*y+0 = 0 by A5,COMPLEX1:4,12; then a*(x|^ 3 - 3*x*(3*x^2+c/a)+0)+c*x+d = 0 by A1,A5,A6,XCMPLX_1:89; then 0 =a*x|^ 3 - a*(9*(x*x^2)+(3*x)*(c/a))+c*x+d .=a*x|^ 3 - a*(9*(x|^1*x*x)+(3*x)*(c/a))+c*x+d .=a*x|^ 3 - a*(9*(x|^(1+1)*x)+(3*x)*(c/a))+c*x+d by NEWTON:6 .=a*x|^ 3 - a*(9*(x|^(2+1))+(3*x)*(c/a)+0)+c*x+d by NEWTON:6 .=a*x|^ 3 - (a*(9*(x|^3))+(3*x)*(c*(a/a)))+c*x+d .=a*x|^ 3 - (a*(9*(x|^3))+(3*x)*c)+c*x+d by A1,XCMPLX_1:88 .=(-8*a)*x|^3+(-2*c)*x+d; then (-1)*0=(8*a)*x|^3+(2*c)*x+(-d); then 0=x|^3*((8*a)/(8*a))+(8*a)"*((2*c)*x)+(8*a)"*(-d); then 0=1*x|^3+0*x^2+((2*c)/(8*a))*x+((8*a)"*(-d)) by A1,XCMPLX_1:88; then 0=1*x|^3+0*x^2+((2/8*c)/a)*x+((-d)/(8*a)) by XCMPLX_1:83; then 0=1*x|^3+0*x^2+(1/a*(c/4))*x+((-d)/(8*a)); then A10: Polynom(1,0,c/(4*a),-d/(8*a),x) = 0 by XCMPLX_1:103; assume Re z=u+v & 3*v*u+c/(4*a)=0; then A11: x = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(pp/3 ) |^ 3)) or x = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2+sqrt(q^2/4+( pp/3) |^ 3)) or x = 3-root(-q/2-sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2-sqrt(q^2 /4+(pp/3) |^ 3)) by A10,POLYEQ_1:19; A12: now per cases by A11; case x = m + n; hence z=m+n+sqrt(3*(m + n )^2+c/a)* or z=m+n+(-sqrt(3*(m + n )^2+c/a)) * by A7,Th12; end; case x = 2*m; hence z=2*m+sqrt(3*(2*m)^2+c/a)* or z=2*m+(-sqrt(3*(2*m)^2+c/a))* by A7,Th12; end; case x = 2*n; hence z=2*n+sqrt(3*(2*n )^2+c/a)* or z=2*n+(-sqrt(3*(2*n )^2+c/a))* by A7,Th12; end; end; q^2/4=(1/2*(d/(8*a)))^2; hence thesis by A9,A12,A8; end; theorem 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* proof assume A1: a<>0; set p = (3*a*c-b^2)/(3*a^2); set b9=c/a; A2: a = a+0*; set q = 2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2); set c9=d/a; set a9=b/a; set y=Im z; set x=Re z; assume that A3: Polynom(a,b,c,d,z)=0 and A4: Im z=0; A5: z = x + y* by COMPLEX1:13; 0 = a*(Re z^3+(Im z^3)*)+b*z^2+c*z+d by A3,COMPLEX1:13 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*) +b*z^2+c*z+d by Th5 .= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*) +b*z^2+c*z+d by Th5 .= (a+0*)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) +b*z^2+c*(Re z+Im z *)+d by COMPLEX1:13 .= Re a*Re ((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) -Im a*Im((x|^ 3 - 3* x*y^2)+(-y|^ 3+3*x^2*y)*)+ (Re a*Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) +Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a)* +b*z^2+c*(Re z+Im z *) +d by COMPLEX1:82 .= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) -0*Im((x|^ 3 - 3*x*y ^2)+(-y|^ 3+3*x^2*y)*))+( Re a*Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) + Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*Im a )* +b*z^2+c*(Re z+Im z *) +d by A2,COMPLEX1:12 .= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) -0)+(Re a*Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) +Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*)*0 )* +b*z^2+c*(Re z+Im z *)+d by A2,COMPLEX1:12 .= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*) -0)+(Re a*(-y|^ 3+3* x^2*y)+0 )* +b*z^2+c*(Re z+Im z *)+d by COMPLEX1:12 .= (Re a*(x|^ 3 - 3*x*y^2)-0)+(Re a*(-y|^ 3+3*x^2*y))* +b*z^2+c*(Re z +Im z *)+d by COMPLEX1:12 .= (a*(x|^ 3 - 3*x*y^2)-0)+(Re a*(-y|^ 3+3*x^2*y))* +b*z^2+c*(Re z+Im z *)+d by A2,COMPLEX1:12 .= a*(x|^ 3 - 3*x*y^2)+(a*(-y|^ 3+3*x^2*y))* +b*(x^2-y^2+(2*x*y)*) +(c*x+(c*y)*)+d by A2,A5,COMPLEX1:12; then 0 = a*(x|^ 3 - 3*x*0)+b*(x^2-0)+c*x+d +(a*(-0|^ 3+0)+b*0+0)* by A4 .= (a*x|^ 3+b*x^2+c*x+d)+(a*0+0)* by NEWTON:11; then A6: Polynom(a,b,c,d,x) = 0; A7: c9=d/a; p/3=1/3*((3*a*c-b^2)/(3*a^2)); then A8: p/3=(3*a*c-b^2)/(a^2*3*3) by XCMPLX_1:103; A9: -q/2=-((b/(3*a)) |^ 3+1/2*((3*a*d-b*c)/(3*a^2))) .=-((b/(3*a)) |^ 3+(3*a*d-b*c)/(a^2*3*2)) by XCMPLX_1:103 .=-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2); let u,v,x1; assume that A10: x1=Re z +b/(3*a) & Re z=u+v-b/(3*a) and A11: 3*u*v+(3*a*c-b^2)/(3*a^2)=0; a9=b/a & b9=c/a; then Polynom(1,0,p,q,x1) = 0 by A1,A10,A6,A7,POLYEQ_1:16; then x1 = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) or x1 = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2+sqrt(q^2/4+(p/ 3) |^ 3)) or x1 = 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+ (p/3) |^ 3)) by A10,A11,POLYEQ_1:19; hence thesis by A4,A10,A8,A9,COMPLEX1:13; end; theorem Th16: z1 <> 0 & Polynom(z1,z2,z) = 0 implies z = -(z2/z1) proof assume z1 <> 0 & Polynom(z1,z2,z) = 0; then z = (-z2)*z1" by XCMPLX_1:203; hence thesis; end; begin theorem (for z holds Polynom(z1,z2,z3,z) = Polynom(s1,s2,s3,z)) implies z1 = s1 & z2 = s2 & z3 = s3 proof assume A1: for z holds Polynom(z1,z2,z3,z) = Polynom(s1,s2,s3,z); then A2: Polynom(z1,z2,z3,-1r) = Polynom(s1,s2,s3,-1r); Polynom(z1,z2,z3,0c) = Polynom(s1,s2,s3,0c) & Polynom(z1,z2,z3,1r) = Polynom (s1,s2,s3,1r) by A1; hence thesis by A2,COMPLEX1:def 4; end; theorem (-a+sqrt (a^2+b^2))/2 >=0 & (a+sqrt (a^2+b^2))/2>=0 proof A1: b^2>=0 by XREAL_1:63; A2: a^2>=0 by XREAL_1:63; then A3: sqrt (a^2+b^2)>=0 by A1,SQUARE_1:def 2; a^2+b^2>=0+a^2 by A1,XREAL_1:7; then A4: sqrt(a^2+b^2)>=sqrt(a^2) by A2,SQUARE_1:26; per cases; suppose A5: a>=0; then sqrt(a^2+b^2)>=a by A4,SQUARE_1:22; then sqrt(a^2+b^2)-a>=a-a by XREAL_1:9; hence thesis by A3,A5; end; suppose A6: a<0; then sqrt(a^2+b^2) >= -a by A4,SQUARE_1:23; then sqrt(a^2+b^2)-(-a) >= -a-(-a) by XREAL_1:9; hence thesis by A3,A6; end; end; theorem Th19: 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))* proof set a=Re s; set b=Im s; set u=Re z; set v=Im z; A1: z = u+v* by COMPLEX1:13; assume z^2=s; then A2: u^2-v^2+2*u*v* =a+b* by A1,COMPLEX1:13; assume Im s >=0; then A3: u<=0 & v<=0 or u>=0 & v>=0 by A2,COMPLEX1:77; A4: u^2>=0 & v^2>=0 by XREAL_1:63; A5: u^2-v^2=a by A2,COMPLEX1:77; then (u^2+v^2)^2=a^2+b^2 by A2; then u^2+v^2=sqrt (a^2+b^2) by A4,SQUARE_1:22; then -u=sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/ 2) or u= sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) by A5,A3, SQUARE_1:22,23; hence thesis by COMPLEX1:13; end; theorem z^2 = s & Im s = 0 & Re s > 0 implies z=sqrt(Re s) or z=-sqrt(Re s) proof assume A1: z^2=s; assume that A2: Im s =0 and A3: Re s >0; z=sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+0))/2 ))* or z=-sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+ 0^2))/2))* by A1,A2,Th19; then z=sqrt (( Re s+Re s)/2)+ sqrt ((-Re s+sqrt ((Re s)^2+0))/2)* or z=- sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ -sqrt ((-Re s+sqrt ((Re s)^2+0))/2)* by A3,SQUARE_1:22; then z=sqrt (( Re s+Re s)/2)+ sqrt ((-Re s+Re s)/2)* or z=-sqrt (( Re s+Re s)/2) + -sqrt ((-Re s+sqrt ((Re s)^2+0))/2)* by A3,SQUARE_1:22; then z=sqrt (Re s)+ sqrt ((0+(Re s-Re s))/2)* or z=-sqrt (Re s)+-sqrt ((0+ (Re s-Re s))/2)* by A3,SQUARE_1:22; hence thesis by SQUARE_1:17; end; theorem z^2 = s & Im s = 0 & Re s < 0 implies z= sqrt (-Re s)* or z= -sqrt (-Re s)* proof assume A1: z^2=s; assume that A2: Im s =0 and A3: Re s < 0; z=sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+0))/2 ))* or z=-sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+ 0^2))/2))* by A1,A2,Th19; then z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+sqrt ((Re s)^2+0))/2)* or z=- sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+0))/2))* by A3,SQUARE_1:23; then z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+-Re s)/2)* or z=-sqrt (( Re s+ -Re s)/2)+(-sqrt ((-Re s+sqrt ((Re s)^2+0))/2))* by A3,SQUARE_1:23; then z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+-Re s)/2)* or z=-sqrt (( Re s+ -Re s)/2)+(-sqrt ((-Re s+-Re s)/2))* by A3,SQUARE_1:23; hence thesis by SQUARE_1:17; end; theorem 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))* proof assume A1: z^2=s; set v=Im z; set u=Re z; set b=Im s; set a=Re s; z = u + v* by COMPLEX1:13; then A2: s=a+b* & z^2 = u^2-v^2 + 2*u*v* by COMPLEX1:13; assume Im s<0; then 2*(u*v)<0 by A1,A2,COMPLEX1:77; then u*v<0; then A3: u<0 & v>0 or u>0 & v<0 by XREAL_1:133; A4: u^2>=0 & v^2>=0 by XREAL_1:63; A5: u^2-v^2=a by A1,A2,COMPLEX1:77; then sqrt (u^2+v^2)^2=sqrt (a^2+b^2) by A1,A2; then u^2+v^2=sqrt (a^2+b^2) by A4,SQUARE_1:22; then -u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) or u= sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/2) by A5,A3, SQUARE_1:22,23; hence thesis by COMPLEX1:13; end; theorem Th23: 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))* proof set a=Re s; set b=Im s; set u=Re z; set v=Im z; A1: u^2>=0 & v^2>=0 by XREAL_1:63; z = u + v* by COMPLEX1:13; then A2: s=a+b* & z^2 = u^2-v^2 + 2*u*v* by COMPLEX1:13; assume A3: z^2=s; then A4: u^2-v^2=a by A2,COMPLEX1:77; then sqrt (u^2+v^2)^2=sqrt (a^2+b^2) by A3,A2; then A5: u^2+v^2=sqrt (a^2+b^2) by A1,SQUARE_1:22; per cases; suppose b>=0; then u<=0 & v<=0 or u>=0 & v>=0 by A3,A2,COMPLEX1:77; then -u=sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/ 2) or u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) by A4,A5, SQUARE_1:22,23; hence thesis by COMPLEX1:13; end; suppose b<0; then 2*(u*v)<0 by A3,A2,COMPLEX1:77; then u*v<0; then u<0 & v>0 or u>0 & v<0 by XREAL_1:133; then -u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) or u= sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/2) by A4,A5, SQUARE_1:22,23; hence thesis by COMPLEX1:13; end; end; theorem z1<>0 & Polynom(z1,z2,0,z)=0 implies z=-(z2/z1) or z=0 proof assume that A1: z1<>0 and A2: Polynom(z1,z2,0,z)=0; 0 =(z1*z+z2)*z by A2; then Polynom(z1,z2,z) = 0 or z=0; hence thesis by A1,Th16; end; theorem Th25: 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))* proof assume z1<>0 & Polynom(z1,0,z3,z)=0; then A1: z^2=(-z3)/z1 by XCMPLX_1:89; let s; assume s=-(z3/z1); hence thesis by A1,Th23; end; theorem Th26: 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 proof assume that A1: z1<>0 and A2: Polynom(z1,z2,z3,z)=0; (z1*z^2+z2*z+z3)/z1=0 by A2; then (z^2*z1)/z1+(z2*z)/z1+z3/z1=0; then z^2+(z2/z1)*z+z3/z1=0 by A1,XCMPLX_1:89; then z^2+2*z2/(2*z1)*z+z3/z1=0 by XCMPLX_1:91; then A3: (z+(z2/(2*z1)))^2-((z2/(2*z1))^2-z3/z1)=0; let h,t; assume h=(z2/(2*z1))^2-z3/z1 & t=z2/(2*z1); then z+t-t= 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+t-t=-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+t-t= 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+t-t=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*-t by A3,Th23; hence thesis; end; theorem z|^ 3=z*z*z & z|^ 3=z^2*z & z|^ 3 = z^3 proof z|^ 3 = z|^(2+1) .= z|^(1+1)*z by NEWTON:6 .= z|^1*z*z by NEWTON:6 .= z*z*z; hence thesis; end; theorem z1<>0 & Polynom(z1,z2,0,0,z)=0 implies z=-z2/z1 or z=0 proof assume that A1: z1<>0 and A2: Polynom(z1,z2,0,0,z)=0; 0 =(z1*z +z2)*z^2 by A2; then Polynom(z1,z2,z)=0 or 1*z^2+0*z+0=0; hence thesis by A1,Th16; end; theorem 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))* proof assume that A1: z1<>0 and A2: Polynom(z1,0,z3,0,z)=0; let s; 0 =(z1*z^2+z3)*z by A2; then A3: Polynom(z1,0,z3,z)=0 or z=0; assume s=-(z3/z1); hence thesis by A1,A3,Th25; end; theorem 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 proof assume that A1: z1<>0 and A2: Polynom(z1,z2,z3,0,z)=0; let s,h,t; 0 =Polynom(z1,z2,z3,z)*z by A2; then A3: z=0 or Polynom(z1,z2,z3,z)=0; assume h=(z2/(2*z1))^2-z3/z1 & t=z2/(2*z1); hence thesis by A1,A3,Th26; end; Lm2: for n be Nat st n>0 holds 0 |^ n = 0 proof let n be Nat; assume n>0; then n >= 0+1 by NAT_1:13; hence thesis by NEWTON:11; end; theorem Th31: for x being Real, n be Nat holds (cos x + sin x*) |^ n = cos (n*x) + sin (n*x)* proof let x be Real; defpred P[Nat] means (cos x +sin x*)|^ \$1 = cos (\$1*x)+sin (\$1*x)*; A1: now let n be Nat; assume P[n]; then (cos x + sin x*) |^ (n+1) = (cos(n*x)+sin(n*x)*)*(cos x+(sin x)* ) by NEWTON:6 .= cos(n*x)*cos x - sin(n*x)*sin x+ (cos(n*x)*sin x+cos x*sin(n*x))* .= cos(n*x+x)+(cos(n*x)*sin x+cos x*sin(n*x))* by SIN_COS:75 .= cos((n+1)*x)+sin((n+1)*x)* by SIN_COS:75; hence P[n+1]; end; A2: P[0] by NEWTON:4,SIN_COS:31; thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1); end; theorem 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)* proof let z be Element of COMPLEX; let n be Element of NAT; z|^ n =(|.z.|*cos Arg z-0*sin Arg z+(|.z.|*sin Arg z+cos Arg z*0)*) |^ n by COMPTRIG:62 .=(|.z.|*(cos Arg z+sin Arg z*))|^ n .= |.z.||^ n*(cos Arg z+sin Arg z*)|^ n by NEWTON:7; hence z|^ n = (|.z.| to_power n)*(cos (n*Arg z)+sin (n*Arg z)*) by Th31 .= (|.z.| to_power n)*cos(n*Arg z)+(|.z.| to_power n)*sin(n*Arg z)*; end; theorem Th33: 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)* proof let n,k be Element of NAT,x be Real; assume A1: n <> 0; thus (cos((x+2*PI*k)/n)+ sin((x+2*PI*k)/n)*)|^ n = cos (n*((x+2*PI*k)/n)) +sin (n*((x+2*PI*k)/n))* by Th31 .= cos(x+2*PI*k)+sin(n*((x+2*PI*k)/n))* by A1,XCMPLX_1:87 .= cos(x+2*PI*k)+sin(x+2*PI*k)* by A1,XCMPLX_1:87 .= cos.(x+2*PI*k)+sin(x+2*PI*k)* by SIN_COS:def 19 .= cos.(x+2*PI*k)+(sin.(x+2*PI*k))* by SIN_COS:def 17 .= cos.(x+2*PI*k)+(sin.x)* by SIN_COS2:10 .= cos.x + (sin.x)* by SIN_COS2:11 .= cos.x + (sin x)* by SIN_COS:def 17 .= cos x + (sin x)* by SIN_COS:def 19; end; theorem Th34: 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 proof let z be Complex; let n,k be Element of NAT; assume A1: n <> 0; then A2: n >= 0+1 by NAT_1:13; per cases; suppose z <> 0; then A3: |.z.| > 0 by COMPLEX1:47; thus ((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI *k)/n)*)|^ n = ((n-root |.z.|)* (cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*k)/n) *))|^ n .= ((n-root |.z.|)|^ n) *((cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*k)/n) *)|^ n) by NEWTON:7 .= ((n-root |.z.|)|^ n)*(cos Arg z+(sin Arg z)*) by A1,Th33 .= |.z.|*(cos Arg z+(sin Arg z)*) by A1,A3,COMPTRIG:4 .= |.z.|*cos Arg z-0*sin Arg z+(|.z.|*sin Arg z+0*cos Arg z)* .= z by COMPTRIG:62; end; suppose A4: z = 0; hence ((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI *k)/n)*)|^ n =((0*cos((Arg z+2*PI*k)/n)+ (n-root 0)*sin((Arg z+2*PI*k)/n)* )|^ n) by A2,COMPLEX1:44,POWER:5 .= (0*sin((Arg z+2*PI*k)/n)*)|^ n by A2,POWER:5 .= z by A1,A4,Lm2; end; end; theorem 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 proof let z be Element of COMPLEX, n be non zero Element of NAT,k be Element of NAT; ((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI*k) /n)*)|^ n=z by Th34; hence thesis by COMPTRIG:def 2; end; theorem for z be Complex, v be CRoot of 1,z holds v = z proof let z be Complex, v be CRoot of 1,z; v|^ 1 = z by COMPTRIG:def 2; hence thesis; end; theorem for n be non zero Nat, v be CRoot of n,0 holds v = 0 proof let n be non zero Nat, v be CRoot of n,0; defpred P[Nat] means v|^ \$1 = 0; A1: now let k be non zero Nat; assume that A2: k <> 1 and A3: P[k]; consider t be Nat such that A4: k = t+1 by NAT_1:6; t <> 0 by A2,A4; then reconsider t as non zero Nat; take t; thus t < k by A4,NAT_1:13; v|^ k = (v|^ t)*v by A4,NEWTON:6; then v|^ t = 0 or v = 0 by A3; hence P[t] by Lm2; end; A5: ex n be non zero Nat st P[n] proof take n; thus thesis by COMPTRIG:def 2; end; P[1] from COMPTRIG:sch 1(A5,A1); hence thesis; end; theorem for n be non zero Element of NAT, z be Complex for v be CRoot of n,z st v = 0 holds z = 0 proof let n be non zero Element of NAT, z be Complex; let v be CRoot of n,z; assume v = 0; then 0|^ n = z by COMPTRIG:def 2; hence thesis by Lm2; end; theorem 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 proof let n be non zero Element of NAT,k be Element of NAT; (cos(2*PI*k/n)+sin(2*PI*k/n)*)|^n =cos(n*((2*PI*k)/n))+sin(n*((2*PI*k )/n))* by Th31 .=cos(2*PI*k)+(sin(n*((2*PI*k)/n)))* by XCMPLX_1:87 .=cos(2*PI*k+0)+(sin(2*PI*k+0))* by XCMPLX_1:87 .=cos.(2*PI*k+0)+(sin(2*PI*k+0))* by SIN_COS:def 19 .=cos.(2*PI*k+0)+(sin.(2*PI*k+0))* by SIN_COS:def 17 .=cos.(2*PI*k+0)+(sin.0)* by SIN_COS2:10 .=1 by SIN_COS:30,SIN_COS2:11; hence thesis by COMPTRIG:def 2; end; theorem 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.| proof let z,s be Element of COMPLEX, n be Element of NAT; assume that A1: s<>0 and A2: z<>0 and A3: n>=1 and A4: s|^ n=z|^ n; z|^ n = (|.s.|*cos Arg s + |.s.|*sin Arg s *)|^ n by A4,COMPTRIG:62 .=(|.s.|*(cos Arg s+sin Arg s *))|^ n .=(|.s.||^ n)*((cos Arg s+sin Arg s *)|^ n) by NEWTON:7 .=(|.s.| to_power n)*(cos (n*Arg s)+sin (n*Arg s)*) by Th31 .= ((|.s.| to_power n)*cos (n*Arg s) )+((|.s.| to_power n)*sin (n*Arg s) )*; then A5: ((|.s.| to_power n)*cos (n*Arg s)) +((|.s.| to_power n)*sin (n*Arg s ))* = (|.z.|*cos Arg z + |.z.|*sin Arg z *)|^ n by COMPTRIG:62 .=(|.z.|*(cos Arg z+sin Arg z *))|^ n .=(|.z.||^ n)*((cos Arg z+sin Arg z *)|^ n) by NEWTON:7 .=(|.z.| to_power n)*(cos (n*Arg z)+sin (n*Arg z)*) by Th31 .= ((|.z.| to_power n)*cos (n*Arg z))+((|.z.| to_power n) *sin (n*Arg z) )*; then (|.s.| to_power n)*cos (n*Arg s)=(|.z.| to_power n)*cos (n*Arg z) by COMPLEX1:77; then (|.s.| to_power n) ^2*(cos (n*Arg s))^2+ ((|.s.| to_power n)*sin (n*Arg s))^2 =((|.z.| to_power n)*cos (n*Arg z))^2+ ((|.z.| to_power n)*sin (n*Arg z)) ^2 by A5,SQUARE_1:9; then (|.s.| to_power n) ^2*((cos (n*Arg s))^2+(sin (n*Arg s))^2) =((|.z.| to_power n))^2*((cos (n*Arg z))^2+(sin (n*Arg z))^2); then (|.s.| to_power n) ^2*((cos (n*Arg s))^2+(sin (n*Arg s))^2) =((|.z.| to_power n))^2*1 by SIN_COS:29; then A6: (|.s.| to_power n) ^2*1=((|.z.| to_power n))^2 by SIN_COS:29; A7: |.s.|>0 by A1,COMPLEX1:47; then |.s.| to_power n > 0 by POWER:34; then A8: (|.s.| to_power n) =sqrt ((|.z.| to_power n))^2 by A6,SQUARE_1:22; A9: |.z.|>0 by A2,COMPLEX1:47; then |.z.| to_power n > 0 by POWER:34; then |.s.| |^ n=|.z.| |^ n by A8,SQUARE_1:22; then |.s.| = n-root (|.z.| |^ n) by A3,A7,POWER:4; hence thesis by A3,A9,POWER:4; end;