:: Solving the Roots of the Special Polynomial Equation with Real Coefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Copyright (c) 2004-2018 Association of Mizar Users

theorem Th1: :: POLYEQ_4:1
for a, b, 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 )
proof end;

theorem :: POLYEQ_4:2
for a, b, 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 )
proof end;

theorem :: POLYEQ_4:3
for a, b, c 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 ) )
proof end;

theorem Th4: :: POLYEQ_4:4
for x, a 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)
proof end;

theorem Th5: :: POLYEQ_4:5
for x, a, b being Real st a <> 0 & Polynom (a,b,0,x) = 0 & not x = 0 holds
x = - (b / a)
proof end;

theorem :: POLYEQ_4:6
for x, a being Real st a <> 0 & Polynom (a,0,0,x) = 0 holds
x = 0
proof end;

theorem :: POLYEQ_4:7
for x, a, b, c 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))
proof end;

theorem :: POLYEQ_4:8
for x, a, b, c 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)))
proof end;

theorem :: POLYEQ_4:9
for x, a, b 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))
proof end;

theorem :: POLYEQ_4:10
for x, a, b 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)))
proof end;

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)) )
proof end;

theorem :: POLYEQ_4:12
for x, a, b 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)
proof end;

definition
let a, b, c, d, e, f, x be Complex;
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 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;
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;
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 x, a, b, c 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
proof end;

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 )
proof end;

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) )
proof end;

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)) )
proof end;

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)) )
proof end;

theorem :: POLYEQ_4:18
for x, y, a, b, 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 )
proof end;

theorem :: POLYEQ_4:19
for x, y, a, b, 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 )
proof end;

theorem :: POLYEQ_4:20
for x, y, a, p, 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)) )
proof end;

theorem :: POLYEQ_4:21
for x, y, a, p, 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))) )
proof end;

theorem :: POLYEQ_4:22
for a, x being Real st a > 0 & a <> 1 & a to_power x = 1 holds
x = 0
proof end;

theorem :: POLYEQ_4:23
for a, x being Real st a > 0 & a <> 1 & a to_power x = a holds
x = 1
proof end;

theorem :: POLYEQ_4:24
for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 0 holds
x = 1
proof end;

theorem :: POLYEQ_4:25
for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 1 holds
x = a
proof end;