:: Solving the Roots of the Special Polynomial Equation with Real Coefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004-2021 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;