:: Solving the Roots of the Special Polynomial Equation with Real Coefficients :: by Yuzhong Ding and Xiquan Liang :: :: Received March 18, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin theorem Th1: :: POLYEQ_4:1 for b, a, c being Real st b / a < 0 & c / a > 0 & delta (a,b,c) >= 0 holds ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) proofend; theorem :: POLYEQ_4:2 for b, a, c being Real st b / a > 0 & c / a > 0 & delta (a,b,c) >= 0 holds ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) proofend; theorem :: POLYEQ_4:3 for c, a, b being Real holds ( not c / a < 0 or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) proofend; theorem Th4: :: POLYEQ_4:4 for a, x being Real for n being Element of NAT st a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a holds x = - (n -root a) proofend; theorem Th5: :: POLYEQ_4:5 for a, b, x being Real st a <> 0 & Polynom (a,b,0,x) = 0 & not x = 0 holds x = - (b / a) proofend; theorem :: POLYEQ_4:6 for a, x being Real st a <> 0 & Polynom (a,0,0,x) = 0 holds x = 0 proofend; theorem :: POLYEQ_4:7 for a, b, c, x being Real for n being Element of NAT st a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) holds x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) proofend; theorem :: POLYEQ_4:8 for a, b, c, x being Real for n being Element of NAT st a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) holds x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) proofend; theorem :: POLYEQ_4:9 for a, b, x being Real for n being Element of NAT st a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 holds x = n -root (- (b / a)) proofend; theorem :: POLYEQ_4:10 for a, b, x being Real for n being Element of NAT st a <> 0 & b / a < 0 & n is even & n >= 1 & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 & not x = n -root (- (b / a)) holds x = - (n -root (- (b / a))) proofend; theorem Th11: :: POLYEQ_4:11 for a, b being Real holds ( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) ) proofend; theorem :: POLYEQ_4:12 for a, b, x being Real st a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 & Polynom (a,b,b,a,x) = 0 & not x = - 1 & not x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) holds x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) proofend; definition let a, b, c, d, e, f, x be complex number ; func Polynom (a,b,c,d,e,f,x) -> set equals :: POLYEQ_4:def 1 (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f; coherence (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f is set ; end; :: deftheorem defines Polynom POLYEQ_4:def_1_:_ for a, b, c, d, e, f, x being complex number holds Polynom (a,b,c,d,e,f,x) = (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f; registration let a, b, c, d, e, f, x be complex number ; cluster Polynom (a,b,c,d,e,f,x) -> complex ; coherence Polynom (a,b,c,d,e,f,x) is complex ; end; registration let a, b, c, d, e, f, x be real number ; cluster Polynom (a,b,c,d,e,f,x) -> real ; coherence Polynom (a,b,c,d,e,f,x) is real ; end; theorem :: POLYEQ_4:13 for a, b, c, x being Real st a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 & Polynom (a,b,c,c,b,a,x) = 0 holds for y1, y2 being Real st y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 holds x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 proofend; theorem Th14: :: POLYEQ_4:14 for x, y, p, q being Real st x + y = p & x * y = q & (p ^2) - (4 * q) >= 0 & not ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) holds ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) proofend; theorem :: POLYEQ_4:15 for x, y, p, q being Real for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) holds ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) proofend; theorem :: POLYEQ_4:16 for x, y, p, q being Real for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & p > 0 & q > 0 & n is even & n >= 1 & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) holds ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) proofend; theorem :: POLYEQ_4:17 for x, y, a, b being Real for n being Element of NAT st (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) holds ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) proofend; theorem :: POLYEQ_4:18 for a, x, b, y, p being Real for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) holds ( x = n -root (p / a) & y = 0 ) proofend; theorem :: POLYEQ_4:19 for a, x, b, y, p being Real for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) holds ( x = - (n -root (p / a)) & y = 0 ) proofend; theorem :: POLYEQ_4:20 for a, x, p, y, q being Real for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 holds ( x = n -root (p / a) & y = q * (n -root (a / p)) ) proofend; theorem :: POLYEQ_4:21 for a, x, p, y, q being Real for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) holds ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) proofend; theorem :: POLYEQ_4:22 for a, x being Real st a > 0 & a <> 1 & a to_power x = 1 holds x = 0 proofend; theorem :: POLYEQ_4:23 for a, x being Real st a > 0 & a <> 1 & a to_power x = a holds x = 1 proofend; theorem :: POLYEQ_4:24 for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 0 holds x = 1 proofend; theorem :: POLYEQ_4:25 for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 1 holds x = a proofend;