:: POLYEQ_2 semantic presentation

Lemma1: 4 = 2 * 2
;

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

:: deftheorem Def1 defines Four POLYEQ_2:def 1 :
for b1, b2, b3, b4, b5, b6 being real number holds Four b1,b2,b3,b4,b5,b6 = ((((b1 * (b6 |^ 4)) + (b2 * (b6 |^ 3))) + (b3 * (b6 ^2 ))) + (b4 * b6)) + b5;

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

theorem Th1: :: POLYEQ_2:1
for b1, b2, b3, b4 being real number st b1 <> 0 & b3 <> 0 & (b2 ^2 ) - ((4 * b1) * b3) > 0 & Four b1,0,b2,0,b3,b4 = 0 holds
( b4 <> 0 & ( b4 = sqrt (((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1)) or b4 = sqrt (((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)) or b4 = - (sqrt (((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1))) or b4 = - (sqrt (((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1))) ) )
proof end;

theorem Th2: :: POLYEQ_2:2
for b1, b2, b3, b4, b5 being real number st b1 <> 0 & b5 = b4 + (1 / b4) & Four b1,b2,b3,b2,b1,b4 = 0 holds
( b4 <> 0 & (((b1 * (b5 ^2 )) + (b2 * b5)) + b3) - (2 * b1) = 0 )
proof end;

theorem Th3: :: POLYEQ_2:3
for b1, b2, b3, b4, b5 being real number st b1 <> 0 & ((b2 ^2 ) - ((4 * b1) * b3)) + (8 * (b1 ^2 )) > 0 & b5 = b4 + (1 / b4) & Four b1,b2,b3,b2,b1,b4 = 0 holds
for b6, b7 being real number st b6 = ((- b2) + (sqrt (((b2 ^2 ) - ((4 * b1) * b3)) + (8 * (b1 ^2 ))))) / (2 * b1) & b7 = ((- b2) - (sqrt (((b2 ^2 ) - ((4 * b1) * b3)) + (8 * (b1 ^2 ))))) / (2 * b1) holds
( b4 <> 0 & ( b4 = (b6 + (sqrt (delta 1,(- b6),1))) / 2 or b4 = (b7 + (sqrt (delta 1,(- b7),1))) / 2 or b4 = (b6 - (sqrt (delta 1,(- b6),1))) / 2 or b4 = (b7 - (sqrt (delta 1,(- b7),1))) / 2 ) )
proof end;

theorem Th4: :: POLYEQ_2:4
for b1 being real number holds
( b1 |^ 3 = (b1 ^2 ) * b1 & (b1 |^ 3) * b1 = b1 |^ 4 & (b1 ^2 ) * (b1 ^2 ) = b1 |^ 4 )
proof end;

theorem Th5: :: POLYEQ_2:5
for b1, b2 being real number st b1 + b2 <> 0 holds
(b1 + b2) |^ 4 = ((((b1 |^ 3) + (((3 * b2) * (b1 ^2 )) + ((3 * (b2 ^2 )) * b1))) + (b2 |^ 3)) * b1) + ((((b1 |^ 3) + (((3 * b2) * (b1 ^2 )) + ((3 * (b2 ^2 )) * b1))) + (b2 |^ 3)) * b2)
proof end;

theorem Th6: :: POLYEQ_2:6
for b1, b2 being real number st b1 + b2 <> 0 holds
(b1 + b2) |^ 4 = ((b1 |^ 4) + ((((4 * b2) * (b1 |^ 3)) + ((6 * (b2 ^2 )) * (b1 ^2 ))) + ((4 * (b2 |^ 3)) * b1))) + (b2 |^ 4)
proof end;

theorem Th7: :: POLYEQ_2:7
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being real number st ( for b11 being real number holds Four b1,b2,b3,b4,b5,b11 = Four b6,b7,b8,b9,b10,b11 ) holds
( b5 = b10 & ((b1 - b2) + b3) - b4 = ((b6 - b7) + b8) - b9 & ((b1 + b2) + b3) + b4 = ((b6 + b7) + b8) + b9 )
proof end;

theorem Th8: :: POLYEQ_2:8
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being real number st ( for b11 being real number holds Four b1,b2,b3,b4,b5,b11 = Four b6,b7,b8,b9,b10,b11 ) holds
( b1 - b6 = b8 - b3 & b2 - b7 = b9 - b4 )
proof end;

theorem Th9: :: POLYEQ_2:9
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being real number st ( for b11 being real number holds Four b1,b2,b3,b4,b5,b11 = Four b6,b7,b8,b9,b10,b11 ) holds
( b1 = b6 & b2 = b7 & b3 = b8 & b4 = b9 & b5 = b10 )
proof end;

definition
let c1, c2, c3, c4, c5, c6 be real number ;
func Four0 c1,c2,c3,c4,c5,c6 -> set equals :: POLYEQ_2:def 2
a1 * ((((a6 - a2) * (a6 - a3)) * (a6 - a4)) * (a6 - a5));
correctness
coherence
c1 * ((((c6 - c2) * (c6 - c3)) * (c6 - c4)) * (c6 - c5)) is set ;
;
end;

:: deftheorem Def2 defines Four0 POLYEQ_2:def 2 :
for b1, b2, b3, b4, b5, b6 being real number holds Four0 b1,b2,b3,b4,b5,b6 = b1 * ((((b6 - b2) * (b6 - b3)) * (b6 - b4)) * (b6 - b5));

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

theorem Th10: :: POLYEQ_2:10
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being real number st b1 <> 0 & ( for b11 being real number holds Four b1,b2,b3,b4,b5,b11 = Four0 b1,b7,b8,b9,b10,b11 ) holds
(((((b1 * (b6 |^ 4)) + (b2 * (b6 |^ 3))) + (b3 * (b6 ^2 ))) + (b4 * b6)) + b5) / b1 = (((((b6 ^2 ) * (b6 ^2 )) - (((b7 + b8) + b9) * ((b6 ^2 ) * b6))) + ((((b7 * b9) + (b8 * b9)) + (b7 * b8)) * (b6 ^2 ))) - (((b7 * b8) * b9) * b6)) - ((((b6 - b7) * (b6 - b8)) * (b6 - b9)) * b10)
proof end;

theorem Th11: :: POLYEQ_2:11
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being real number st b1 <> 0 & ( for b11 being real number holds Four b1,b2,b3,b4,b5,b11 = Four0 b1,b7,b8,b9,b10,b11 ) holds
(((((b1 * (b6 |^ 4)) + (b2 * (b6 |^ 3))) + (b3 * (b6 ^2 ))) + (b4 * b6)) + b5) / b1 = ((((b6 |^ 4) - ((((b7 + b8) + b9) + b10) * (b6 |^ 3))) + ((((((b7 * b8) + (b7 * b9)) + (b7 * b10)) + ((b8 * b9) + (b8 * b10))) + (b9 * b10)) * (b6 ^2 ))) - ((((((b7 * b8) * b9) + ((b7 * b8) * b10)) + ((b7 * b9) * b10)) + ((b8 * b9) * b10)) * b6)) + (((b7 * b8) * b9) * b10)
proof end;

theorem Th12: :: POLYEQ_2:12
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being real number st b1 <> 0 & ( for b10 being real number holds Four b1,b2,b3,b4,b5,b10 = Four0 b1,b6,b7,b8,b9,b10 ) holds
( b2 / b1 = - (((b6 + b7) + b8) + b9) & b3 / b1 = ((((b6 * b7) + (b6 * b8)) + (b6 * b9)) + ((b7 * b8) + (b7 * b9))) + (b8 * b9) & b4 / b1 = - (((((b6 * b7) * b8) + ((b6 * b7) * b9)) + ((b6 * b8) * b9)) + ((b7 * b8) * b9)) & b5 / b1 = ((b6 * b7) * b8) * b9 )
proof end;

theorem Th13: :: POLYEQ_2:13
for b1, b2, b3 being real number st b1 <> 0 & ( for b4 being real number holds (b4 |^ 4) + (b1 |^ 4) = ((b2 * b1) * b4) * ((b4 ^2 ) + (b1 ^2 )) ) holds
(((b3 |^ 4) - (b2 * (b3 |^ 3))) - (b2 * b3)) + 1 = 0
proof end;