begin
:: deftheorem defines ^2 POLYEQ_3:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
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:
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
theorem
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 :
Lm1:
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
(((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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem
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
canceled;
theorem
canceled;
theorem
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
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
theorem
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
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:
theorem
theorem
theorem
theorem Th24:
begin
theorem
canceled;
theorem
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
theorem Th28:
theorem
theorem
theorem
theorem Th32:
theorem
canceled;
theorem
canceled;
theorem
theorem Th36:
theorem Th37:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
Lm2:
for n being Nat st n > 0 holds
0 |^ n = 0
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem