:: POLYEQ_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: 4 = 2 * 2
;

definition
let a, b, c, d, e, x be real number ;
func Four a,b,c,d,e,x -> set equals :: POLYEQ_2:def 1
((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2 ))) + (d * x)) + e;
correctness
coherence
((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2 ))) + (d * x)) + e is set ;
;
end;

:: deftheorem defines Four POLYEQ_2:def 1 :
for a, b, c, d, e, x being real number holds Four a,b,c,d,e,x = ((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2 ))) + (d * x)) + e;

registration
let a, b, c, d, e, x be real number ;
cluster Four a,b,c,d,e,x -> real ;
coherence
Four a,b,c,d,e,x is real ;
end;

theorem :: POLYEQ_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, e, x being real number st a <> 0 & e <> 0 & (c ^2 ) - ((4 * a) * e) > 0 & Four a,0,c,0,e,x = 0 holds
( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) )
proof end;

theorem Th2: :: POLYEQ_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, x, y being real number st a <> 0 & y = x + (1 / x) & Four a,b,c,b,a,x = 0 holds
( x <> 0 & (((a * (y ^2 )) + (b * y)) + c) - (2 * a) = 0 )
proof end;

theorem :: POLYEQ_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, x, y being real number st a <> 0 & ((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 )) > 0 & y = x + (1 / x) & Four a,b,c,b,a,x = 0 holds
for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta 1,(- y1),1))) / 2 or x = (y2 + (sqrt (delta 1,(- y2),1))) / 2 or x = (y1 - (sqrt (delta 1,(- y1),1))) / 2 or x = (y2 - (sqrt (delta 1,(- y2),1))) / 2 ) )
proof end;

theorem Th4: :: POLYEQ_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 )
proof end;

theorem Th5: :: POLYEQ_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x + y <> 0 holds
(x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x))) + (y |^ 3)) * y)
proof end;

theorem :: POLYEQ_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x + y <> 0 holds
(x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2 )) * (x ^2 ))) + ((4 * (y |^ 3)) * x))) + (y |^ 4)
proof end;

theorem Th7: :: POLYEQ_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four b1,b2,b3,b4,b5,x ) holds
( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 )
proof end;

theorem Th8: :: POLYEQ_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four b1,b2,b3,b4,b5,x ) holds
( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 )
proof end;

theorem Th9: :: POLYEQ_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four b1,b2,b3,b4,b5,x ) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 )
proof end;

definition
let a1, x1, x2, x3, x4, x be real number ;
func Four0 a1,x1,x2,x3,x4,x -> set equals :: POLYEQ_2:def 2
a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));
correctness
coherence
a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) is set ;
;
end;

:: deftheorem defines Four0 POLYEQ_2:def 2 :
for a1, x1, x2, x3, x4, x being real number holds Four0 a1,x1,x2,x3,x4,x = a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));

registration
let a1, x1, x2, x3, x4, x be real number ;
cluster Four0 a1,x1,x2,x3,x4,x -> real ;
coherence
Four0 a1,x1,x2,x3,x4,x is real ;
end;

theorem Th10: :: POLYEQ_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x ) holds
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = (((((x ^2 ) * (x ^2 )) - (((x1 + x2) + x3) * ((x ^2 ) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2 ))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4)
proof end;

theorem Th11: :: POLYEQ_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x ) holds
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
proof end;

theorem :: POLYEQ_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, a3, a4, a5, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Four a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x ) holds
( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 )
proof end;

theorem :: POLYEQ_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, k, y being real number st a <> 0 & ( for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2 ) + (a ^2 )) ) holds
(((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
proof end;