:: 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-2012 Association of Mizar Users begin definition let z be Element of COMPLEX ; :: original:^2 redefine funcz ^2 -> Element of COMPLEX equals :: POLYEQ_3:def 1 (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ); compatibility for b1 being Element of COMPLEX holds ( b1 = z ^2 iff b1 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ) ) proofend; correctness coherence z ^2 is Element of COMPLEX ; by XCMPLX_0:def_2; end; :: deftheorem defines ^2 POLYEQ_3:def_1_:_ for z being Element of COMPLEX holds z ^2 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ); definition let a, b, c be Real; let z be Element of COMPLEX ; :: original:Polynom redefine func Polynom (a,b,c,z) -> Element of COMPLEX ; coherence Polynom (a,b,c,z) is Element of COMPLEX by XCMPLX_0:def_2; end; theorem Th1: :: POLYEQ_3:1 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) holds z = - (b / (2 * a)) proofend; theorem Th2: :: POLYEQ_3:2 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) holds z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) proofend; theorem :: POLYEQ_3:3 for b, c being Real for z being Element of COMPLEX st b <> 0 & ( for z being Element of COMPLEX holds Polynom (0,b,c,z) = 0 ) holds z = - (c / b) proofend; theorem :: POLYEQ_3:4 for a, b, c being Real for z, z1, z2 being complex number st a <> 0 & ( for z being complex number holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) holds ( b / a = - (z1 + z2) & c / a = z1 * z2 ) proofend; definition let z be complex number ; funcz ^3 -> Element of COMPLEX equals :: POLYEQ_3:def 2 (z ^2) * z; correctness coherence (z ^2) * z is Element of COMPLEX ; ; end; :: deftheorem defines ^3 POLYEQ_3:def_2_:_ for z being complex number holds z ^3 = (z ^2) * z; Lm1: for z being complex number holds z |^ 2 = z * z proofend; definition let a, b, c, d, z be complex number ; redefine func Polynom (a,b,c,d,z) equals :: POLYEQ_3:def 3 (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d; compatibility for b1 being set holds ( b1 = Polynom (a,b,c,d,z) iff b1 = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d ) proofend; end; :: deftheorem defines Polynom POLYEQ_3:def_3_:_ for a, b, c, d, z being complex number holds Polynom (a,b,c,d,z) = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d; theorem Th5: :: POLYEQ_3:5 for z being Element of COMPLEX holds ( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) ) proofend; theorem :: POLYEQ_3:6 for a, b, c, d, a9, b9, c9, d9 being Real st ( for z being complex number holds Polynom (a,b,c,d,z) = Polynom (a9,b9,c9,d9,z) ) holds ( a = a9 & b = b9 & c = c9 & d = d9 ) proofend; theorem :: POLYEQ_3:7 for b, c, d being Real for z being Element of COMPLEX st b <> 0 & delta (b,c,d) >= 0 & Polynom (0,b,c,d,z) = 0 & not z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) & not z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) holds z = - (c / (2 * b)) proofend; theorem :: POLYEQ_3:8 for b, c, d being Real for z being Element of COMPLEX st b <> 0 & delta (b,c,d) < 0 & Polynom (0,b,c,d,z) = 0 & not z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) holds z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) proofend; theorem :: POLYEQ_3:9 for a, c being Real for z being Element of COMPLEX st a <> 0 & (4 * a) * c <= 0 & Polynom (a,0,c,0,z) = 0 & not z = (sqrt (- ((4 * a) * c))) / (2 * a) & not z = (- (sqrt (- ((4 * a) * c)))) / (2 * a) holds z = 0 proofend; theorem :: POLYEQ_3:10 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,0,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & not z = - (b / (2 * a)) holds z = 0 proofend; theorem :: POLYEQ_3:11 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,0,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) holds z = 0 proofend; theorem Th12: :: POLYEQ_3:12 for y, a being Real holds ( not y ^2 = a or y = sqrt a or y = - (sqrt a) ) proofend; theorem :: POLYEQ_3:13 for a, c, d being Real for z being Element of COMPLEX st a <> 0 & Im z = 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not 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))))) & not 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))))) 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))))) proofend; theorem :: POLYEQ_3:14 for a, c, d being Real for z being Element of COMPLEX st a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not 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))) * ) & not 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))) * ) & not 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))) * ) & not 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))) * ) & not 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))) * ) holds 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))) * ) proofend; theorem :: POLYEQ_3:15 for a, b, c, d being Real for z being Element of COMPLEX st a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 holds for u, v, x1 being Real 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 & not 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 * ) & not 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 * ) 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 * ) proofend; theorem Th16: :: POLYEQ_3:16 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z) = 0 holds z = - (z2 / z1) proofend; begin theorem :: POLYEQ_3:17 for z1, z2, z3, s1, s2, s3 being Element of COMPLEX st ( for z being Element of COMPLEX holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ) holds ( z1 = s1 & z2 = s2 & z3 = s3 ) proofend; theorem :: POLYEQ_3:18 for a, b being Real holds ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) proofend; theorem Th19: :: POLYEQ_3:19 for z, s being Element of COMPLEX st z ^2 = s & Im s >= 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) holds z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) proofend; theorem :: POLYEQ_3:20 for z, s being Element of COMPLEX st z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) holds z = - (sqrt (Re s)) proofend; theorem :: POLYEQ_3:21 for z, s being Element of COMPLEX st z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * holds z = - ((sqrt (- (Re s))) * ) proofend; theorem :: POLYEQ_3:22 for z, s being Element of COMPLEX st z ^2 = s & Im s < 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) holds z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) proofend; theorem Th23: :: POLYEQ_3:23 for z, s being Element of COMPLEX holds ( not z ^2 = s 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)) * ) ) proofend; theorem :: POLYEQ_3:24 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,0,z) = 0 & not z = - (z2 / z1) holds z = 0 proofend; theorem Th25: :: POLYEQ_3:25 for z1, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,0,z3,z) = 0 holds for s being Element of COMPLEX holds ( not s = - (z3 / z1) 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)) * ) ) proofend; theorem Th26: :: POLYEQ_3:26 for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z3,z) = 0 holds for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t 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 proofend; theorem :: POLYEQ_3:27 for z being Element of COMPLEX holds ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 ) proofend; theorem :: POLYEQ_3:28 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,0,0,z) = 0 & not z = - (z2 / z1) holds z = 0 proofend; theorem :: POLYEQ_3:29 for z1, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,0,z3,0,z) = 0 holds for s being Element of COMPLEX holds ( not s = - (z3 / z1) or 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)) * ) ) proofend; theorem :: POLYEQ_3:30 for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 holds for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t 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 proofend; Lm2: for n being Nat st n > 0 holds 0 |^ n = 0 proofend; theorem Th31: :: POLYEQ_3:31 for x being real number for n being Element of NAT holds ((cos x) + ((sin x) * )) |^ n = (cos (n * x)) + ((sin (n * x)) * ) proofend; 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)))) * ) proofend; theorem Th33: :: POLYEQ_3:33 for n, k being Element of NAT for x being Real st n <> 0 holds ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) proofend; theorem Th34: :: POLYEQ_3:34 for z being complex number for n, k being 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 proofend; theorem :: POLYEQ_3:35 for z being Element of COMPLEX for n being non empty Element of NAT for k being 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 proofend; theorem :: POLYEQ_3:36 for z being complex number for v being CRoot of 1,z holds v = z proofend; theorem :: POLYEQ_3:37 for n being non empty Nat for v being CRoot of n, 0 holds v = 0 proofend; theorem :: POLYEQ_3:38 for n being non empty Element of NAT for z being complex number for v being CRoot of n,z st v = 0 holds z = 0 proofend; theorem :: POLYEQ_3:39 for n being non empty Element of NAT for k being Element of NAT holds (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * ) is CRoot of n,1 proofend; theorem :: POLYEQ_3:40 for z, s being Element of COMPLEX for n being Element of NAT st s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n holds |.s.| = |.z.| proofend;