:: 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

definition

let z be Element of COMPLEX ;

:: original: ^2
redefine func z ^2 -> Element of COMPLEX equals :: POLYEQ_3:def 1
(((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>);

compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z ^2 iff b₁ = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>) )

proof end;

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))) * <i>);

definition

let a, b, c be Real;
let z be 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;

:: deftheorem POLYEQ_3:def 2 :
canceled;

theorem Th1: :: POLYEQ_3:1

for a, b, c being Real
for z being 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))

proof end;

theorem Th2: :: POLYEQ_3:2

for a, b, c being Real
for z being 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)) * <i>) holds
z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>)

proof end;

theorem :: POLYEQ_3:3

for b, c being Real
for z being Complex st b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) holds
z = - (c / b)

proof end;

theorem :: POLYEQ_3:4

for a, b, c being Real
for 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 end;

definition

let z be Complex;

func z ^3 -> Element of COMPLEX equals :: POLYEQ_3:def 3
(z ^2) * z;

correctness
coherence
(z ^2) * z is Element of COMPLEX ;
by XCMPLX_0:def 2;

end;

:: deftheorem defines ^3 POLYEQ_3:def 3 :
for z being Complex holds z ^3 = (z ^2) * z;

Lm1: for z being Complex holds z |^ 2 = z * z

proof 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;

compatibility
for b₁ being set holds
( b₁ = Polynom (a,b,c,d,z) iff b₁ = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d )

proof end;

end;

:: deftheorem defines Polynom POLYEQ_3:def 4 :
for a, b, c, d, z being Complex holds Polynom (a,b,c,d,z) = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d;

theorem Th5: :: POLYEQ_3:5

for z being 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)) )

proof end;

theorem :: POLYEQ_3:6

for a, b, c, d, a9, b9, c9, d9 being Real st ( for z being Complex holds Polynom (a,b,c,d,z) = Polynom (a9,b9,c9,d9,z) ) holds
( a = a9 & b = b9 & c = c9 & d = d9 )

proof end;

theorem :: POLYEQ_3:7

for b, c, d being Real
for z being 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))

proof end;

theorem :: POLYEQ_3:8

for b, c, d being Real
for z being 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)) * <i>) holds
z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * <i>)

proof end;

theorem :: POLYEQ_3:9

for a, c being Real
for z being 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

proof end;

theorem :: POLYEQ_3:10

for a, b, c being Real
for z being 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

proof end;

theorem :: POLYEQ_3:11

for a, b, c being Real
for z being 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)) * <i>) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) holds
z = 0

proof end;

theorem Th12: :: POLYEQ_3:12

for a, y being Real holds
( not y ^2 = a or y = sqrt a or y = - (sqrt a) )

proof end;

theorem :: POLYEQ_3:13

for a, c, d being Real
for z being 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)))))

proof end;

theorem :: POLYEQ_3:14

for a, c, d being Real
for z being 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))) * <i>) & 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))) * <i>) & 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))) * <i>) & 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))) * <i>) & 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))) * <i>) 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))) * <i>)

proof end;

theorem :: POLYEQ_3:15

for a, b, c, d being Real
for z being 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 * <i>) & 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 * <i>) 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 * <i>)

proof end;

theorem Th16: :: POLYEQ_3:16

for z, z1, z2 being Complex st z1 <> 0 & Polynom (z1,z2,z) = 0 holds
z = - (z2 / z1)

proof end;

theorem :: POLYEQ_3:17

for z1, z2, z3, s1, s2, s3 being Complex st ( for z being Complex holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ) holds
( z1 = s1 & z2 = s2 & z3 = s3 )

proof end;

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 )

proof end;

theorem Th19: :: POLYEQ_3:19

for s, z being 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)) * <i>) holds
z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>)

proof end;

theorem :: POLYEQ_3:20

for s, z being Complex st z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) holds
z = - (sqrt (Re s))

proof end;

theorem :: POLYEQ_3:21

for s, z being Complex st z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * <i> holds
z = - ((sqrt (- (Re s))) * <i>)

proof end;

theorem :: POLYEQ_3:22

for s, z being 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))) * <i>) holds
z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>)

proof end;

theorem Th23: :: POLYEQ_3:23

for s, z being 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)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )

proof end;

theorem :: POLYEQ_3:24

for z, z1, z2 being Complex st z1 <> 0 & Polynom (z1,z2,0,z) = 0 & not z = - (z2 / z1) holds
z = 0

proof end;

theorem Th25: :: POLYEQ_3:25

for z, z1, z3 being Complex st z1 <> 0 & Polynom (z1,0,z3,z) = 0 holds
for s being 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)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )

proof end;

theorem Th26: :: POLYEQ_3:26

for z, z1, z2, z3 being Complex st z1 <> 0 & Polynom (z1,z2,z3,z) = 0 holds
for h, t being 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)) * <i>)) - 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))) * <i>)) - 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))) * <i>)) - 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)) * <i>)) - t

proof end;

theorem :: POLYEQ_3:27

for z being Complex holds
( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 )

proof end;

theorem :: POLYEQ_3:28

for z, z1, z2 being Complex st z1 <> 0 & Polynom (z1,z2,0,0,z) = 0 & not z = - (z2 / z1) holds
z = 0

proof end;

theorem :: POLYEQ_3:29

for z, z1, z3 being Complex st z1 <> 0 & Polynom (z1,0,z3,0,z) = 0 holds
for s being 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)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )

proof end;

theorem :: POLYEQ_3:30

for z, z1, z2, z3 being Complex st z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 holds
for s, h, t being 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)) * <i>)) - 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))) * <i>)) - 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))) * <i>)) - 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)) * <i>)) - t

proof end;

Lm2: for n being Nat st n > 0 holds
0 |^ n = 0

proof end;

theorem Th31: :: POLYEQ_3:31

for x being Real
for n being Nat holds ((cos x) + ((sin x) * <i>)) |^ n = (cos (n * x)) + ((sin (n * x)) * <i>)

proof end;

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)))) * <i>)

proof end;

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)) * <i>)) |^ n = (cos x) + ((sin x) * <i>)

proof end;

theorem Th34: :: POLYEQ_3:34

for z being Complex
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))) * <i>)) |^ n

proof end;

theorem :: POLYEQ_3:35

for z being Element of COMPLEX
for n being non zero 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))) * <i>) is CRoot of n,z

proof end;

theorem :: POLYEQ_3:36

for z being Complex
for v being CRoot of 1,z holds v = z

proof end;

theorem :: POLYEQ_3:37

for n being non zero Nat
for v being CRoot of n, 0 holds v = 0

proof end;

theorem :: POLYEQ_3:38

for n being non zero Element of NAT
for z being Complex
for v being CRoot of n,z st v = 0 holds
z = 0

proof end;

theorem :: POLYEQ_3:39

for n being non zero Element of NAT
for k being Element of NAT holds (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * <i>) is CRoot of n,1

proof end;

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.|

proof end;