:: POLYEQ_3 semantic presentation

Lm1: 0 = [*0,0*]
by ARYTM_0:def 7;

definition

let a be Real;
let z be Element of COMPLEX ;
:: original: *
redefine func a * z -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;
:: original: +
redefine func a + z -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;

end;

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

proof end;

correctness by XCMPLX_0:def 2;

end;

:: deftheorem defines ^2 POLYEQ_3:def 1 :

definition

let a, b, c be Real;
let z be Element of COMPLEX ;
:: original: Poly2
redefine func Poly2 a,b,c,z -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem :: POLYEQ_3:1

for a, c, b, d being Real holds (a + (c * )) * (b + (d * )) = ((a * b) - (c * d)) + (((a * d) + (b * c)) * ) ;

theorem :: POLYEQ_3:2

for x, y being Real holds [*x,y*] ^2 = ((x ^2 ) - (y ^2 )) + (((2 * x) * y) * )

proof end;

theorem :: POLYEQ_3:3

canceled;

theorem Th4: :: POLYEQ_3:4

for a, b, c being Real
for z being Element of COMPLEX st a <> 0 & delta a,b,c >= 0 & Poly2 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 Th5: :: POLYEQ_3:5

for a, b, c being Real
for z being Element of COMPLEX st a <> 0 & delta a,b,c < 0 & Poly2 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))) * )

proof end;

theorem :: POLYEQ_3:6

for b, c being Real
for z being Element of COMPLEX st b <> 0 & ( for z being Element of COMPLEX holds Poly2 0,b,c,z = 0 ) holds
z = - (c / b)

proof end;

theorem :: POLYEQ_3:7

for a, b, c being Real
for z, z1, z2 being complex number st a <> 0 & ( for z being complex number holds Poly2 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 number ;
func z ^3 -> Element of COMPLEX equals :: POLYEQ_3:def 2
(z ^2 ) * z;
correctness by XCMPLX_0:def 2;

end;

:: deftheorem defines ^3 POLYEQ_3:def 2 :

definition

let a, b, c, d be Real;
let z be complex number ;
func Poly_3 a,b,c,d,z -> Element of COMPLEX equals :: POLYEQ_3:def 3
(((a * (z ^3 )) + (b * (z ^2 ))) + (c * z)) + d;
coherence by XCMPLX_0:def 2;

end;

:: deftheorem defines Poly_3 POLYEQ_3:def 3 :

theorem :: POLYEQ_3:8

0c ^3 = 0 by COMPLEX1:def 6;

theorem :: POLYEQ_3:9

1 ^3 = 1 ;

theorem :: POLYEQ_3:10

(- 1) ^3 = - 1 ;

theorem Th11: :: POLYEQ_3:11

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

proof end;

theorem :: POLYEQ_3:12

for a, b, c, d, a', b', c', d' being Real st ( for z being complex number holds Poly_3 a,b,c,d,z = Poly_3 a',b',c',d',z ) holds
( a = a' & b = b' & c = c' & d = d' )

proof end;

theorem :: POLYEQ_3:13

for z, h being Element of COMPLEX holds (z + h) ^3 = (((z ^3 ) + ((3 * h) * (z ^2 ))) + ((3 * (h ^2 )) * z)) + (h ^3 ) ;

theorem :: POLYEQ_3:14

for z, h being Element of COMPLEX holds (z * h) ^3 = (z ^3 ) * (h ^3 ) ;

theorem :: POLYEQ_3:15

for b, c, d being Real
for z being Element of COMPLEX st b <> 0 & Poly_3 0,b,c,d,z = 0 & delta b,c,d >= 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:16

for b, c, d being Real
for z being Element of COMPLEX st b <> 0 & Poly_3 0,b,c,d,z = 0 & delta b,c,d < 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))) * )

proof end;

theorem :: POLYEQ_3:17

for a, c being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 a,0,c,0,z = 0 & (4 * a) * c <= 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:18

for a, b, c being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 a,b,c,0,z = 0 & delta a,b,c >= 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:19

for a, b, c being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 a,b,c,0,z = 0 & delta a,b,c < 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

proof end;

theorem Th20: :: POLYEQ_3:20

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

proof end;

theorem :: POLYEQ_3:21

for a, c, d being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 a,0,c,d,z = 0 & Im 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:22

for a, c, d being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 a,0,c,d,z = 0 & Im z <> 0 holds
for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / 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))) * )

proof end;

theorem :: POLYEQ_3:23

for a, b, c, d being Real
for z being Element of COMPLEX st a <> 0 & Poly_3 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 * )

proof end;

theorem Th24: :: POLYEQ_3:24

for z1, z2, z being Element of COMPLEX st z1 <> 0 & Poly1 z1,z2,z = 0 holds
z = - (z2 / z1)

proof end;

theorem :: POLYEQ_3:25

for z2 being Element of COMPLEX st z2 <> 0 holds
for z being Element of COMPLEX holds not Poly1 0,z2,z = 0 ;

definition

let z1, z2, z3, z be Element of COMPLEX ;
func CPoly2 z1,z2,z3,z -> Element of COMPLEX equals :: POLYEQ_3:def 4
((z1 * (z ^2 )) + (z2 * z)) + z3;
coherence ;

end;

:: deftheorem defines CPoly2 POLYEQ_3:def 4 :

theorem :: POLYEQ_3:26

for z1, z2, z3, s1, s2, s3 being Element of COMPLEX st ( for z being Element of COMPLEX holds CPoly2 z1,z2,z3,z = CPoly2 s1,s2,s3,z ) holds
( z1 = s1 & z2 = s2 & z3 = s3 )

proof end;

theorem :: POLYEQ_3:27

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 Th28: :: POLYEQ_3:28

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

proof end;

theorem :: POLYEQ_3:29

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

proof end;

theorem :: POLYEQ_3:30

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

proof end;

theorem :: POLYEQ_3:31

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

proof end;

theorem Th32: :: POLYEQ_3:32

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

proof end;

theorem :: POLYEQ_3:33

for z being Element of COMPLEX holds CPoly2 0c ,0c ,0c ,z = 0 by COMPLEX1:def 6;

theorem Th34: :: POLYEQ_3:34

for z1, z being Element of COMPLEX st z1 <> 0 & CPoly2 z1,0c ,0c ,z = 0 holds
z = 0

proof end;

theorem :: POLYEQ_3:35

for z1, z2, z being Element of COMPLEX st z1 <> 0 & CPoly2 z1,z2,0c ,z = 0 & not z = - (z2 / z1) holds
z = 0

proof end;

theorem Th36: :: POLYEQ_3:36

for z1, z3, z being Element of COMPLEX st z1 <> 0 & CPoly2 z1,0c ,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)) * ) )

proof end;

theorem Th37: :: POLYEQ_3:37

for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & CPoly2 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

proof end;

definition

let z1, z2, z3, z4, z be Element of COMPLEX ;
func CPoly3 z1,z2,z3,z4,z -> Element of COMPLEX equals :: POLYEQ_3:def 5
(((z1 * (z ^3 )) + (z2 * (z ^2 ))) + (z3 * z)) + z4;
coherence ;

end;

:: deftheorem defines CPoly3 POLYEQ_3:def 5 :

theorem :: POLYEQ_3:38

for z being Element of COMPLEX holds
( not z ^2 = 1 or z = 1 or z = - 1 ) by XCMPLX_1:183;

theorem :: POLYEQ_3:39

for z being Element of COMPLEX holds
( z #N 3 = (z * z) * z & z #N 3 = (z ^2 ) * z & z #N 3 = z ^3 )

proof end;

theorem :: POLYEQ_3:40

for z1, z2, z being Element of COMPLEX st z1 <> 0 & CPoly3 z1,z2,0c ,0c ,z = 0 & not z = - (z2 / z1) holds
z = 0

proof end;

theorem :: POLYEQ_3:41

for z1, z3, z being Element of COMPLEX st z1 <> 0 & CPoly3 z1,0c ,z3,0c ,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)) * ) )

proof end;

theorem :: POLYEQ_3:42

for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & CPoly3 z1,z2,z3,0c ,z = 0 holds
for s, h, t being Element of COMPLEX st s = - (z3 / z1) & 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

proof end;

theorem :: POLYEQ_3:43

for s, z1 being Element of COMPLEX holds (s - ((1 / 3) * z1)) ^2 = ((s ^2 ) + (((- (2 / 3)) * z1) * s)) + ((1 / 9) * (z1 ^2 )) ;

theorem :: POLYEQ_3:44

for z, s, z1 being Element of COMPLEX st z = s - ((1 / 3) * z1) holds
z ^3 = (((s ^3 ) - (z1 * (s ^2 ))) + (((1 / 3) * (z1 ^2 )) * s)) - ((1 / 27) * (z1 ^3 )) ;

theorem :: POLYEQ_3:45

for z1, z2, z3, z being Element of COMPLEX st CPoly3 1r ,z1,z2,z3,z = 0 holds
for p, q, s being Element of COMPLEX st z = s - ((1 / 3) * z1) & p = (- ((1 / 3) * (z1 ^2 ))) + z2 & q = (((2 / 27) * (z1 ^3 )) - (((1 / 3) * z1) * z2)) + z3 holds
CPoly3 1r ,0c ,p,q,s = 0 by COMPLEX1:def 6, COMPLEX1:def 7;

theorem Th46: :: POLYEQ_3:46

for z being Element of COMPLEX holds [*(|.z.| * (cos (Arg z))),(|.z.| * (sin (Arg z)))*] = [*|.z.|,0*] * [*(cos (Arg z)),(sin (Arg z))*]

proof end;

theorem Th47: :: POLYEQ_3:47

for z being Element of COMPLEX
for n being Nat holds z #N (n + 1) = (z #N n) * z

proof end;

theorem Th48: :: POLYEQ_3:48

for z being Element of COMPLEX holds z #N 1 = z

proof end;

theorem :: POLYEQ_3:49

for z being Element of COMPLEX holds z #N 2 = z * z

proof end;

theorem Th50: :: POLYEQ_3:50

for n being Nat st n > 0 holds
0c #N n = 0

proof end;

theorem Th51: :: POLYEQ_3:51

for x, y being Element of COMPLEX
for n being Nat holds (x * y) #N n = (x #N n) * (y #N n)

proof end;

theorem Th52: :: POLYEQ_3:52

for x being Real st x > 0 holds
for n being Nat holds [*x,0*] #N n = x to_power n

proof end;

theorem Th53: :: POLYEQ_3:53

for x being Real
for n being Nat holds [*(cos x),(sin x)*] #N n = (cos (n * x)) + ((sin (n * x)) * )

proof end;

theorem :: POLYEQ_3:54

for z being Element of COMPLEX
for n being Nat st ( z <> 0 or n > 0 ) holds
z #N n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * )

proof end;

theorem Th55: :: POLYEQ_3:55

for n, k being Nat
for x being Real st n <> 0 holds
[*(cos ((x + ((2 * PI ) * k)) / n)),(sin ((x + ((2 * PI ) * k)) / n))*] #N n = (cos x) + ((sin x) * )

proof end;

theorem Th56: :: POLYEQ_3:56

for z being complex number
for n, k being 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 n

proof end;

definition

let z be complex number ;
let n be non empty Nat;
mode CRoot of n,z -> Element of COMPLEX means :Def6: :: POLYEQ_3:def 6
it #N n = z;
existence

proof end;

end;

:: deftheorem Def6 defines CRoot POLYEQ_3:def 6 :

theorem :: POLYEQ_3:57

for z being Element of COMPLEX
for n being non empty Nat
for k being 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 end;

theorem :: POLYEQ_3:58

for z being complex number
for v being CRoot of 1,z holds v = z

proof end;

theorem :: POLYEQ_3:59

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

proof end;

theorem :: POLYEQ_3:60

for n being non empty Nat
for z being complex number
for v being CRoot of n,z st v = 0 holds
z = 0

proof end;

theorem :: POLYEQ_3:61

for n being non empty Nat
for k being Nat holds (cos (((2 * PI ) * k) / n)) + ((sin (((2 * PI ) * k) / n)) * ) is CRoot of n,1

proof end;

theorem :: POLYEQ_3:62

canceled;

theorem :: POLYEQ_3:63

for z, s being Element of COMPLEX
for n being Nat st s <> 0 & z <> 0 & n >= 1 & s #N n = z #N n holds
|.s.| = |.z.|

proof end;