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

definition
let a, b, x be complex number ;
func Poly1 a,b,x -> set equals :: POLYEQ_1:def 1
(a * x) + b;
coherence
(a * x) + b is set ;
end;

:: deftheorem defines Poly1 POLYEQ_1:def 1 :
for a, b, x being complex number holds Poly1 a,b,x = (a * x) + b;

registration
let a, b, x be complex number ;
cluster Poly1 a,b,x -> complex ;
coherence
Poly1 a,b,x is complex ;
end;

registration
let a, b, x be real number ;
cluster Poly1 a,b,x -> complex real ;
coherence
Poly1 a,b,x is real ;
end;

definition
let a, b, x be Real;
:: original: Poly1
redefine func Poly1 a,b,x -> Real;
coherence
Poly1 a,b,x is Real by XREAL_0:def 1;
end;

theorem :: POLYEQ_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, x being complex number st a <> 0 & Poly1 a,b,x = 0 holds
x = - (b / a)
proof end;

theorem :: POLYEQ_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being complex number holds Poly1 0,0,x = 0 ;

theorem :: POLYEQ_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being complex number st b <> 0 holds
for x being complex number holds not Poly1 0,b,x = 0 ;

definition
let a, b, c, x be complex number ;
func Poly2 a,b,c,x -> set equals :: POLYEQ_1:def 2
((a * (x ^2 )) + (b * x)) + c;
coherence
((a * (x ^2 )) + (b * x)) + c is set ;
end;

:: deftheorem defines Poly2 POLYEQ_1:def 2 :
for a, b, c, x being complex number holds Poly2 a,b,c,x = ((a * (x ^2 )) + (b * x)) + c;

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

registration
let a, b, c, x be complex number ;
cluster Poly2 a,b,c,x -> complex ;
coherence
Poly2 a,b,c,x is complex ;
end;

definition
let a, b, c, x be Real;
:: original: Poly2
redefine func Poly2 a,b,c,x -> Real;
coherence
Poly2 a,b,c,x is Real by XREAL_0:def 1;
end;

theorem Th4: :: POLYEQ_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, a', b', c' being complex number st ( for x being real number holds Poly2 a,b,c,x = Poly2 a',b',c',x ) holds
( a = a' & b = b' & c = c' )
proof end;

theorem Th5: :: POLYEQ_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a <> 0 & delta a,b,c >= 0 holds
for x being real number holds
( not Poly2 a,b,c,x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
proof end;

theorem :: POLYEQ_1:6  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 being complex number st a <> 0 & delta a,b,c = 0 & Poly2 a,b,c,x = 0 holds
x = - (b / (2 * a))
proof end;

theorem :: POLYEQ_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a <> 0 & delta a,b,c < 0 holds
for x being real number holds not Poly2 a,b,c,x = 0
proof end;

theorem :: POLYEQ_1:8  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
for b, c being complex number st b <> 0 & ( for x being real number holds Poly2 0,b,c,x = 0 ) holds
x = - (c / b)
proof end;

theorem :: POLYEQ_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being complex number holds Poly2 0,0,0,x = 0 ;

theorem :: POLYEQ_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being complex number st c <> 0 holds
for x being complex number holds not Poly2 0,0,c,x = 0 ;

definition
let a, x, x1, x2 be complex number ;
func Quard a,x1,x2,x -> set equals :: POLYEQ_1:def 3
a * ((x - x1) * (x - x2));
coherence
a * ((x - x1) * (x - x2)) is set ;
end;

:: deftheorem defines Quard POLYEQ_1:def 3 :
for a, x, x1, x2 being complex number holds Quard a,x1,x2,x = a * ((x - x1) * (x - x2));

registration
let a, x, x1, x2 be real number ;
cluster Quard a,x1,x2,x -> real ;
coherence
Quard a,x1,x2,x is real ;
end;

definition
let a, x, x1, x2 be Real;
:: original: Quard
redefine func Quard a,x1,x2,x -> Real;
coherence
Quard a,x1,x2,x is Real by XREAL_0:def 1;
end;

theorem :: POLYEQ_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being real number
for a, b, c being complex number st a <> 0 & ( for x being real number holds Poly2 a,b,c,x = Quard a,x1,x2,x ) holds
( b / a = - (x1 + x2) & c / a = x1 * x2 )
proof end;

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

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

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

definition
let a, b, c, d, x be Real;
:: original: Poly3
redefine func Poly3 a,b,c,d,x -> Real;
coherence
Poly3 a,b,c,d,x is Real by XREAL_0:def 1;
end;

theorem Th12: :: POLYEQ_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, a', b', c', d' being real number st ( for x being real number holds Poly3 a,b,c,d,x = Poly3 a',b',c',d',x ) holds
( a = a' & b = b' & c = c' & d = d' )
proof end;

definition
let a, x, x1, x2, x3 be real number ;
func Tri a,x1,x2,x3,x -> set equals :: POLYEQ_1:def 5
a * (((x - x1) * (x - x2)) * (x - x3));
coherence
a * (((x - x1) * (x - x2)) * (x - x3)) is set ;
end;

:: deftheorem defines Tri POLYEQ_1:def 5 :
for a, x, x1, x2, x3 being real number holds Tri a,x1,x2,x3,x = a * (((x - x1) * (x - x2)) * (x - x3));

registration
let a, x, x1, x2, x3 be real number ;
cluster Tri a,x1,x2,x3,x -> real ;
coherence
Tri a,x1,x2,x3,x is real ;
end;

definition
let a, x, x1, x2, x3 be Real;
:: original: Tri
redefine func Tri a,x1,x2,x3,x -> Real;
coherence
Tri a,x1,x2,x3,x is Real by XREAL_0:def 1;
end;

theorem :: POLYEQ_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, x1, x2, x3 being real number st a <> 0 & ( for x being real number holds Poly3 a,b,c,d,x = Tri a,x1,x2,x3,x ) holds
( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )
proof end;

theorem Th14: :: POLYEQ_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, h being real number holds (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (h |^ 3)
proof end;

theorem Th15: :: POLYEQ_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, x being real number st a <> 0 & Poly3 a,b,c,d,x = 0 holds
for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2 )) + ((((3 * (h ^2 )) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3)) = 0
proof end;

theorem :: POLYEQ_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, x being real number st a <> 0 & Poly3 a,b,c,d,x = 0 holds
for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
(((y |^ 3) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0
proof end;

theorem :: POLYEQ_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, a, c, b, d being real number st (((y |^ 3) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0 holds
for p, q being real number st p = (((3 * a) * c) - (b ^2 )) / (3 * (a ^2 )) & q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) holds
Poly3 1,0,p,q,y = 0 ;

theorem Th18: :: POLYEQ_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, y being real number st Poly3 1,0,p,q,y = 0 holds
for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
proof end;

theorem Th19: :: POLYEQ_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, y being real number st Poly3 1,0,p,q,y = 0 holds
for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))
proof end;

theorem :: POLYEQ_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b, c, d, x being real number st b <> 0 & delta b,c,d > 0 & Poly3 0,b,c,d,x = 0 & not x = ((- c) + (sqrt (delta b,c,d))) / (2 * b) holds
x = ((- c) - (sqrt (delta b,c,d))) / (2 * b)
proof end;

theorem :: POLYEQ_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, p, c, q, d, x being real number st a <> 0 & p = c / a & q = d / a & Poly3 a,0,c,d,x = 0 holds
for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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
x = (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_1:22  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 being real number st a <> 0 & delta a,b,c >= 0 & Poly3 a,b,c,0,x = 0 & not x = 0 & not x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) holds
x = ((- b) - (sqrt (delta a,b,c))) / (2 * a)
proof end;

theorem :: POLYEQ_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, x being real number st a <> 0 & c / a < 0 & Poly3 a,0,c,0,x = 0 & not x = 0 & not x = sqrt (- (c / a)) holds
x = - (sqrt (- (c / a)))
proof end;