:: Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients :: by Liang Xiquan :: :: Received May 18, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin definition let a, b, x be complex number ; func Polynom (a,b,x) -> set equals :: POLYEQ_1:def 1 (a * x) + b; coherence (a * x) + b is set ; end; :: deftheorem defines Polynom POLYEQ_1:def_1_:_ for a, b, x being complex number holds Polynom (a,b,x) = (a * x) + b; registration let a, b, x be complex number ; cluster Polynom (a,b,x) -> complex ; coherence Polynom (a,b,x) is complex ; end; registration let a, b, x be real number ; cluster Polynom (a,b,x) -> real ; coherence Polynom (a,b,x) is real ; end; definition let a, b, x be Real; :: original:Polynom redefine func Polynom (a,b,x) -> Real; coherence Polynom (a,b,x) is Real by XREAL_0:def_1; end; theorem :: POLYEQ_1:1 for a, b, x being complex number st a <> 0 & Polynom (a,b,x) = 0 holds x = - (b / a) proofend; theorem :: POLYEQ_1:2 for x being complex number holds Polynom (0,0,x) = 0 ; theorem :: POLYEQ_1:3 for b being complex number st b <> 0 holds for x being complex number holds not Polynom (0,b,x) = 0 ; definition let a, b, c, x be complex number ; func Polynom (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 Polynom POLYEQ_1:def_2_:_ for a, b, c, x being complex number holds Polynom (a,b,c,x) = ((a * (x ^2)) + (b * x)) + c; registration let a, b, c, x be real number ; cluster Polynom (a,b,c,x) -> real ; coherence Polynom (a,b,c,x) is real ; end; registration let a, b, c, x be complex number ; cluster Polynom (a,b,c,x) -> complex ; coherence Polynom (a,b,c,x) is complex ; end; definition let a, b, c, x be Real; :: original:Polynom redefine func Polynom (a,b,c,x) -> Real; coherence Polynom (a,b,c,x) is Real by XREAL_0:def_1; end; theorem Th4: :: POLYEQ_1:4 for a, b, c, a9, b9, c9 being complex number st ( for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) holds ( a = a9 & b = b9 & c = c9 ) proofend; theorem Th5: :: POLYEQ_1:5 for a, b, c being real number st a <> 0 & delta (a,b,c) >= 0 holds for x being real number holds ( not Polynom (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) ) proofend; theorem :: POLYEQ_1:6 for a, b, c, x being complex number st a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 holds x = - (b / (2 * a)) proofend; theorem :: POLYEQ_1:7 for a, b, c being real number st delta (a,b,c) < 0 holds for x being real number holds not Polynom (a,b,c,x) = 0 proofend; theorem :: POLYEQ_1:8 for x being real number for b, c being complex number st b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) holds x = - (c / b) proofend; theorem :: POLYEQ_1:9 for x being complex number holds Polynom (0,0,0,x) = 0 ; theorem :: POLYEQ_1:10 for c being complex number st c <> 0 holds for x being complex number holds not Polynom (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 for x1, x2 being real number for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds ( b / a = - (x1 + x2) & c / a = x1 * x2 ) proofend; begin definition let a, b, c, d, x be complex number ; func Polynom (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 Polynom POLYEQ_1:def_4_:_ for a, b, c, d, x being complex number holds Polynom (a,b,c,d,x) = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d; registration let a, b, c, d, x be complex number ; cluster Polynom (a,b,c,d,x) -> complex ; coherence Polynom (a,b,c,d,x) is complex ; end; registration let a, b, c, d, x be real number ; cluster Polynom (a,b,c,d,x) -> real ; coherence Polynom (a,b,c,d,x) is real ; end; definition let a, b, c, d, x be Real; :: original:Polynom redefine func Polynom (a,b,c,d,x) -> Real; coherence Polynom (a,b,c,d,x) is Real by XREAL_0:def_1; end; 3 = (2 * 1) + 1 ; then Lm1: 3 is odd by ABIAN:1; theorem Th12: :: POLYEQ_1:12 for a, b, c, d, a9, b9, c9, d9 being real number st ( for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) holds ( a = a9 & b = b9 & c = c9 & d = d9 ) proofend; 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 for a, b, c, d, x1, x2, x3 being real number st a <> 0 & ( for x being real number holds Polynom (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) ) proofend; theorem Th14: :: POLYEQ_1:14 for y, h being real number holds (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) proofend; theorem Th15: :: POLYEQ_1:15 for a, b, c, d, x being real number st a <> 0 & Polynom (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 proofend; theorem :: POLYEQ_1:16 for a, b, c, d, x being real number st a <> 0 & Polynom (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 proofend; theorem :: POLYEQ_1:17 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 Polynom (1,0,p,q,y) = 0 ; theorem Th18: :: POLYEQ_1:18 for p, q, y being real number st Polynom (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 ) proofend; theorem Th19: :: POLYEQ_1:19 for p, q, y being real number st Polynom (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))))) proofend; theorem :: POLYEQ_1:20 for b, c, d, x being real number st b <> 0 & delta (b,c,d) > 0 & Polynom (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) proofend; theorem :: POLYEQ_1:21 for a, p, c, q, d, x being real number st a <> 0 & p = c / a & q = d / a & Polynom (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))))) proofend; theorem :: POLYEQ_1:22 for a, b, c, x being real number st a <> 0 & delta (a,b,c) >= 0 & Polynom (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) proofend; theorem :: POLYEQ_1:23 for a, c, x being real number st a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) holds x = - (sqrt (- (c / a))) proofend;