:: by Robert Milewski

::

:: Received August 21, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

Lm1: for x, y being Real st ( for c being Real st c > 0 & c < 1 holds

c * x >= y ) holds

y <= 0

by Th3;

theorem Th4: :: POLYNOM5:4

for p being FinSequence of REAL st ( for n being Element of NAT st n in dom p holds

p . n >= 0 ) holds

for i being Element of NAT st i in dom p holds

Sum p >= p . i

p . n >= 0 ) holds

for i being Element of NAT st i in dom p holds

Sum p >= p . i

proof end;

definition

let R be non empty multMagma ;

let z be Element of R;

let n be Nat;

coherence

(power R) . (z,n) is Element of R ;

end;
let z be Element of R;

let n be Nat;

coherence

(power R) . (z,n) is Element of R ;

:: deftheorem defines power POLYNOM5:def 1 :

for R being non empty multMagma

for z being Element of R

for n being Nat holds power (z,n) = (power R) . (z,n);

for R being non empty multMagma

for z being Element of R

for n being Nat holds power (z,n) = (power R) . (z,n);

theorem Th7: :: POLYNOM5:7

for z being Element of F_Complex st z <> 0. F_Complex holds

for n being Nat holds |.(power (z,n)).| = |.z.| to_power n

for n being Nat holds |.(power (z,n)).| = |.z.| to_power n

proof end;

definition

let p be FinSequence of the carrier of F_Complex;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len p & ( for n being Element of NAT st n in dom p holds

b_{1} /. n = |.(p /. n).| ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len p & ( for n being Element of NAT st n in dom p holds

b_{1} /. n = |.(p /. n).| ) & len b_{2} = len p & ( for n being Element of NAT st n in dom p holds

b_{2} /. n = |.(p /. n).| ) holds

b_{1} = b_{2}

end;
func |.p.| -> FinSequence of REAL means :Def2: :: POLYNOM5:def 2

( len it = len p & ( for n being Element of NAT st n in dom p holds

it /. n = |.(p /. n).| ) );

existence ( len it = len p & ( for n being Element of NAT st n in dom p holds

it /. n = |.(p /. n).| ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines |. POLYNOM5:def 2 :

for p being FinSequence of the carrier of F_Complex

for b_{2} being FinSequence of REAL holds

( b_{2} = |.p.| iff ( len b_{2} = len p & ( for n being Element of NAT st n in dom p holds

b_{2} /. n = |.(p /. n).| ) ) );

for p being FinSequence of the carrier of F_Complex

for b

( b

b

theorem :: POLYNOM5:13

for p being FinSequence of the carrier of F_Complex

for x being Element of F_Complex holds

( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )

for x being Element of F_Complex holds

( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )

proof end;

definition

let L be non empty right_complementable Abelian add-associative right_zeroed right_unital distributive commutative doubleLoopStr ;

let p be Polynomial of L;

let n be Nat;

coherence

(power (Polynom-Ring L)) . (p,n) is sequence of L

end;
let p be Polynomial of L;

let n be Nat;

coherence

(power (Polynom-Ring L)) . (p,n) is sequence of L

proof end;

:: deftheorem defines `^ POLYNOM5:def 3 :

for L being non empty right_complementable Abelian add-associative right_zeroed right_unital distributive commutative doubleLoopStr

for p being Polynomial of L

for n being Nat holds p `^ n = (power (Polynom-Ring L)) . (p,n);

for L being non empty right_complementable Abelian add-associative right_zeroed right_unital distributive commutative doubleLoopStr

for p being Polynomial of L

for n being Nat holds p `^ n = (power (Polynom-Ring L)) . (p,n);

registration

let L be non empty right_complementable Abelian add-associative right_zeroed right_unital distributive commutative doubleLoopStr ;

let p be Polynomial of L;

let n be Nat;

coherence

p `^ n is finite-Support

end;
let p be Polynomial of L;

let n be Nat;

coherence

p `^ n is finite-Support

proof end;

theorem Th15: :: POLYNOM5:15

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds p `^ 0 = 1_. L

for p being Polynomial of L holds p `^ 0 = 1_. L

proof end;

theorem :: POLYNOM5:16

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds p `^ 1 = p

for p being Polynomial of L holds p `^ 1 = p

proof end;

theorem :: POLYNOM5:17

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds p `^ 2 = p *' p

for p being Polynomial of L holds p `^ 2 = p *' p

proof end;

theorem :: POLYNOM5:18

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds p `^ 3 = (p *' p) *' p

for p being Polynomial of L holds p `^ 3 = (p *' p) *' p

proof end;

theorem Th19: :: POLYNOM5:19

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L

for n being Nat holds p `^ (n + 1) = (p `^ n) *' p

for p being Polynomial of L

for n being Nat holds p `^ (n + 1) = (p `^ n) *' p

proof end;

theorem Th20: :: POLYNOM5:20

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L

for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L

proof end;

theorem :: POLYNOM5:21

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for n being Nat holds (1_. L) `^ n = 1_. L

for n being Nat holds (1_. L) `^ n = 1_. L

proof end;

theorem Th22: :: POLYNOM5:22

for L being Field

for p being Polynomial of L

for x being Element of L

for n being Nat holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)

for p being Polynomial of L

for x being Element of L

for n being Nat holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)

proof end;

Lm2: for L being non empty ZeroStr

for p being AlgSequence of L st len p > 0 holds

p . ((len p) -' 1) <> 0. L

proof end;

theorem Th23: :: POLYNOM5:23

for L being domRing

for p being Polynomial of L st len p <> 0 holds

for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1

for p being Polynomial of L st len p <> 0 holds

for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1

proof end;

definition

let L be non empty multMagma ;

let p be sequence of L;

let v be Element of L;

ex b_{1} being sequence of L st

for n being Element of NAT holds b_{1} . n = v * (p . n)

for b_{1}, b_{2} being sequence of L st ( for n being Element of NAT holds b_{1} . n = v * (p . n) ) & ( for n being Element of NAT holds b_{2} . n = v * (p . n) ) holds

b_{1} = b_{2}

end;
let p be sequence of L;

let v be Element of L;

func v * p -> sequence of L means :Def4: :: POLYNOM5:def 4

for n being Element of NAT holds it . n = v * (p . n);

existence for n being Element of NAT holds it . n = v * (p . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines * POLYNOM5:def 4 :

for L being non empty multMagma

for p being sequence of L

for v being Element of L

for b_{4} being sequence of L holds

( b_{4} = v * p iff for n being Element of NAT holds b_{4} . n = v * (p . n) );

for L being non empty multMagma

for p being sequence of L

for v being Element of L

for b

( b

registration

let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;

let p be Polynomial of L;

let v be Element of L;

coherence

v * p is finite-Support

end;
let p be Polynomial of L;

let v be Element of L;

coherence

v * p is finite-Support

proof end;

theorem Th24: :: POLYNOM5:24

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for p being Polynomial of L holds len ((0. L) * p) = 0

for p being Polynomial of L holds len ((0. L) * p) = 0

proof end;

theorem Th25: :: POLYNOM5:25

for L being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L

for v being Element of L st v <> 0. L holds

len (v * p) = len p

for p being Polynomial of L

for v being Element of L st v <> 0. L holds

len (v * p) = len p

proof end;

theorem Th26: :: POLYNOM5:26

for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr

for p being sequence of L holds (0. L) * p = 0_. L

for p being sequence of L holds (0. L) * p = 0_. L

proof end;

theorem Th28: :: POLYNOM5:28

for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for v being Element of L holds v * (0_. L) = 0_. L

for v being Element of L holds v * (0_. L) = 0_. L

proof end;

theorem Th29: :: POLYNOM5:29

for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr

for v being Element of L holds v * (1_. L) = <%v%>

for v being Element of L holds v * (1_. L) = <%v%>

proof end;

theorem Th30: :: POLYNOM5:30

for L being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L

for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))

for p being Polynomial of L

for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))

proof end;

theorem Th31: :: POLYNOM5:31

for L being non empty right_complementable add-associative right_zeroed right-distributive unital doubleLoopStr

for p being Polynomial of L holds eval (p,(0. L)) = p . 0

for p being Polynomial of L holds eval (p,(0. L)) = p . 0

proof end;

definition

let L be non empty ZeroStr ;

let z0, z1 be Element of L;

coherence

((0_. L) +* (0,z0)) +* (1,z1) is sequence of L ;

end;
let z0, z1 be Element of L;

coherence

((0_. L) +* (0,z0)) +* (1,z1) is sequence of L ;

:: deftheorem defines <% POLYNOM5:def 5 :

for L being non empty ZeroStr

for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* (0,z0)) +* (1,z1);

for L being non empty ZeroStr

for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* (0,z0)) +* (1,z1);

theorem Th32: :: POLYNOM5:32

for L being non empty ZeroStr

for z0 being Element of L holds

( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds

<%z0%> . n = 0. L ) )

for z0 being Element of L holds

( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds

<%z0%> . n = 0. L ) )

proof end;

theorem Th35: :: POLYNOM5:35

for L being non empty right_complementable add-associative right_zeroed well-unital distributive associative commutative domRing-like doubleLoopStr

for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>

for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>

proof end;

theorem Th36: :: POLYNOM5:36

for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for n being Nat holds <%x%> `^ n = <%(power (x,n))%>

for x being Element of L

for n being Nat holds <%x%> `^ n = <%(power (x,n))%>

proof end;

theorem :: POLYNOM5:37

for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr

for z0, x being Element of L holds eval (<%z0%>,x) = z0

for z0, x being Element of L holds eval (<%z0%>,x) = z0

proof end;

theorem Th38: :: POLYNOM5:38

for L being non empty ZeroStr

for z0, z1 being Element of L holds

( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds

<%z0,z1%> . n = 0. L ) )

for z0, z1 being Element of L holds

( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds

<%z0,z1%> . n = 0. L ) )

proof end;

registration

let L be non empty ZeroStr ;

let z0, z1 be Element of L;

coherence

<%z0,z1%> is finite-Support

end;
let z0, z1 be Element of L;

coherence

<%z0,z1%> is finite-Support

proof end;

theorem Th44: :: POLYNOM5:44

for L being non empty right_complementable add-associative right_zeroed left-distributive unital doubleLoopStr

for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)

for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)

proof end;

theorem :: POLYNOM5:45

for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr

for z0, z1, x being Element of L holds eval (<%z0,(0. L)%>,x) = z0

for z0, z1, x being Element of L holds eval (<%z0,(0. L)%>,x) = z0

proof end;

theorem :: POLYNOM5:46

for L being non empty right_complementable add-associative right_zeroed left-distributive unital doubleLoopStr

for z0, z1, x being Element of L holds eval (<%(0. L),z1%>,x) = z1 * x

for z0, z1, x being Element of L holds eval (<%(0. L),z1%>,x) = z1 * x

proof end;

theorem Th47: :: POLYNOM5:47

for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr

for z0, z1, x being Element of L holds eval (<%z0,(1. L)%>,x) = z0 + x

for z0, z1, x being Element of L holds eval (<%z0,(1. L)%>,x) = z0 + x

proof end;

theorem :: POLYNOM5:48

for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr

for z0, z1, x being Element of L holds eval (<%(0. L),(1. L)%>,x) = x

for z0, z1, x being Element of L holds eval (<%(0. L),(1. L)%>,x) = x

proof end;

definition

let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr ;

let p, q be Polynomial of L;

ex b_{1} being Polynomial of L ex F being FinSequence of the carrier of (Polynom-Ring L) st

( b_{1} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )

for b_{1}, b_{2} being Polynomial of L st ex F being FinSequence of the carrier of (Polynom-Ring L) st

( b_{1} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) & ex F being FinSequence of the carrier of (Polynom-Ring L) st

( b_{2} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) holds

b_{1} = b_{2}

end;
let p, q be Polynomial of L;

func Subst (p,q) -> Polynomial of L means :Def6: :: POLYNOM5:def 6

ex F being FinSequence of the carrier of (Polynom-Ring L) st

( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) );

existence ex F being FinSequence of the carrier of (Polynom-Ring L) st

( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) );

ex b

( b

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )

proof end;

uniqueness for b

( b

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) & ex F being FinSequence of the carrier of (Polynom-Ring L) st

( b

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) holds

b

proof end;

:: deftheorem Def6 defines Subst POLYNOM5:def 6 :

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p, q, b_{4} being Polynomial of L holds

( b_{4} = Subst (p,q) iff ex F being FinSequence of the carrier of (Polynom-Ring L) st

( b_{4} = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p, q, b

( b

( b

F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );

theorem Th49: :: POLYNOM5:49

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds Subst ((0_. L),p) = 0_. L

for p being Polynomial of L holds Subst ((0_. L),p) = 0_. L

proof end;

theorem :: POLYNOM5:50

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr

for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>

for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>

proof end;

theorem :: POLYNOM5:51

for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L

for x being Element of L holds len (Subst (p,<%x%>)) <= 1

for p being Polynomial of L

for x being Element of L holds len (Subst (p,<%x%>)) <= 1

proof end;

theorem Th52: :: POLYNOM5:52

for L being Field

for p, q being Polynomial of L st len p <> 0 & len q > 1 holds

len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2

for p, q being Polynomial of L st len p <> 0 & len q > 1 holds

len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2

proof end;

theorem Th53: :: POLYNOM5:53

for L being Field

for p, q being Polynomial of L

for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))

for p, q being Polynomial of L

for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))

proof end;

definition
end;

:: deftheorem defines is_a_root_of POLYNOM5:def 7 :

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for x being Element of L holds

( x is_a_root_of p iff eval (p,x) = 0. L );

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for x being Element of L holds

( x is_a_root_of p iff eval (p,x) = 0. L );

:: deftheorem defines with_roots POLYNOM5:def 8 :

for L being non empty unital doubleLoopStr

for p being Polynomial of L holds

( p is with_roots iff ex x being Element of L st x is_a_root_of p );

for L being non empty unital doubleLoopStr

for p being Polynomial of L holds

( p is with_roots iff ex x being Element of L st x is_a_root_of p );

theorem :: POLYNOM5:55

for L being non empty unital doubleLoopStr

for x being Element of L holds x is_a_root_of 0_. L by POLYNOM4:17;

for x being Element of L holds x is_a_root_of 0_. L by POLYNOM4:17;

registration

let L be non empty unital doubleLoopStr ;

ex b_{1} being Polynomial of L st b_{1} is with_roots

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support with_roots for Element of K29(K30(NAT, the carrier of L));

existence ex b

proof end;

definition

let L be non empty unital doubleLoopStr ;

end;
attr L is algebraic-closed means :: POLYNOM5:def 9

for p being Polynomial of L st len p > 1 holds

p is with_roots ;

for p being Polynomial of L st len p > 1 holds

p is with_roots ;

:: deftheorem defines algebraic-closed POLYNOM5:def 9 :

for L being non empty unital doubleLoopStr holds

( L is algebraic-closed iff for p being Polynomial of L st len p > 1 holds

p is with_roots );

for L being non empty unital doubleLoopStr holds

( L is algebraic-closed iff for p being Polynomial of L st len p > 1 holds

p is with_roots );

definition

let L be non empty unital doubleLoopStr ;

let p be Polynomial of L;

ex b_{1} being Subset of L st

for x being Element of L holds

( x in b_{1} iff x is_a_root_of p )

for b_{1}, b_{2} being Subset of L st ( for x being Element of L holds

( x in b_{1} iff x is_a_root_of p ) ) & ( for x being Element of L holds

( x in b_{2} iff x is_a_root_of p ) ) holds

b_{1} = b_{2}

end;
let p be Polynomial of L;

func Roots p -> Subset of L means :Def10: :: POLYNOM5:def 10

for x being Element of L holds

( x in it iff x is_a_root_of p );

existence for x being Element of L holds

( x in it iff x is_a_root_of p );

ex b

for x being Element of L holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines Roots POLYNOM5:def 10 :

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for b_{3} being Subset of L holds

( b_{3} = Roots p iff for x being Element of L holds

( x in b_{3} iff x is_a_root_of p ) );

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for b

( b

( x in b

definition

let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;

let p be Polynomial of L;

ex b_{1} being sequence of L st

for n being Element of NAT holds b_{1} . n = (p . n) / (p . ((len p) -' 1))

for b_{1}, b_{2} being sequence of L st ( for n being Element of NAT holds b_{1} . n = (p . n) / (p . ((len p) -' 1)) ) & ( for n being Element of NAT holds b_{2} . n = (p . n) / (p . ((len p) -' 1)) ) holds

b_{1} = b_{2}

end;
let p be Polynomial of L;

func NormPolynomial p -> sequence of L means :Def11: :: POLYNOM5:def 11

for n being Element of NAT holds it . n = (p . n) / (p . ((len p) -' 1));

existence for n being Element of NAT holds it . n = (p . n) / (p . ((len p) -' 1));

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines NormPolynomial POLYNOM5:def 11 :

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L

for b_{3} being sequence of L holds

( b_{3} = NormPolynomial p iff for n being Element of NAT holds b_{3} . n = (p . n) / (p . ((len p) -' 1)) );

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L

for b

( b

registration

let L be non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;

let p be Polynomial of L;

coherence

NormPolynomial p is finite-Support

end;
let p be Polynomial of L;

coherence

NormPolynomial p is finite-Support

proof end;

theorem Th56: :: POLYNOM5:56

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for p being Polynomial of L st len p <> 0 holds

(NormPolynomial p) . ((len p) -' 1) = 1. L

for p being Polynomial of L st len p <> 0 holds

(NormPolynomial p) . ((len p) -' 1) = 1. L

proof end;

theorem Th58: :: POLYNOM5:58

for L being Field

for p being Polynomial of L st len p <> 0 holds

for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))

for p being Polynomial of L st len p <> 0 holds

for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))

proof end;

theorem Th59: :: POLYNOM5:59

for L being Field

for p being Polynomial of L st len p <> 0 holds

for x being Element of L holds

( x is_a_root_of p iff x is_a_root_of NormPolynomial p )

for p being Polynomial of L st len p <> 0 holds

for x being Element of L holds

( x is_a_root_of p iff x is_a_root_of NormPolynomial p )

proof end;

theorem Th60: :: POLYNOM5:60

for L being Field

for p being Polynomial of L st len p <> 0 holds

( p is with_roots iff NormPolynomial p is with_roots )

for p being Polynomial of L st len p <> 0 holds

( p is with_roots iff NormPolynomial p is with_roots )

proof end;

theorem :: POLYNOM5:61

for L being Field

for p being Polynomial of L st len p <> 0 holds

Roots p = Roots (NormPolynomial p)

for p being Polynomial of L st len p <> 0 holds

Roots p = Roots (NormPolynomial p)

proof end;

definition

let L be non empty unital multMagma ;

let x be Element of L;

let n be Nat;

ex b_{1} being Function of L,L st

for y being Element of L holds b_{1} . y = x * (power (y,n))

for b_{1}, b_{2} being Function of L,L st ( for y being Element of L holds b_{1} . y = x * (power (y,n)) ) & ( for y being Element of L holds b_{2} . y = x * (power (y,n)) ) holds

b_{1} = b_{2}

end;
let x be Element of L;

let n be Nat;

func FPower (x,n) -> Function of L,L means :Def12: :: POLYNOM5:def 12

for y being Element of L holds it . y = x * (power (y,n));

existence for y being Element of L holds it . y = x * (power (y,n));

ex b

for y being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines FPower POLYNOM5:def 12 :

for L being non empty unital multMagma

for x being Element of L

for n being Nat

for b_{4} being Function of L,L holds

( b_{4} = FPower (x,n) iff for y being Element of L holds b_{4} . y = x * (power (y,n)) );

for L being non empty unital multMagma

for x being Element of L

for n being Nat

for b

( b

theorem Th66: :: POLYNOM5:66

for L being non empty unital multMagma

for x being Element of L holds FPower (x,0) = the carrier of L --> x

for x being Element of L holds FPower (x,0) = the carrier of L --> x

proof end;

theorem :: POLYNOM5:67

for x being Element of F_Complex ex x1 being Element of COMPLEX st

( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )

( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )

proof end;

theorem :: POLYNOM5:68

for x being Element of F_Complex ex x1 being Element of COMPLEX st

( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )

( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )

proof end;

theorem Th69: :: POLYNOM5:69

for x being Element of F_Complex

for n being Nat ex f being Function of COMPLEX,COMPLEX st

( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )

for n being Nat ex f being Function of COMPLEX,COMPLEX st

( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )

proof end;

theorem Th70: :: POLYNOM5:70

for x being Element of F_Complex

for n being Nat ex f being Function of COMPLEX,COMPLEX st

( f = FPower (x,n) & f is_continuous_on COMPLEX )

for n being Nat ex f being Function of COMPLEX,COMPLEX st

( f = FPower (x,n) & f is_continuous_on COMPLEX )

proof end;

definition

let L be non empty well-unital doubleLoopStr ;

let p be Polynomial of L;

ex b_{1} being Function of L,L st

for x being Element of L holds b_{1} . x = eval (p,x)

for b_{1}, b_{2} being Function of L,L st ( for x being Element of L holds b_{1} . x = eval (p,x) ) & ( for x being Element of L holds b_{2} . x = eval (p,x) ) holds

b_{1} = b_{2}

end;
let p be Polynomial of L;

func Polynomial-Function (L,p) -> Function of L,L means :Def13: :: POLYNOM5:def 13

for x being Element of L holds it . x = eval (p,x);

existence for x being Element of L holds it . x = eval (p,x);

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines Polynomial-Function POLYNOM5:def 13 :

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L

for b_{3} being Function of L,L holds

( b_{3} = Polynomial-Function (L,p) iff for x being Element of L holds b_{3} . x = eval (p,x) );

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L

for b

( b

theorem Th71: :: POLYNOM5:71

for p being Polynomial of F_Complex ex f being Function of COMPLEX,COMPLEX st

( f = Polynomial-Function (F_Complex,p) & f is_continuous_on COMPLEX )

( f = Polynomial-Function (F_Complex,p) & f is_continuous_on COMPLEX )

proof end;

theorem Th72: :: POLYNOM5:72

for p being Polynomial of F_Complex st len p > 2 & |.(p . ((len p) -' 1)).| = 1 holds

for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = |.(p . (n -' 1)).| ) holds

for z being Element of F_Complex st |.z.| > Sum F holds

|.(eval (p,z)).| > |.(p . 0).| + 1

for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds

F . n = |.(p . (n -' 1)).| ) holds

for z being Element of F_Complex st |.z.| > Sum F holds

|.(eval (p,z)).| > |.(p . 0).| + 1

proof end;

theorem Th73: :: POLYNOM5:73

for p being Polynomial of F_Complex st len p > 2 holds

ex z0 being Element of F_Complex st

for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|

ex z0 being Element of F_Complex st

for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|

proof end;

:: Fundamental Theorem of Algebra

registration
end;

registration

ex b_{1} being non empty well-unital doubleLoopStr st

( b_{1} is algebraic-closed & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian & b_{1} is commutative & b_{1} is associative & b_{1} is distributive & b_{1} is almost_left_invertible & not b_{1} is degenerated )
end;

cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed right_unital well-unital distributive left_unital unital associative commutative algebraic-closed for doubleLoopStr ;

existence ex b

( b

proof end;