environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, RELAT_1, ARYTM_3, SQUARE_1, COMPLEX1, ARYTM_1, XCMPLX_0, POLYEQ_1, CARD_1, FUNCT_3, XXREAL_0, NEWTON, POWER, NAT_1, SIN_COS, COMPTRIG, FUNCT_1, POLYEQ_3;
notations HIDDEN, SUBSET_1, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, REAL_1, COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, QUIN_1, POWER, NAT_1, SIN_COS, COMPTRIG;
definitions ;
theorems COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, COMPTRIG, NAT_1, POWER, SIN_COS, SIN_COS2, XCMPLX_0, XCMPLX_1, XREAL_1;
schemes NAT_1, COMPTRIG;
registrations XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON, POLYEQ_1, VALUED_0, RELSET_1, POWER, SIN_COS, QUIN_1, ORDINAL1, CARD_1;
constructors HIDDEN, FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, QUIN_1, PREPOWER, POWER, POLYEQ_1, BINARITH, SIN_COS, COMPTRIG, VALUED_1, BINOP_2, NAT_D, XREAL_0, ABIAN, NEWTON, XCMPLX_0;
requirements HIDDEN, ARITHM, SUBSET, REAL, BOOLE, NUMERALS;
equalities POLYEQ_1, SQUARE_1, XCMPLX_0, QUIN_1;
expansions ;
theorem Th1:
for
a,
b,
c being
Real for
z being
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 Th2:
for
a,
b,
c being
Real for
z being
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
for
a,
b,
c being
Real for
z,
z1,
z2 being
Complex st
a <> 0 & ( for
z being
Complex holds
Polynom (
a,
b,
c,
z)
= Quard (
a,
z1,
z2,
z) ) holds
(
b / a = - (z1 + z2) &
c / a = z1 * z2 )
Lm1:
for z being Complex holds z |^ 2 = z * z
definition
let a,
b,
c,
d,
z be
Complex;
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;
theorem
for
a,
b,
c,
d,
a9,
b9,
c9,
d9 being
Real st ( for
z being
Complex holds
Polynom (
a,
b,
c,
d,
z)
= Polynom (
a9,
b9,
c9,
d9,
z) ) holds
(
a = a9 &
b = b9 &
c = c9 &
d = d9 )
theorem
for
b,
c,
d being
Real for
z being
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
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
for
a,
b,
c being
Real for
z being
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
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
for
z1,
z2,
z3,
s1,
s2,
s3 being
Complex st ( for
z being
Complex holds
Polynom (
z1,
z2,
z3,
z)
= Polynom (
s1,
s2,
s3,
z) ) holds
(
z1 = s1 &
z2 = s2 &
z3 = s3 )
Lm2:
for n being Nat st n > 0 holds
0 |^ n = 0