environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, NAT_1, RELAT_1, ARYTM_3, TARSKI, ORDINAL4, PARTFUN1, XXREAL_0, FUNCT_1, SUBSET_1, STRUCT_0, BINOP_1, VECTSP_1, LATTICES, SUPINF_2, ARYTM_1, GROUP_1, CARD_1, MESFUNC1, COMPLFLD, COMPLEX1, CARD_3, POLYNOM1, POLYNOM3, SGRAPH1, INT_1, ALGSEQ_1, VECTSP_2, POLYNOM5, AFINSQ_1, POLYNOM2, FUNCT_4, FUNCOP_1, XCMPLX_0, SQUARE_1, HURWITZ;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, ALGSTR_0, VECTSP_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_D, XXREAL_0, FINSEQ_1, INT_1, NAT_1, FUNCOP_1, STRUCT_0, RLVECT_1, VFUNCT_1, GROUP_1, POLYNOM1, COMPLEX1, COMPLFLD, BINOP_1, NORMSP_1, ALGSEQ_1, FUNCT_4, POLYNOM3, POLYNOM4, POLYNOM5, VECTSP_1, SQUARE_1;
definitions ;
theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1, SQUARE_1, VECTSP_2, INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, TARSKI, FUNCT_4, POLYNOM3, XBOOLE_1, POLYNOM2, FUNCOP_1, XCMPLX_1, XCMPLX_0, COMPLFLD, POLYNOM5, XXREAL_0, ALGSTR_1, COMPLEX1, FINSEQ_2, POLYNOM1, FINSEQ_3, BHSP_1, NORMSP_1, ORDINAL1, PARTFUN1, XREAL_0, NAT_D;
schemes NAT_1, FUNCT_2, FINSEQ_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM3, POLYNOM4, POLYNOM5, FUNCOP_1, CARD_1, VFUNCT_1, FUNCT_2, MEMBERED;
constructors HIDDEN, BINOP_1, REAL_1, SQUARE_1, FINSOP_1, BINARITH, VECTSP_2, ALGSTR_1, POLYNOM4, POLYNOM5, NAT_D, RELSET_1, FVSUM_1, VFUNCT_1, ALGSEQ_1, BINOP_2;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities FINSEQ_1, POLYNOM3, COMPLEX1, SQUARE_1, FUNCOP_1;
expansions ;
Lm1:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of L
for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )
Lm2:
( Im (1_ F_Complex) = 0 & Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 0 )
Lm3:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds - (- p) = p
Lm4:
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for f being Element of (Polynom-Ring L) st f = p holds
- f = - p
Lm5:
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for p29 being Element of (Polynom-Ring L) st p29 = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
Lm6:
for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
Lm7:
for L being non empty ZeroStr
for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L
Lm8:
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
Lm9:
for L being non empty ZeroStr
for p being Polynomial of L holds deg p >= - 1
Lm10:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )
Lm11:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
Lm12:
for f, g, h being Polynomial of F_Complex st f = g *' h holds
for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f
Lm13:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) holds
(|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv
Lm14:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) )