:: POLYEQ_1 semantic presentation

definition
let c1, c2, c3 be complex number ;
func Poly1 c1,c2,c3 -> set equals :: POLYEQ_1:def 1
(a1 * a3) + a2;
coherence
(c1 * c3) + c2 is set ;
end;

:: deftheorem Def1 defines Poly1 POLYEQ_1:def 1 :
for b1, b2, b3 being complex number holds Poly1 b1,b2,b3 = (b1 * b3) + b2;

registration
let c1, c2, c3 be complex number ;
cluster Poly1 a1,a2,a3 -> complex ;
coherence
Poly1 c1,c2,c3 is complex ;
end;

registration
let c1, c2, c3 be real number ;
cluster Poly1 a1,a2,a3 -> complex real ;
coherence
Poly1 c1,c2,c3 is real ;
end;

definition
let c1, c2, c3 be Real;
redefine func Poly1 as Poly1 c1,c2,c3 -> Real;
coherence
Poly1 c1,c2,c3 is Real by XREAL_0:def 1;
end;

theorem Th1: :: POLYEQ_1:1
for b1, b2, b3 being complex number st b1 <> 0 & Poly1 b1,b2,b3 = 0 holds
b3 = - (b2 / b1)
proof end;

theorem Th2: :: POLYEQ_1:2
for b1 being complex number holds Poly1 0,0,b1 = 0 ;

theorem Th3: :: POLYEQ_1:3
for b1 being complex number st b1 <> 0 holds
for b2 being complex number holds not Poly1 0,b1,b2 = 0 ;

definition
let c1, c2, c3, c4 be complex number ;
func Poly2 c1,c2,c3,c4 -> set equals :: POLYEQ_1:def 2
((a1 * (a4 ^2 )) + (a2 * a4)) + a3;
coherence
((c1 * (c4 ^2 )) + (c2 * c4)) + c3 is set ;
end;

:: deftheorem Def2 defines Poly2 POLYEQ_1:def 2 :
for b1, b2, b3, b4 being complex number holds Poly2 b1,b2,b3,b4 = ((b1 * (b4 ^2 )) + (b2 * b4)) + b3;

registration
let c1, c2, c3, c4 be real number ;
cluster Poly2 a1,a2,a3,a4 -> real ;
coherence
Poly2 c1,c2,c3,c4 is real ;
end;

registration
let c1, c2, c3, c4 be complex number ;
cluster Poly2 a1,a2,a3,a4 -> complex ;
coherence
Poly2 c1,c2,c3,c4 is complex ;
end;

definition
let c1, c2, c3, c4 be Real;
redefine func Poly2 as Poly2 c1,c2,c3,c4 -> Real;
coherence
Poly2 c1,c2,c3,c4 is Real by XREAL_0:def 1;
end;

theorem Th4: :: POLYEQ_1:4
for b1, b2, b3, b4, b5, b6 being complex number st ( for b7 being real number holds Poly2 b1,b2,b3,b7 = Poly2 b4,b5,b6,b7 ) holds
( b1 = b4 & b2 = b5 & b3 = b6 )
proof end;

theorem Th5: :: POLYEQ_1:5
for b1, b2, b3 being real number st b1 <> 0 & delta b1,b2,b3 >= 0 holds
for b4 being real number holds
( not Poly2 b1,b2,b3,b4 = 0 or b4 = ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) or b4 = ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) )
proof end;

theorem Th6: :: POLYEQ_1:6
for b1, b2, b3, b4 being complex number st b1 <> 0 & delta b1,b2,b3 = 0 & Poly2 b1,b2,b3,b4 = 0 holds
b4 = - (b2 / (2 * b1))
proof end;

theorem Th7: :: POLYEQ_1:7
for b1, b2, b3 being real number st b1 <> 0 & delta b1,b2,b3 < 0 holds
for b4 being real number holds not Poly2 b1,b2,b3,b4 = 0
proof end;

theorem Th8: :: POLYEQ_1:8
for b1 being real number
for b2, b3 being complex number st b2 <> 0 & ( for b4 being real number holds Poly2 0,b2,b3,b4 = 0 ) holds
b1 = - (b3 / b2)
proof end;

theorem Th9: :: POLYEQ_1:9
for b1 being complex number holds Poly2 0,0,0,b1 = 0 ;

theorem Th10: :: POLYEQ_1:10
for b1 being complex number st b1 <> 0 holds
for b2 being complex number holds not Poly2 0,0,b1,b2 = 0 ;

definition
let c1, c2, c3, c4 be complex number ;
func Quard c1,c3,c4,c2 -> set equals :: POLYEQ_1:def 3
a1 * ((a2 - a3) * (a2 - a4));
coherence
c1 * ((c2 - c3) * (c2 - c4)) is set ;
end;

:: deftheorem Def3 defines Quard POLYEQ_1:def 3 :
for b1, b2, b3, b4 being complex number holds Quard b1,b3,b4,b2 = b1 * ((b2 - b3) * (b2 - b4));

registration
let c1, c2, c3, c4 be real number ;
cluster Quard a1,a3,a4,a2 -> real ;
coherence
Quard c1,c3,c4,c2 is real ;
end;

definition
let c1, c2, c3, c4 be Real;
redefine func Quard as Quard c1,c3,c4,c2 -> Real;
coherence
Quard c1,c3,c4,c2 is Real by XREAL_0:def 1;
end;

theorem Th11: :: POLYEQ_1:11
for b1, b2 being real number
for b3, b4, b5 being complex number st b3 <> 0 & ( for b6 being real number holds Poly2 b3,b4,b5,b6 = Quard b3,b1,b2,b6 ) holds
( b4 / b3 = - (b1 + b2) & b5 / b3 = b1 * b2 )
proof end;

definition
let c1, c2, c3, c4, c5 be real number ;
func Poly3 c1,c2,c3,c4,c5 -> set equals :: POLYEQ_1:def 4
(((a1 * (a5 |^ 3)) + (a2 * (a5 ^2 ))) + (a3 * a5)) + a4;
coherence
(((c1 * (c5 |^ 3)) + (c2 * (c5 ^2 ))) + (c3 * c5)) + c4 is set ;
end;

:: deftheorem Def4 defines Poly3 POLYEQ_1:def 4 :
for b1, b2, b3, b4, b5 being real number holds Poly3 b1,b2,b3,b4,b5 = (((b1 * (b5 |^ 3)) + (b2 * (b5 ^2 ))) + (b3 * b5)) + b4;

registration
let c1, c2, c3, c4, c5 be real number ;
cluster Poly3 a1,a2,a3,a4,a5 -> real ;
coherence
Poly3 c1,c2,c3,c4,c5 is real ;
end;

definition
let c1, c2, c3, c4, c5 be Real;
redefine func Poly3 as Poly3 c1,c2,c3,c4,c5 -> Real;
coherence
Poly3 c1,c2,c3,c4,c5 is Real by XREAL_0:def 1;
end;

theorem Th12: :: POLYEQ_1:12
for b1, b2, b3, b4, b5, b6, b7, b8 being real number st ( for b9 being real number holds Poly3 b1,b2,b3,b4,b9 = Poly3 b5,b6,b7,b8,b9 ) holds
( b1 = b5 & b2 = b6 & b3 = b7 & b4 = b8 )
proof end;

definition
let c1, c2, c3, c4, c5 be real number ;
func Tri c1,c3,c4,c5,c2 -> set equals :: POLYEQ_1:def 5
a1 * (((a2 - a3) * (a2 - a4)) * (a2 - a5));
coherence
c1 * (((c2 - c3) * (c2 - c4)) * (c2 - c5)) is set ;
end;

:: deftheorem Def5 defines Tri POLYEQ_1:def 5 :
for b1, b2, b3, b4, b5 being real number holds Tri b1,b3,b4,b5,b2 = b1 * (((b2 - b3) * (b2 - b4)) * (b2 - b5));

registration
let c1, c2, c3, c4, c5 be real number ;
cluster Tri a1,a3,a4,a5,a2 -> real ;
coherence
Tri c1,c3,c4,c5,c2 is real ;
end;

definition
let c1, c2, c3, c4, c5 be Real;
redefine func Tri as Tri c1,c3,c4,c5,c2 -> Real;
coherence
Tri c1,c3,c4,c5,c2 is Real by XREAL_0:def 1;
end;

theorem Th13: :: POLYEQ_1:13
for b1, b2, b3, b4, b5, b6, b7 being real number st b1 <> 0 & ( for b8 being real number holds Poly3 b1,b2,b3,b4,b8 = Tri b1,b5,b6,b7,b8 ) holds
( b2 / b1 = - ((b5 + b6) + b7) & b3 / b1 = ((b5 * b6) + (b6 * b7)) + (b5 * b7) & b4 / b1 = - ((b5 * b6) * b7) )
proof end;

theorem Th14: :: POLYEQ_1:14
for b1, b2 being real number holds (b1 + b2) |^ 3 = ((b1 |^ 3) + (((3 * b2) * (b1 ^2 )) + ((3 * (b2 ^2 )) * b1))) + (b2 |^ 3)
proof end;

theorem Th15: :: POLYEQ_1:15
for b1, b2, b3, b4, b5 being real number st b1 <> 0 & Poly3 b1,b2,b3,b4,b5 = 0 holds
for b6, b7, b8, b9, b10 being real number st b10 = b5 + (b2 / (3 * b1)) & b9 = - (b2 / (3 * b1)) & b6 = b2 / b1 & b7 = b3 / b1 & b8 = b4 / b1 holds
((b10 |^ 3) + ((((3 * b9) + b6) * (b10 ^2 )) + ((((3 * (b9 ^2 )) + (2 * (b6 * b9))) + b7) * b10))) + (((b9 |^ 3) + (b6 * (b9 ^2 ))) + ((b7 * b9) + b8)) = 0
proof end;

theorem Th16: :: POLYEQ_1:16
for b1, b2, b3, b4, b5 being real number st b1 <> 0 & Poly3 b1,b2,b3,b4,b5 = 0 holds
for b6, b7, b8, b9, b10 being real number st b10 = b5 + (b2 / (3 * b1)) & b9 = - (b2 / (3 * b1)) & b6 = b2 / b1 & b7 = b3 / b1 & b8 = b4 / b1 holds
(((b10 |^ 3) + (0 * (b10 ^2 ))) + (((((3 * b1) * b3) - (b2 ^2 )) / (3 * (b1 ^2 ))) * b10)) + ((2 * ((b2 / (3 * b1)) |^ 3)) + ((((3 * b1) * b4) - (b2 * b3)) / (3 * (b1 ^2 )))) = 0
proof end;

theorem Th17: :: POLYEQ_1:17
for b1, b2, b3, b4, b5 being real number st (((b1 |^ 3) + (0 * (b1 ^2 ))) + (((((3 * b2) * b3) - (b4 ^2 )) / (3 * (b2 ^2 ))) * b1)) + ((2 * ((b4 / (3 * b2)) |^ 3)) + ((((3 * b2) * b5) - (b4 * b3)) / (3 * (b2 ^2 )))) = 0 holds
for b6, b7 being real number st b6 = (((3 * b2) * b3) - (b4 ^2 )) / (3 * (b2 ^2 )) & b7 = (2 * ((b4 / (3 * b2)) |^ 3)) + ((((3 * b2) * b5) - (b4 * b3)) / (3 * (b2 ^2 ))) holds
Poly3 1,0,b6,b7,b1 = 0 ;

theorem Th18: :: POLYEQ_1:18
for b1, b2, b3 being real number st Poly3 1,0,b1,b2,b3 = 0 holds
for b4, b5 being real number st b3 = b4 + b5 & ((3 * b5) * b4) + b1 = 0 holds
( (b4 |^ 3) + (b5 |^ 3) = - b2 & (b4 |^ 3) * (b5 |^ 3) = (- (b1 / 3)) |^ 3 )
proof end;

theorem Th19: :: POLYEQ_1:19
for b1, b2, b3 being real number st Poly3 1,0,b1,b2,b3 = 0 holds
for b4, b5 being real number st b3 = b4 + b5 & ((3 * b5) * b4) + b1 = 0 & not b3 = (3 -root ((- (b2 / 2)) + (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3))))) + (3 -root ((- (b2 / 2)) - (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3))))) & not b3 = (3 -root ((- (b2 / 2)) + (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3))))) + (3 -root ((- (b2 / 2)) + (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3))))) holds
b3 = (3 -root ((- (b2 / 2)) - (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3))))) + (3 -root ((- (b2 / 2)) - (sqrt (((b2 ^2 ) / 4) + ((b1 / 3) |^ 3)))))
proof end;

theorem Th20: :: POLYEQ_1:20
for b1, b2, b3, b4 being real number st b1 <> 0 & delta b1,b2,b3 > 0 & Poly3 0,b1,b2,b3,b4 = 0 & not b4 = ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) holds
b4 = ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)
proof end;

theorem Th21: :: POLYEQ_1:21
for b1, b2, b3, b4, b5, b6 being real number st b1 <> 0 & b2 = b3 / b1 & b4 = b5 / b1 & Poly3 b1,0,b3,b5,b6 = 0 holds
for b7, b8 being real number st b6 = b7 + b8 & ((3 * b8) * b7) + b2 = 0 & not b6 = (3 -root ((- (b5 / (2 * b1))) + (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3))))) + (3 -root ((- (b5 / (2 * b1))) - (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3))))) & not b6 = (3 -root ((- (b5 / (2 * b1))) + (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3))))) + (3 -root ((- (b5 / (2 * b1))) + (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3))))) holds
b6 = (3 -root ((- (b5 / (2 * b1))) - (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3))))) + (3 -root ((- (b5 / (2 * b1))) - (sqrt (((b5 ^2 ) / (4 * (b1 ^2 ))) + ((b3 / (3 * b1)) |^ 3)))))
proof end;

theorem Th22: :: POLYEQ_1:22
for b1, b2, b3, b4 being real number st b1 <> 0 & delta b1,b2,b3 >= 0 & Poly3 b1,b2,b3,0,b4 = 0 & not b4 = 0 & not b4 = ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) holds
b4 = ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)
proof end;

theorem Th23: :: POLYEQ_1:23
for b1, b2, b3 being real number st b1 <> 0 & b2 / b1 < 0 & Poly3 b1,0,b2,0,b3 = 0 & not b3 = 0 & not b3 = sqrt (- (b2 / b1)) holds
b3 = - (sqrt (- (b2 / b1)))
proof end;