:: Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients :: by Xiquan Liang :: :: Received February 3, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin 4 = 2 * 2 ; then 2 divides 4 by INT_1:def_3; then Lm1: 4 is even by ABIAN:def_1; 3 = (2 * 1) + 1 ; then Lm2: 3 is odd by ABIAN:1; definition let a, b, c, d, e, x be complex number ; func Polynom (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 Polynom POLYEQ_2:def_1_:_ for a, b, c, d, e, x being complex number holds Polynom (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 complex number ; cluster Polynom (a,b,c,d,e,x) -> complex ; coherence Polynom (a,b,c,d,e,x) is complex ; end; registration let a, b, c, d, e, x be real number ; cluster Polynom (a,b,c,d,e,x) -> real ; coherence Polynom (a,b,c,d,e,x) is real ; end; theorem :: POLYEQ_2:1 for a, c, e, x being real number st a <> 0 & e <> 0 & (c ^2) - ((4 * a) * e) > 0 & Polynom (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))) ) ) proofend; theorem Th2: :: POLYEQ_2:2 for a, b, c, x, y being real number st a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) proofend; theorem :: POLYEQ_2:3 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) & Polynom (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 ) ) proofend; theorem Th4: :: POLYEQ_2:4 for x being real number holds ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) proofend; theorem Th5: :: POLYEQ_2:5 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) proofend; theorem :: POLYEQ_2:6 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) proofend; theorem Th7: :: POLYEQ_2:7 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (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 ) proofend; theorem Th8: :: POLYEQ_2:8 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) proofend; theorem Th9: :: POLYEQ_2:9 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) proofend; 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 for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (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) proofend; theorem Th11: :: POLYEQ_2:11 for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (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) proofend; theorem :: POLYEQ_2:12 for a1, a2, a3, a4, a5, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (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 ) proofend; theorem :: POLYEQ_2:13 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 proofend;