:: POLYEQ_3 semantic presentation

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

definition

let c₁ be Real;
let c₂ be Element of COMPLEX ;
redefine func * as c₁ * c₂ -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;
redefine func + as c₁ + c₂ -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;

end;

definition

let c₁ be Element of COMPLEX ;
redefine func ^2 as c₁ ^2 -> Element of COMPLEX equals :: POLYEQ_3:def 1
(((Re a₁) ^2 ) - ((Im a₁) ^2 )) + ((2 * ((Re a₁) * (Im a₁))) * );
compatibility

proof end;

correctness by XCMPLX_0:def 2;

end;

:: deftheorem Def1 defines ^2 POLYEQ_3:def 1 :

definition

let c₁, c₂, c₃ be Real;
let c₄ be Element of COMPLEX ;
redefine func Poly2 as Poly2 c₁,c₂,c₃,c₄ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem Th1: :: POLYEQ_3:1

for b₁, b₂, b₃, b₄ being Real holds (b₁ + (b₂ * )) * (b₃ + (b₄ * )) = ((b₁ * b₃) - (b₂ * b₄)) + (((b₁ * b₄) + (b₃ * b₂)) * ) ;

theorem Th2: :: POLYEQ_3:2

for b₁, b₂ being Real holds [*b₁,b₂*] ^2 = ((b₁ ^2 ) - (b₂ ^2 )) + (((2 * b₁) * b₂) * )

proof end;

theorem Th3: :: POLYEQ_3:3

canceled;

theorem Th4: :: POLYEQ_3:4

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & delta b₁,b₂,b₃ >= 0 & Poly2 b₁,b₂,b₃,b₄ = 0 & not b₄ = ((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) & not b₄ = ((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) holds
b₄ = - (b₂ / (2 * b₁))

proof end;

theorem Th5: :: POLYEQ_3:5

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & delta b₁,b₂,b₃ < 0 & Poly2 b₁,b₂,b₃,b₄ = 0 & not b₄ = (- (b₂ / (2 * b₁))) + (((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁)) * ) holds
b₄ = (- (b₂ / (2 * b₁))) + ((- ((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁))) * )

proof end;

theorem Th6: :: POLYEQ_3:6

for b₁, b₂ being Real
for b₃ being Element of COMPLEX st b₁ <> 0 & ( for b₄ being Element of COMPLEX holds Poly2 0,b₁,b₂,b₄ = 0 ) holds
b₃ = - (b₂ / b₁)

proof end;

theorem Th7: :: POLYEQ_3:7

for b₁, b₂, b₃ being Real
for b₄, b₅, b₆ being complex number st b₁ <> 0 & ( for b₇ being complex number holds Poly2 b₁,b₂,b₃,b₇ = Quard b₁,b₅,b₆,b₇ ) holds
( b₂ / b₁ = - (b₅ + b₆) & b₃ / b₁ = b₅ * b₆ )

proof end;

definition

let c₁ be complex number ;
func c₁ ^3 -> Element of COMPLEX equals :: POLYEQ_3:def 2
(a₁ ^2 ) * a₁;
correctness by XCMPLX_0:def 2;

end;

:: deftheorem Def2 defines ^3 POLYEQ_3:def 2 :

definition

let c₁, c₂, c₃, c₄ be Real;
let c₅ be complex number ;
func Poly_3 c₁,c₂,c₃,c₄,c₅ -> Element of COMPLEX equals :: POLYEQ_3:def 3
(((a₁ * (a₅ ^3 )) + (a₂ * (a₅ ^2 ))) + (a₃ * a₅)) + a₄;
coherence by XCMPLX_0:def 2;

end;

:: deftheorem Def3 defines Poly_3 POLYEQ_3:def 3 :

theorem Th8: :: POLYEQ_3:8

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

theorem Th9: :: POLYEQ_3:9

1 ^3 = 1 ;

theorem Th10: :: POLYEQ_3:10

(- 1) ^3 = - 1 ;

theorem Th11: :: POLYEQ_3:11

for b₁ being Element of COMPLEX holds
( Re (b₁ ^3 ) = ((Re b₁) |^ 3) - ((3 * (Re b₁)) * ((Im b₁) ^2 )) & Im (b₁ ^3 ) = (- ((Im b₁) |^ 3)) + ((3 * ((Re b₁) ^2 )) * (Im b₁)) )

proof end;

theorem Th12: :: POLYEQ_3:12

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Real st ( for b₉ being complex number holds Poly_3 b₁,b₂,b₃,b₄,b₉ = Poly_3 b₅,b₆,b₇,b₈,b₉ ) holds
( b₁ = b₅ & b₂ = b₆ & b₃ = b₇ & b₄ = b₈ )

proof end;

theorem Th13: :: POLYEQ_3:13

for b₁, b₂ being Element of COMPLEX holds (b₁ + b₂) ^3 = (((b₁ ^3 ) + ((3 * b₂) * (b₁ ^2 ))) + ((3 * (b₂ ^2 )) * b₁)) + (b₂ ^3 ) ;

theorem Th14: :: POLYEQ_3:14

for b₁, b₂ being Element of COMPLEX holds (b₁ * b₂) ^3 = (b₁ ^3 ) * (b₂ ^3 ) ;

theorem Th15: :: POLYEQ_3:15

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 0,b₁,b₂,b₃,b₄ = 0 & delta b₁,b₂,b₃ >= 0 & not b₄ = ((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) & not b₄ = ((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) holds
b₄ = - (b₂ / (2 * b₁))

proof end;

theorem Th16: :: POLYEQ_3:16

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 0,b₁,b₂,b₃,b₄ = 0 & delta b₁,b₂,b₃ < 0 & not b₄ = (- (b₂ / (2 * b₁))) + (((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁)) * ) holds
b₄ = (- (b₂ / (2 * b₁))) + ((- ((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁))) * )

proof end;

theorem Th17: :: POLYEQ_3:17

for b₁, b₂ being Real
for b₃ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,0,b₂,0,b₃ = 0 & (4 * b₁) * b₂ <= 0 & not b₃ = (sqrt (- ((4 * b₁) * b₂))) / (2 * b₁) & not b₃ = (- (sqrt (- ((4 * b₁) * b₂)))) / (2 * b₁) holds
b₃ = 0

proof end;

theorem Th18: :: POLYEQ_3:18

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,b₂,b₃,0,b₄ = 0 & delta b₁,b₂,b₃ >= 0 & not b₄ = ((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) & not b₄ = ((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) & not b₄ = - (b₂ / (2 * b₁)) holds
b₄ = 0

proof end;

theorem Th19: :: POLYEQ_3:19

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,b₂,b₃,0,b₄ = 0 & delta b₁,b₂,b₃ < 0 & not b₄ = (- (b₂ / (2 * b₁))) + (((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁)) * ) & not b₄ = (- (b₂ / (2 * b₁))) + ((- ((sqrt (- (delta b₁,b₂,b₃))) / (2 * b₁))) * ) holds
b₄ = 0

proof end;

theorem Th20: :: POLYEQ_3:20

for b₁, b₂ being Real holds
( not b₁ ^2 = b₂ or b₁ = sqrt b₂ or b₁ = - (sqrt b₂) )

proof end;

theorem Th21: :: POLYEQ_3:21

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,0,b₂,b₃,b₄ = 0 & Im b₄ = 0 holds
for b₅, b₆ being Real st Re b₄ = b₅ + b₆ & ((3 * b₆) * b₅) + (b₂ / b₁) = 0 & not b₄ = (3 -root ((- (b₃ / (2 * b₁))) + (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3))))) + (3 -root ((- (b₃ / (2 * b₁))) - (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3))))) & not b₄ = (3 -root ((- (b₃ / (2 * b₁))) + (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3))))) + (3 -root ((- (b₃ / (2 * b₁))) + (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3))))) holds
b₄ = (3 -root ((- (b₃ / (2 * b₁))) - (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3))))) + (3 -root ((- (b₃ / (2 * b₁))) - (sqrt (((b₃ ^2 ) / (4 * (b₁ ^2 ))) + ((b₂ / (3 * b₁)) |^ 3)))))

proof end;

theorem Th22: :: POLYEQ_3:22

for b₁, b₂, b₃ being Real
for b₄ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,0,b₂,b₃,b₄ = 0 & Im b₄ <> 0 holds
for b₅, b₆ being Real st Re b₄ = b₅ + b₆ & ((3 * b₆) * b₅) + (b₂ / (4 * b₁)) = 0 & b₂ / b₁ >= 0 & not b₄ = ((3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3))))) + (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3))))) + (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * ) & not b₄ = ((3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3))))) + (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3))))) + (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * ) & not b₄ = (2 * (3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * ) & not b₄ = (2 * (3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((b₃ / (16 * b₁)) + (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * ) & not b₄ = (2 * (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * ) holds
b₄ = (2 * (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((b₃ / (16 * b₁)) - (sqrt (((b₃ / (16 * b₁)) ^2 ) + ((b₂ / (12 * b₁)) |^ 3)))))) ^2 )) + (b₂ / b₁))) * )

proof end;

theorem Th23: :: POLYEQ_3:23

for b₁, b₂, b₃, b₄ being Real
for b₅ being Element of COMPLEX st b₁ <> 0 & Poly_3 b₁,b₂,b₃,b₄,b₅ = 0 & Im b₅ = 0 holds
for b₆, b₇, b₈ being Real st b₈ = (Re b₅) + (b₂ / (3 * b₁)) & Re b₅ = (b₆ + b₇) - (b₂ / (3 * b₁)) & ((3 * b₆) * b₇) + ((((3 * b₁) * b₃) - (b₂ ^2 )) / (3 * (b₁ ^2 ))) = 0 & not b₅ = (((3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) + (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3))))) + (3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) - (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3)))))) - (b₂ / (3 * b₁))) + (0 * ) & not b₅ = (((3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) + (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3))))) + (3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) + (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3)))))) - (b₂ / (3 * b₁))) + (0 * ) holds
b₅ = (((3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) - (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3))))) + (3 -root (((- ((b₂ / (3 * b₁)) |^ 3)) - ((((3 * b₁) * b₄) - (b₂ * b₃)) / (6 * (b₁ ^2 )))) - (sqrt (((((2 * ((b₂ / (3 * b₁)) |^ 3)) + ((((3 * b₁) * b₄) - (b₂ * b₃)) / (3 * (b₁ ^2 )))) ^2 ) / 4) + (((((3 * b₁) * b₃) - (b₂ ^2 )) / (9 * (b₁ ^2 ))) |^ 3)))))) - (b₂ / (3 * b₁))) + (0 * )

proof end;

theorem Th24: :: POLYEQ_3:24

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> 0 & Poly1 b₁,b₂,b₃ = 0 holds
b₃ = - (b₂ / b₁)

proof end;

theorem Th25: :: POLYEQ_3:25

for b₁ being Element of COMPLEX st b₁ <> 0 holds
for b₂ being Element of COMPLEX holds not Poly1 0,b₁,b₂ = 0 ;

definition

let c₁, c₂, c₃, c₄ be Element of COMPLEX ;
func CPoly2 c₁,c₂,c₃,c₄ -> Element of COMPLEX equals :: POLYEQ_3:def 4
((a₁ * (a₄ ^2 )) + (a₂ * a₄)) + a₃;
coherence ;

end;

:: deftheorem Def4 defines CPoly2 POLYEQ_3:def 4 :

theorem Th26: :: POLYEQ_3:26

for b₁, b₂, b₃, b₄, b₅, b₆ being Element of COMPLEX st ( for b₇ being Element of COMPLEX holds CPoly2 b₁,b₂,b₃,b₇ = CPoly2 b₄,b₅,b₆,b₇ ) holds
( b₁ = b₄ & b₂ = b₅ & b₃ = b₆ )

proof end;

theorem Th27: :: POLYEQ_3:27

for b₁, b₂ being Real holds
( ((- b₁) + (sqrt ((b₁ ^2 ) + (b₂ ^2 )))) / 2 >= 0 & (b₁ + (sqrt ((b₁ ^2 ) + (b₂ ^2 )))) / 2 >= 0 )

proof end;

theorem Th28: :: POLYEQ_3:28

for b₁, b₂ being Element of COMPLEX st b₁ ^2 = b₂ & Im b₂ >= 0 & not b₁ = (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) + ((sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) * ) holds
b₁ = (- (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) * )

proof end;

theorem Th29: :: POLYEQ_3:29

for b₁, b₂ being Element of COMPLEX st b₁ ^2 = b₂ & Im b₂ = 0 & Re b₂ > 0 & not b₁ = sqrt (Re b₂) holds
b₁ = - (sqrt (Re b₂))

proof end;

theorem Th30: :: POLYEQ_3:30

for b₁, b₂ being Element of COMPLEX st b₁ ^2 = b₂ & Im b₂ = 0 & Re b₂ < 0 & not b₁ = (sqrt (- (Re b₂))) * holds
b₁ = - ((sqrt (- (Re b₂))) * )

proof end;

theorem Th31: :: POLYEQ_3:31

for b₁, b₂ being Element of COMPLEX st b₁ ^2 = b₂ & Im b₂ < 0 & not b₁ = (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) * ) holds
b₁ = (- (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) + ((sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) * )

proof end;

theorem Th32: :: POLYEQ_3:32

for b₁, b₂ being Element of COMPLEX holds
( not b₁ ^2 = b₂ or b₁ = (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) + ((sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) * ) or b₁ = (- (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) * ) or b₁ = (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) * ) or b₁ = (- (sqrt (((Re b₂) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2))) + ((sqrt (((- (Re b₂)) + (sqrt (((Re b₂) ^2 ) + ((Im b₂) ^2 )))) / 2)) * ) )

proof end;

theorem Th33: :: POLYEQ_3:33

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

theorem Th34: :: POLYEQ_3:34

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & CPoly2 b₁,0c ,0c ,b₂ = 0 holds
b₂ = 0

proof end;

theorem Th35: :: POLYEQ_3:35

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> 0 & CPoly2 b₁,b₂,0c ,b₃ = 0 & not b₃ = - (b₂ / b₁) holds
b₃ = 0

proof end;

theorem Th36: :: POLYEQ_3:36

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> 0 & CPoly2 b₁,0c ,b₂,b₃ = 0 holds
for b₄ being Element of COMPLEX holds
( not b₄ = - (b₂ / b₁) or b₃ = (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) + ((sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) * ) or b₃ = (- (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) * ) or b₃ = (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) * ) or b₃ = (- (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) + ((sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) * ) )

proof end;

theorem Th37: :: POLYEQ_3:37

for b₁, b₂, b₃, b₄ being Element of COMPLEX st b₁ <> 0 & CPoly2 b₁,b₂,b₃,b₄ = 0 holds
for b₅, b₆ being Element of COMPLEX st b₅ = ((b₂ / (2 * b₁)) ^2 ) - (b₃ / b₁) & b₆ = b₂ / (2 * b₁) & not b₄ = ((sqrt (((Re b₅) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2)) + ((sqrt (((- (Re b₅)) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2)) * )) - b₆ & not b₄ = ((- (sqrt (((Re b₅) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₅)) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2))) * )) - b₆ & not b₄ = ((sqrt (((Re b₅) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₅)) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2))) * )) - b₆ holds
b₄ = ((- (sqrt (((Re b₅) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2))) + ((sqrt (((- (Re b₅)) + (sqrt (((Re b₅) ^2 ) + ((Im b₅) ^2 )))) / 2)) * )) - b₆

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be Element of COMPLEX ;
func CPoly3 c₁,c₂,c₃,c₄,c₅ -> Element of COMPLEX equals :: POLYEQ_3:def 5
(((a₁ * (a₅ ^3 )) + (a₂ * (a₅ ^2 ))) + (a₃ * a₅)) + a₄;
coherence ;

end;

:: deftheorem Def5 defines CPoly3 POLYEQ_3:def 5 :

theorem Th38: :: POLYEQ_3:38

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

theorem Th39: :: POLYEQ_3:39

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

proof end;

theorem Th40: :: POLYEQ_3:40

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> 0 & CPoly3 b₁,b₂,0c ,0c ,b₃ = 0 & not b₃ = - (b₂ / b₁) holds
b₃ = 0

proof end;

theorem Th41: :: POLYEQ_3:41

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> 0 & CPoly3 b₁,0c ,b₂,0c ,b₃ = 0 holds
for b₄ being Element of COMPLEX holds
( not b₄ = - (b₂ / b₁) or b₃ = 0 or b₃ = (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) + ((sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) * ) or b₃ = (- (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) * ) or b₃ = (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) * ) or b₃ = (- (sqrt (((Re b₄) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2))) + ((sqrt (((- (Re b₄)) + (sqrt (((Re b₄) ^2 ) + ((Im b₄) ^2 )))) / 2)) * ) )

proof end;

theorem Th42: :: POLYEQ_3:42

for b₁, b₂, b₃, b₄ being Element of COMPLEX st b₁ <> 0 & CPoly3 b₁,b₂,b₃,0c ,b₄ = 0 holds
for b₅, b₆, b₇ being Element of COMPLEX st b₅ = - (b₃ / b₁) & b₆ = ((b₂ / (2 * b₁)) ^2 ) - (b₃ / b₁) & b₇ = b₂ / (2 * b₁) & not b₄ = 0 & not b₄ = ((sqrt (((Re b₆) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2)) + ((sqrt (((- (Re b₆)) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2)) * )) - b₇ & not b₄ = ((- (sqrt (((Re b₆) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2))) + ((- (sqrt (((- (Re b₆)) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2))) * )) - b₇ & not b₄ = ((sqrt (((Re b₆) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2)) + ((- (sqrt (((- (Re b₆)) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2))) * )) - b₇ holds
b₄ = ((- (sqrt (((Re b₆) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2))) + ((sqrt (((- (Re b₆)) + (sqrt (((Re b₆) ^2 ) + ((Im b₆) ^2 )))) / 2)) * )) - b₇

proof end;

theorem Th43: :: POLYEQ_3:43

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

theorem Th44: :: POLYEQ_3:44

for b₁, b₂, b₃ being Element of COMPLEX st b₁ = b₂ - ((1 / 3) * b₃) holds
b₁ ^3 = (((b₂ ^3 ) - (b₃ * (b₂ ^2 ))) + (((1 / 3) * (b₃ ^2 )) * b₂)) - ((1 / 27) * (b₃ ^3 )) ;

theorem Th45: :: POLYEQ_3:45

for b₁, b₂, b₃, b₄ being Element of COMPLEX st CPoly3 1r ,b₁,b₂,b₃,b₄ = 0 holds
for b₅, b₆, b₇ being Element of COMPLEX st b₄ = b₇ - ((1 / 3) * b₁) & b₅ = (- ((1 / 3) * (b₁ ^2 ))) + b₂ & b₆ = (((2 / 27) * (b₁ ^3 )) - (((1 / 3) * b₁) * b₂)) + b₃ holds
CPoly3 1r ,0c ,b₅,b₆,b₇ = 0 by COMPLEX1:def 6, COMPLEX1:def 7;

theorem Th46: :: POLYEQ_3:46

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

proof end;

theorem Th47: :: POLYEQ_3:47

for b₁ being Element of COMPLEX
for b₂ being Nat holds b₁ #N (b₂ + 1) = (b₁ #N b₂) * b₁

proof end;

theorem Th48: :: POLYEQ_3:48

for b₁ being Element of COMPLEX holds b₁ #N 1 = b₁

proof end;

theorem Th49: :: POLYEQ_3:49

for b₁ being Element of COMPLEX holds b₁ #N 2 = b₁ * b₁

proof end;

theorem Th50: :: POLYEQ_3:50

for b₁ being Nat st b₁ > 0 holds
0c #N b₁ = 0

proof end;

theorem Th51: :: POLYEQ_3:51

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (b₁ * b₂) #N b₃ = (b₁ #N b₃) * (b₂ #N b₃)

proof end;

theorem Th52: :: POLYEQ_3:52

for b₁ being Real st b₁ > 0 holds
for b₂ being Nat holds [*b₁,0*] #N b₂ = b₁ to_power b₂

proof end;

theorem Th53: :: POLYEQ_3:53

for b₁ being Real
for b₂ being Nat holds [*(cos b₁),(sin b₁)*] #N b₂ = (cos (b₂ * b₁)) + ((sin (b₂ * b₁)) * )

proof end;

theorem Th54: :: POLYEQ_3:54

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

proof end;

theorem Th55: :: POLYEQ_3:55

for b₁, b₂ being Nat
for b₃ being Real st b₁ <> 0 holds
[*(cos ((b₃ + ((2 * PI ) * b₂)) / b₁)),(sin ((b₃ + ((2 * PI ) * b₂)) / b₁))*] #N b₁ = (cos b₃) + ((sin b₃) * )

proof end;

theorem Th56: :: POLYEQ_3:56

for b₁ being complex number
for b₂, b₃ being Nat st b₂ <> 0 holds
b₁ = [*((b₂ -root |.b₁.|) * (cos (((Arg b₁) + ((2 * PI ) * b₃)) / b₂))),((b₂ -root |.b₁.|) * (sin (((Arg b₁) + ((2 * PI ) * b₃)) / b₂)))*] #N b₂

proof end;

definition

let c₁ be complex number ;
let c₂ be non empty Nat;
mode CRoot of c₂,c₁ -> Element of COMPLEX means :Def6: :: POLYEQ_3:def 6
a₃ #N a₂ = a₁;
existence

proof end;

end;

:: deftheorem Def6 defines CRoot POLYEQ_3:def 6 :

theorem Th57: :: POLYEQ_3:57

for b₁ being Element of COMPLEX
for b₂ being non empty Nat
for b₃ being Nat holds [*((b₂ -root |.b₁.|) * (cos (((Arg b₁) + ((2 * PI ) * b₃)) / b₂))),((b₂ -root |.b₁.|) * (sin (((Arg b₁) + ((2 * PI ) * b₃)) / b₂)))*] is CRoot of b₂,b₁

proof end;

theorem Th58: :: POLYEQ_3:58

for b₁ being complex number
for b₂ being CRoot of 1,b₁ holds b₂ = b₁

proof end;

theorem Th59: :: POLYEQ_3:59

for b₁ being non empty Nat
for b₂ being CRoot of b₁,0 holds b₂ = 0

proof end;

theorem Th60: :: POLYEQ_3:60

for b₁ being non empty Nat
for b₂ being complex number
for b₃ being CRoot of b₁,b₂ st b₃ = 0 holds
b₂ = 0

proof end;

theorem Th61: :: POLYEQ_3:61

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

proof end;

theorem Th62: :: POLYEQ_3:62

canceled;

theorem Th63: :: POLYEQ_3:63

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat st b₂ <> 0 & b₁ <> 0 & b₃ >= 1 & b₂ #N b₃ = b₁ #N b₃ holds
|.b₂.| = |.b₁.|

proof end;