begin
:: deftheorem defines Polynom POLYEQ_1:def 1 :
theorem
theorem
theorem
:: deftheorem defines Polynom POLYEQ_1:def 2 :
theorem Th4:
for
a,
b,
c,
a',
b',
c' being
complex number st ( for
x being
real number holds
Polynom a,
b,
c,
x = Polynom a',
b',
c',
x ) holds
(
a = a' &
b = b' &
c = c' )
theorem Th5:
for
a,
b,
c being
real number st
a <> 0 &
delta a,
b,
c >= 0 holds
for
x being
real number holds
( not
Polynom a,
b,
c,
x = 0 or
x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or
x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Quard POLYEQ_1:def 3 :
theorem
begin
:: deftheorem defines Polynom POLYEQ_1:def 4 :
registration
let a,
b,
c,
d,
x be
complex number ;
cluster Polynom a,
b,
c,
d,
x -> complex ;
coherence
Polynom a,b,c,d,x is complex
;
end;
registration
let a,
b,
c,
d,
x be
real number ;
cluster Polynom a,
b,
c,
d,
x -> real ;
coherence
Polynom a,b,c,d,x is real
;
end;
definition
let a,
b,
c,
d,
x be
Real;
Polynomredefine func Polynom a,
b,
c,
d,
x -> Real;
coherence
Polynom a,b,c,d,x is Real
by XREAL_0:def 1;
end;
theorem Th12:
for
a,
b,
c,
d,
a',
b',
c',
d' being
real number st ( for
x being
real number holds
Polynom a,
b,
c,
d,
x = Polynom a',
b',
c',
d',
x ) holds
(
a = a' &
b = b' &
c = c' &
d = d' )
:: deftheorem defines Tri POLYEQ_1:def 5 :
for
a,
x,
x1,
x2,
x3 being
real number holds
Tri a,
x1,
x2,
x3,
x = a * (((x - x1) * (x - x2)) * (x - x3));
registration
let a,
x,
x1,
x2,
x3 be
real number ;
cluster Tri a,
x1,
x2,
x3,
x -> real ;
coherence
Tri a,x1,x2,x3,x is real
;
end;
definition
let a,
x,
x1,
x2,
x3 be
Real;
Triredefine func Tri a,
x1,
x2,
x3,
x -> Real;
coherence
Tri a,x1,x2,x3,x is Real
by XREAL_0:def 1;
end;
theorem
for
a,
b,
c,
d,
x1,
x2,
x3 being
real number st
a <> 0 & ( for
x being
real number holds
Polynom a,
b,
c,
d,
x = Tri a,
x1,
x2,
x3,
x ) holds
(
b / a = - ((x1 + x2) + x3) &
c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) &
d / a = - ((x1 * x2) * x3) )
theorem Th14:
theorem Th15:
for
a,
b,
c,
d,
x being
real number st
a <> 0 &
Polynom a,
b,
c,
d,
x = 0 holds
for
a1,
a2,
a3,
h,
y being
real number st
y = x + (b / (3 * a)) &
h = - (b / (3 * a)) &
a1 = b / a &
a2 = c / a &
a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2 )) + ((((3 * (h ^2 )) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3)) = 0
theorem
for
a,
b,
c,
d,
x being
real number st
a <> 0 &
Polynom a,
b,
c,
d,
x = 0 holds
for
a1,
a2,
a3,
h,
y being
real number st
y = x + (b / (3 * a)) &
h = - (b / (3 * a)) &
a1 = b / a &
a2 = c / a &
a3 = d / a holds
(((y |^ 3) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0
theorem
theorem Th18:
theorem Th19:
theorem
for
b,
c,
d,
x being
real number st
b <> 0 &
delta b,
c,
d > 0 &
Polynom 0 ,
b,
c,
d,
x = 0 & not
x = ((- c) + (sqrt (delta b,c,d))) / (2 * b) holds
x = ((- c) - (sqrt (delta b,c,d))) / (2 * b)
theorem
for
a,
p,
c,
q,
d,
x being
real number st
a <> 0 &
p = c / a &
q = d / a &
Polynom a,
0 ,
c,
d,
x = 0 holds
for
u,
v being
real number st
x = u + v &
((3 * v) * u) + p = 0 & not
x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not
x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) holds
x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3)))))
theorem
for
a,
b,
c,
x being
real number st
a <> 0 &
delta a,
b,
c >= 0 &
Polynom a,
b,
c,
0 ,
x = 0 & not
x = 0 & not
x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) holds
x = ((- b) - (sqrt (delta a,b,c))) / (2 * a)
theorem