:: Solving the Roots of the Special Polynomial Equation with RealCoefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: POLYEQ_4:1
theorem :: POLYEQ_4:2
theorem :: POLYEQ_4:3
for
a,
c,
b being
Real st
a <> 0 &
c / a < 0 & not (
((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 &
((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) holds
(
((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 &
((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 )
theorem Th4: :: POLYEQ_4:4
theorem Th5: :: POLYEQ_4:5
theorem :: POLYEQ_4:6
theorem :: POLYEQ_4:7
for
a,
b,
c,
x being
Real for
n being
Element of
NAT st
a <> 0 & ex
m being
Element of
NAT st
n = (2 * m) + 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)) holds
x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))
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 & ex
m being
Element of
NAT st
(
n = 2
* m &
m >= 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)))
theorem :: POLYEQ_4:9
theorem :: POLYEQ_4:10
theorem Th11: :: POLYEQ_4:11
theorem :: POLYEQ_4:12
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
theorem Th14: :: POLYEQ_4:14
theorem :: POLYEQ_4:15
theorem :: POLYEQ_4:16
theorem :: POLYEQ_4:17
canceled;
theorem :: POLYEQ_4:18
theorem :: POLYEQ_4:19
theorem :: POLYEQ_4:20
theorem :: POLYEQ_4:21
theorem :: POLYEQ_4:22
theorem :: POLYEQ_4:23
canceled;
theorem :: POLYEQ_4:24
theorem :: POLYEQ_4:25
theorem :: POLYEQ_4:26
canceled;
theorem :: POLYEQ_4:27
theorem :: POLYEQ_4:28