:: Solving Complex Roots of Polynomial Equation of Degree 2 and 3 withComplex Coefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Received January 26, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem defines ^2 POLYEQ_3:def 1 :
theorem :: POLYEQ_3:1
canceled;
theorem :: POLYEQ_3:2
canceled;
theorem :: POLYEQ_3:3
canceled;
theorem Th4: :: POLYEQ_3:4
for
a,
b,
c being
Real for
z being
Element of
COMPLEX st
a <> 0 &
delta a,
b,
c >= 0 &
Polynom a,
b,
c,
z = 0 & not
z = ((- b) + (sqrt (delta a,b,c))) / (2 * a) & not
z = ((- b) - (sqrt (delta a,b,c))) / (2 * a) holds
z = - (b / (2 * a))
theorem Th5: :: POLYEQ_3:5
for
a,
b,
c being
Real for
z being
Element of
COMPLEX st
a <> 0 &
delta a,
b,
c < 0 &
Polynom a,
b,
c,
z = 0 & not
z = (- (b / (2 * a))) + (((sqrt (- (delta a,b,c))) / (2 * a)) * <i> ) holds
z = (- (b / (2 * a))) + ((- ((sqrt (- (delta a,b,c))) / (2 * a))) * <i> )
theorem :: POLYEQ_3:6
theorem :: POLYEQ_3:7
for
a,
b,
c being
Real for
z,
z1,
z2 being
complex number st
a <> 0 & ( for
z being
complex number holds
Polynom a,
b,
c,
z = Quard a,
z1,
z2,
z ) holds
(
b / a = - (z1 + z2) &
c / a = z1 * z2 )
:: deftheorem defines ^3 POLYEQ_3:def 2 :
Lm2:
for z being complex number holds z |^ 2 = z * z
definition
let a,
b,
c,
d,
z be
complex number ;
redefine func Polynom a,
b,
c,
d,
z equals :: POLYEQ_3:def 3
(((a * (z ^3 )) + (b * (z ^2 ))) + (c * z)) + d;
compatibility
for b1 being set holds
( b1 = Polynom a,b,c,d,z iff b1 = (((a * (z ^3 )) + (b * (z ^2 ))) + (c * z)) + d )
end;
:: deftheorem defines Polynom POLYEQ_3:def 3 :
theorem :: POLYEQ_3:8
canceled;
theorem :: POLYEQ_3:9
canceled;
theorem :: POLYEQ_3:10
canceled;
theorem Th11: :: POLYEQ_3:11
theorem :: POLYEQ_3:12
for
a,
b,
c,
d,
a',
b',
c',
d' being
Real st ( for
z being
complex number holds
Polynom a,
b,
c,
d,
z = Polynom a',
b',
c',
d',
z ) holds
(
a = a' &
b = b' &
c = c' &
d = d' )
theorem :: POLYEQ_3:13
canceled;
theorem :: POLYEQ_3:14
canceled;
theorem :: POLYEQ_3:15
for
b,
c,
d being
Real for
z being
Element of
COMPLEX st
b <> 0 &
delta b,
c,
d >= 0 &
Polynom 0 ,
b,
c,
d,
z = 0 & not
z = ((- c) + (sqrt (delta b,c,d))) / (2 * b) & not
z = ((- c) - (sqrt (delta b,c,d))) / (2 * b) holds
z = - (c / (2 * b))
theorem :: POLYEQ_3:16
for
b,
c,
d being
Real for
z being
Element of
COMPLEX st
b <> 0 &
delta b,
c,
d < 0 &
Polynom 0 ,
b,
c,
d,
z = 0 & not
z = (- (c / (2 * b))) + (((sqrt (- (delta b,c,d))) / (2 * b)) * <i> ) holds
z = (- (c / (2 * b))) + ((- ((sqrt (- (delta b,c,d))) / (2 * b))) * <i> )
theorem :: POLYEQ_3:17
theorem :: POLYEQ_3:18
for
a,
b,
c being
Real for
z being
Element of
COMPLEX st
a <> 0 &
delta a,
b,
c >= 0 &
Polynom a,
b,
c,
0 ,
z = 0 & not
z = ((- b) + (sqrt (delta a,b,c))) / (2 * a) & not
z = ((- b) - (sqrt (delta a,b,c))) / (2 * a) & not
z = - (b / (2 * a)) holds
z = 0
theorem :: POLYEQ_3:19
for
a,
b,
c being
Real for
z being
Element of
COMPLEX st
a <> 0 &
delta a,
b,
c < 0 &
Polynom a,
b,
c,
0 ,
z = 0 & not
z = (- (b / (2 * a))) + (((sqrt (- (delta a,b,c))) / (2 * a)) * <i> ) & not
z = (- (b / (2 * a))) + ((- ((sqrt (- (delta a,b,c))) / (2 * a))) * <i> ) holds
z = 0
theorem Th20: :: POLYEQ_3:20
theorem :: POLYEQ_3:21
theorem :: POLYEQ_3:22
theorem :: POLYEQ_3:23
theorem Th24: :: POLYEQ_3:24
theorem :: POLYEQ_3:25
canceled;
theorem :: POLYEQ_3:26
for
z1,
z2,
z3,
s1,
s2,
s3 being
Element of
COMPLEX st ( for
z being
Element of
COMPLEX holds
Polynom z1,
z2,
z3,
z = Polynom s1,
s2,
s3,
z ) holds
(
z1 = s1 &
z2 = s2 &
z3 = s3 )
theorem :: POLYEQ_3:27
theorem Th28: :: POLYEQ_3:28
theorem :: POLYEQ_3:29
theorem :: POLYEQ_3:30
theorem :: POLYEQ_3:31
theorem Th32: :: POLYEQ_3:32
theorem :: POLYEQ_3:33
canceled;
theorem :: POLYEQ_3:34
canceled;
theorem :: POLYEQ_3:35
theorem Th36: :: POLYEQ_3:36
theorem Th37: :: POLYEQ_3:37
theorem :: POLYEQ_3:38
canceled;
theorem :: POLYEQ_3:39
theorem :: POLYEQ_3:40
theorem :: POLYEQ_3:41
theorem :: POLYEQ_3:42
theorem :: POLYEQ_3:43
canceled;
theorem :: POLYEQ_3:44
canceled;
theorem :: POLYEQ_3:45
canceled;
theorem :: POLYEQ_3:46
canceled;
theorem :: POLYEQ_3:47
canceled;
theorem :: POLYEQ_3:48
canceled;
theorem :: POLYEQ_3:49
canceled;
theorem :: POLYEQ_3:50
canceled;
theorem :: POLYEQ_3:51
canceled;
theorem :: POLYEQ_3:52
canceled;
Th50:
for n being Nat st n > 0 holds
0 |^ n = 0
theorem Th53: :: POLYEQ_3:53
theorem :: POLYEQ_3:54
theorem Th55: :: POLYEQ_3:55
theorem Th56: :: POLYEQ_3:56
theorem :: POLYEQ_3:57
theorem :: POLYEQ_3:58
theorem :: POLYEQ_3:59
theorem :: POLYEQ_3:60
theorem :: POLYEQ_3:61
theorem :: POLYEQ_3:62
canceled;
theorem :: POLYEQ_3:63