:: by Piotr Rudnicki

::

:: Received December 30, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th1: :: UPROOTS:1

for f being FinSequence of NAT st ( for i being Element of NAT st i in dom f holds

f . i <> 0 ) holds

( Sum f = len f iff f = (len f) |-> 1 )

f . i <> 0 ) holds

( Sum f = len f iff f = (len f) |-> 1 )

proof end;

theorem Th2: :: UPROOTS:2

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds

r . k = 0. L ) holds

Sum r = (r /. 1) + (r /. 2)

for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds

r . k = 0. L ) holds

Sum r = (r /. 1) + (r /. 2)

proof end;

definition

let X be set ;

let S be finite Subset of X;

let n be Element of NAT ;

correctness

coherence

(EmptyBag X) +* (S --> n) is Element of Bags X;

end;
let S be finite Subset of X;

let n be Element of NAT ;

correctness

coherence

(EmptyBag X) +* (S --> n) is Element of Bags X;

proof end;

:: deftheorem defines -bag UPROOTS:def 2 :

for X being set

for S being finite Subset of X

for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n);

for X being set

for S being finite Subset of X

for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n);

::$CT 3

theorem Th3: :: UPROOTS:6

for X being set

for S being finite Subset of X

for n being Element of NAT

for i being object st not i in S holds

((S,n) -bag) . i = 0

for S being finite Subset of X

for n being Element of NAT

for i being object st not i in S holds

((S,n) -bag) . i = 0

proof end;

theorem Th4: :: UPROOTS:7

for X being set

for S being finite Subset of X

for n being Element of NAT

for i being set st i in S holds

((S,n) -bag) . i = n

for S being finite Subset of X

for n being Element of NAT

for i being set st i in S holds

((S,n) -bag) . i = n

proof end;

theorem Th5: :: UPROOTS:8

for X being set

for S being finite Subset of X

for n being Element of NAT st n <> 0 holds

support ((S,n) -bag) = S

for S being finite Subset of X

for n being Element of NAT st n <> 0 holds

support ((S,n) -bag) = S

proof end;

theorem :: UPROOTS:9

for X being set

for S being finite Subset of X

for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

for S being finite Subset of X

for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

proof end;

theorem Th7: :: UPROOTS:10

for X being set

for S, T being finite Subset of X

for n being Element of NAT st S misses T holds

((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)

for S, T being finite Subset of X

for n being Element of NAT st S misses T holds

((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)

proof end;

definition

let A be set ;

let b be Rbag of A;

ex b_{1} being Real ex f being FinSequence of REAL st

( b_{1} = Sum f & f = b * (canFS (support b)) )

for b_{1}, b_{2} being Real st ex f being FinSequence of REAL st

( b_{1} = Sum f & f = b * (canFS (support b)) ) & ex f being FinSequence of REAL st

( b_{2} = Sum f & f = b * (canFS (support b)) ) holds

b_{1} = b_{2}
;

end;
let b be Rbag of A;

func Sum b -> Real means :Def2: :: UPROOTS:def 3

ex f being FinSequence of REAL st

( it = Sum f & f = b * (canFS (support b)) );

existence ex f being FinSequence of REAL st

( it = Sum f & f = b * (canFS (support b)) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def2 defines Sum UPROOTS:def 3 :

for A being set

for b being Rbag of A

for b_{3} being Real holds

( b_{3} = Sum b iff ex f being FinSequence of REAL st

( b_{3} = Sum f & f = b * (canFS (support b)) ) );

for A being set

for b being Rbag of A

for b

( b

( b

definition

let A be set ;

let b be bag of A;

Sum b is Element of NAT

for b_{1} being Element of NAT holds

( b_{1} = Sum b iff ex f being FinSequence of NAT st

( b_{1} = Sum f & f = b * (canFS (support b)) ) )

end;
let b be bag of A;

:: original: Sum

redefine func degree b -> Element of NAT means :Def3: :: UPROOTS:def 4

ex f being FinSequence of NAT st

( it = Sum f & f = b * (canFS (support b)) );

coherence redefine func degree b -> Element of NAT means :Def3: :: UPROOTS:def 4

ex f being FinSequence of NAT st

( it = Sum f & f = b * (canFS (support b)) );

Sum b is Element of NAT

proof end;

compatibility for b

( b

( b

proof end;

:: deftheorem Def3 defines degree UPROOTS:def 4 :

for A being set

for b being bag of A

for b_{3} being Element of NAT holds

( b_{3} = degree b iff ex f being FinSequence of NAT st

( b_{3} = Sum f & f = b * (canFS (support b)) ) );

for A being set

for b being bag of A

for b

( b

( b

theorem Th10: :: UPROOTS:13

for A being set

for S being finite Subset of A

for b being bag of A holds

( ( S = support b & degree b = card S ) iff b = (S,1) -bag )

for S being finite Subset of A

for b being bag of A holds

( ( S = support b & degree b = card S ) iff b = (S,1) -bag )

proof end;

theorem Th11: :: UPROOTS:14

for A being set

for S being finite Subset of A

for b being Rbag of A st support b c= S holds

ex f being FinSequence of REAL st

( f = b * (canFS S) & Sum b = Sum f )

for S being finite Subset of A

for b being Rbag of A st support b c= S holds

ex f being FinSequence of REAL st

( f = b * (canFS S) & Sum b = Sum f )

proof end;

theorem Th13: :: UPROOTS:16

for L being non empty unital associative commutative multMagma

for f, g being FinSequence of L

for p being Permutation of (dom f) st g = f * p holds

Product g = Product f

for f, g being FinSequence of L

for p being Permutation of (dom f) st g = f * p holds

Product g = Product f

proof end;

:: deftheorem Def4 defines non-zero UPROOTS:def 5 :

for L being non empty ZeroStr

for p being Polynomial of L holds

( p is non-zero iff p <> 0_. L );

for L being non empty ZeroStr

for p being Polynomial of L holds

( p is non-zero iff p <> 0_. L );

registration

let L be non trivial ZeroStr ;

ex b_{1} being Polynomial of L st b_{1} is non-zero

end;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support non-zero for Element of bool [:NAT, the carrier of L:];

existence ex b

proof end;

registration

let L be non empty non degenerated multLoopStr_0 ;

let x be Element of L;

correctness

coherence

<%x,(1. L)%> is non-zero ;

end;
let x be Element of L;

correctness

coherence

<%x,(1. L)%> is non-zero ;

proof end;

theorem Th15: :: UPROOTS:18

for L being non empty ZeroStr

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

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

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

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

proof end;

theorem Th16: :: UPROOTS:19

for L being non empty ZeroStr

for p being AlgSequence of L st len p = 1 holds

( p = <%(p . 0)%> & p . 0 <> 0. L )

for p being AlgSequence of L st len p = 1 holds

( p = <%(p . 0)%> & p . 0 <> 0. L )

proof end;

theorem Th17: :: UPROOTS:20

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

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

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

proof end;

registration

ex b_{1} being non empty 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 domRing-like & not b_{1} is degenerated )
end;

cluster non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed unital associative commutative domRing-like algebraic-closed for doubleLoopStr ;

existence ex b

( b

proof end;

theorem Th18: :: UPROOTS:21

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

for p, q being Polynomial of L holds

( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

for p, q being Polynomial of L holds

( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

proof end;

registration

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

correctness

coherence

Polynom-Ring L is domRing-like ;

end;
correctness

coherence

Polynom-Ring L is domRing-like ;

proof end;

registration

let L be domRing;

let p, q be non-zero Polynomial of L;

correctness

coherence

p *' q is non-zero ;

by Th18;

end;
let p, q be non-zero Polynomial of L;

correctness

coherence

p *' q is non-zero ;

by Th18;

theorem :: UPROOTS:22

for L being non degenerated comRing

for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)

for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)

proof end;

theorem Th21: :: UPROOTS:24

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

for p being Polynomial of L

for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

for p being Polynomial of L

for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

proof end;

theorem Th22: :: UPROOTS:25

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

for p, q being Polynomial of L

for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds

p - q = pc - qc

for p, q being Polynomial of L

for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds

p - q = pc - qc

proof end;

theorem Th23: :: UPROOTS:26

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

for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)

for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)

proof end;

theorem Th24: :: UPROOTS:27

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

for p, q being Polynomial of L st p - q = 0_. L holds

p = q

for p, q being Polynomial of L st p - q = 0_. L holds

p = q

proof end;

theorem Th25: :: UPROOTS:28

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

for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds

q = r

for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds

q = r

proof end;

theorem Th26: :: UPROOTS:29

for L being domRing

for n being Element of NAT

for p being Polynomial of L st p <> 0_. L holds

p `^ n <> 0_. L

for n being Element of NAT

for p being Polynomial of L st p <> 0_. L holds

p `^ n <> 0_. L

proof end;

theorem Th27: :: UPROOTS:30

for L being comRing

for i, j being Nat

for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)

for i, j being Nat

for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)

proof end;

theorem :: UPROOTS:32

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

for p being Polynomial of L holds p *' <%(1. L)%> = p

for p being Polynomial of L holds p *' <%(1. L)%> = p

proof end;

theorem Th30: :: UPROOTS:33

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

for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds

len (p *' q) = 0

for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds

len (p *' q) = 0

proof end;

theorem Th31: :: UPROOTS:34

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

for p, q being Polynomial of L st p *' q is non-zero holds

( p is non-zero & q is non-zero )

for p, q being Polynomial of L st p *' q is non-zero holds

( p is non-zero & q is non-zero )

proof end;

theorem :: UPROOTS:35

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

for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds

0 < len (p *' q)

for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds

0 < len (p *' q)

proof end;

theorem Th33: :: UPROOTS:36

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

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

len p < len (p *' q)

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

len p < len (p *' q)

proof end;

theorem Th34: :: UPROOTS:37

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

for a, b being Element of L

for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

for a, b being Element of L

for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

proof end;

theorem Th35: :: UPROOTS:38

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

for r being Element of L

for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1

for r being Element of L

for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1

proof end;

theorem Th36: :: UPROOTS:39

for L being non degenerated comRing

for x being Element of L

for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

for x being Element of L

for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

proof end;

registration

let L be non degenerated comRing;

let x be Element of L;

let n be Nat;

correctness

coherence

<%x,(1. L)%> `^ n is non-zero ;

end;
let x be Element of L;

let n be Nat;

correctness

coherence

<%x,(1. L)%> `^ n is non-zero ;

proof end;

theorem Th37: :: UPROOTS:40

for L being non degenerated comRing

for x being Element of L

for q being non-zero Polynomial of L

for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)

for x being Element of L

for q being non-zero Polynomial of L

for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)

proof end;

theorem Th38: :: UPROOTS:41

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

for r being Element of L

for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

for r being Element of L

for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

proof end;

definition

let L be non empty ZeroStr ;

let p be Polynomial of L;

let n be Nat;

ex b_{1} being Polynomial of L st

for i being Nat holds b_{1} . i = p . (n + i)

for b_{1}, b_{2} being Polynomial of L st ( for i being Nat holds b_{1} . i = p . (n + i) ) & ( for i being Nat holds b_{2} . i = p . (n + i) ) holds

b_{1} = b_{2}

end;
let p be Polynomial of L;

let n be Nat;

func poly_shift (p,n) -> Polynomial of L means :Def5: :: UPROOTS:def 6

for i being Nat holds it . i = p . (n + i);

existence for i being Nat holds it . i = p . (n + i);

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines poly_shift UPROOTS:def 6 :

for L being non empty ZeroStr

for p being Polynomial of L

for n being Nat

for b_{4} being Polynomial of L holds

( b_{4} = poly_shift (p,n) iff for i being Nat holds b_{4} . i = p . (n + i) );

for L being non empty ZeroStr

for p being Polynomial of L

for n being Nat

for b

( b

theorem Th40: :: UPROOTS:43

for L being non empty ZeroStr

for n being Element of NAT

for p being Polynomial of L st n >= len p holds

poly_shift (p,n) = 0_. L

for n being Element of NAT

for p being Polynomial of L st n >= len p holds

poly_shift (p,n) = 0_. L

proof end;

theorem Th41: :: UPROOTS:44

for L being non empty non degenerated multLoopStr_0

for n being Element of NAT

for p being Polynomial of L st n <= len p holds

(len (poly_shift (p,n))) + n = len p

for n being Element of NAT

for p being Polynomial of L st n <= len p holds

(len (poly_shift (p,n))) + n = len p

proof end;

theorem Th42: :: UPROOTS:45

for L being non degenerated comRing

for x being Element of L

for n being Element of NAT

for p being Polynomial of L st n < len p holds

eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)

for x being Element of L

for n being Element of NAT

for p being Polynomial of L st n < len p holds

eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)

proof end;

definition

let L be non degenerated comRing;

let r be Element of L;

let p be Polynomial of L;

assume A1: r is_a_root_of p ;

( ( len p > 0 implies ex b_{1} being Polynomial of L st

( (len b_{1}) + 1 = len p & ( for i being Nat holds b_{1} . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) & ( not len p > 0 implies ex b_{1} being Polynomial of L st b_{1} = 0_. L ) )

for b_{1}, b_{2} being Polynomial of L holds

( ( len p > 0 & (len b_{1}) + 1 = len p & ( for i being Nat holds b_{1} . i = eval ((poly_shift (p,(i + 1))),r) ) & (len b_{2}) + 1 = len p & ( for i being Nat holds b_{2} . i = eval ((poly_shift (p,(i + 1))),r) ) implies b_{1} = b_{2} ) & ( not len p > 0 & b_{1} = 0_. L & b_{2} = 0_. L implies b_{1} = b_{2} ) )

for b_{1} being Polynomial of L holds verum
;

end;
let r be Element of L;

let p be Polynomial of L;

assume A1: r is_a_root_of p ;

func poly_quotient (p,r) -> Polynomial of L means :Def6: :: UPROOTS:def 7

( (len it) + 1 = len p & ( for i being Nat holds it . i = eval ((poly_shift (p,(i + 1))),r) ) ) if len p > 0

otherwise it = 0_. L;

existence ( (len it) + 1 = len p & ( for i being Nat holds it . i = eval ((poly_shift (p,(i + 1))),r) ) ) if len p > 0

otherwise it = 0_. L;

( ( len p > 0 implies ex b

( (len b

proof end;

uniqueness for b

( ( len p > 0 & (len b

proof end;

consistency for b

:: deftheorem Def6 defines poly_quotient UPROOTS:def 7 :

for L being non degenerated comRing

for r being Element of L

for p being Polynomial of L st r is_a_root_of p holds

for b_{4} being Polynomial of L holds

( ( len p > 0 implies ( b_{4} = poly_quotient (p,r) iff ( (len b_{4}) + 1 = len p & ( for i being Nat holds b_{4} . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) & ( not len p > 0 implies ( b_{4} = poly_quotient (p,r) iff b_{4} = 0_. L ) ) );

for L being non degenerated comRing

for r being Element of L

for p being Polynomial of L st r is_a_root_of p holds

for b

( ( len p > 0 implies ( b

theorem Th44: :: UPROOTS:47

for L being non degenerated comRing

for r being Element of L

for p being non-zero Polynomial of L st r is_a_root_of p holds

len (poly_quotient (p,r)) > 0

for r being Element of L

for p being non-zero Polynomial of L st r is_a_root_of p holds

len (poly_quotient (p,r)) > 0

proof end;

theorem Th45: :: UPROOTS:48

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

for x being Element of L holds Roots <%(- x),(1. L)%> = {x}

for x being Element of L holds Roots <%(- x),(1. L)%> = {x}

proof end;

theorem Th46: :: UPROOTS:49

for L being non trivial comRing

for x being Element of L

for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds

x is_a_root_of p

for x being Element of L

for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds

x is_a_root_of p

proof end;

theorem Th47: :: UPROOTS:50

for L being non degenerated comRing

for r being Element of L

for p being Polynomial of L st r is_a_root_of p holds

p = <%(- r),(1. L)%> *' (poly_quotient (p,r))

for r being Element of L

for p being Polynomial of L st r is_a_root_of p holds

p = <%(- r),(1. L)%> *' (poly_quotient (p,r))

proof end;

theorem :: UPROOTS:51

for L being non degenerated comRing

for r being Element of L

for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds

r is_a_root_of p

for r being Element of L

for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds

r is_a_root_of p

proof end;

Lm1: now :: thesis: for L being domRing

for p being non-zero Polynomial of L holds

( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

for p being non-zero Polynomial of L holds

( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

let L be domRing; :: thesis: for p being non-zero Polynomial of L holds

( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

let p be non-zero Polynomial of L; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

defpred S_{1}[ Nat] means for p being Polynomial of L st len p = $1 holds

( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) );

p <> 0_. L by Def4;

then len p <> 0 by POLYNOM4:5;

then A1: len p >= 0 + 1 by NAT_1:13;

A2: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]

S_{1}[n]
from NAT_1:sch 8(A16, A2);

hence ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) ) by A1; :: thesis: verum

end;
( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

let p be non-zero Polynomial of L; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

defpred S

( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) );

p <> 0_. L by Def4;

then len p <> 0 by POLYNOM4:5;

then A1: len p >= 0 + 1 by NAT_1:13;

A2: for n being Nat st n >= 1 & S

S

proof

A16:
S
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

n >= 1 and

A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let p be Polynomial of L; :: thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) ) )

assume A4: len p = n + 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

end;
assume that

n >= 1 and

A3: S

let p be Polynomial of L; :: thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) ) )

assume A4: len p = n + 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

per cases
( p is with_roots or not p is with_roots )
;

end;

suppose
p is with_roots
; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

( n = card (Roots p) & n < len p ) )

then consider x being Element of L such that

A5: x is_a_root_of p ;

set r = <%(- x),(1. L)%>;

set pq = poly_quotient (p,x);

A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, Th47;

then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th20;

A8: Roots <%(- x),(1. L)%> = {x} by Th45;

then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ;

A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def6;

then consider k being Element of NAT such that

A10: k = card (Roots (poly_quotient (p,x))) and

A11: k < len (poly_quotient (p,x)) by A3, A4;

reconsider Rpq = Roots (poly_quotient (p,x)) as finite set by A3, A4, A9;

reconsider Rp = Rpq \/ Rr as finite set ;

card Rr = 1 by A8, CARD_1:30;

then A12: card Rp <= k + 1 by A10, CARD_2:43;

Roots (poly_quotient (p,x)) is finite by A3, A4, A9;

hence Roots p is finite by A8, A7; :: thesis: ex n being Element of NAT st

( n = card (Roots p) & n < len p )

take m = card Rp; :: thesis: ( m = card (Roots p) & m < len p )

thus m = card (Roots p) by A6, Th20; :: thesis: m < len p

k + 1 < n + 1 by A4, A9, A11, XREAL_1:8;

hence m < len p by A4, A12, XXREAL_0:2; :: thesis: verum

end;
A5: x is_a_root_of p ;

set r = <%(- x),(1. L)%>;

set pq = poly_quotient (p,x);

A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, Th47;

then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th20;

A8: Roots <%(- x),(1. L)%> = {x} by Th45;

then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ;

A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def6;

then consider k being Element of NAT such that

A10: k = card (Roots (poly_quotient (p,x))) and

A11: k < len (poly_quotient (p,x)) by A3, A4;

reconsider Rpq = Roots (poly_quotient (p,x)) as finite set by A3, A4, A9;

reconsider Rp = Rpq \/ Rr as finite set ;

card Rr = 1 by A8, CARD_1:30;

then A12: card Rp <= k + 1 by A10, CARD_2:43;

Roots (poly_quotient (p,x)) is finite by A3, A4, A9;

hence Roots p is finite by A8, A7; :: thesis: ex n being Element of NAT st

( n = card (Roots p) & n < len p )

take m = card Rp; :: thesis: ( m = card (Roots p) & m < len p )

thus m = card (Roots p) by A6, Th20; :: thesis: m < len p

k + 1 < n + 1 by A4, A9, A11, XREAL_1:8;

hence m < len p by A4, A12, XXREAL_0:2; :: thesis: verum

suppose A13:
not p is with_roots
; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

( n = card (Roots p) & n < len p )

take 0 ; :: thesis: ( 0 = card (Roots p) & 0 < len p )

thus 0 = card (Roots p) by A14; :: thesis: 0 < len p

thus 0 < len p by A4; :: thesis: verum

end;

( n = card (Roots p) & n < len p ) )

A14: now :: thesis: not Roots p <> {}

hence
Roots p is finite
; :: thesis: ex n being Element of NAT st
assume
Roots p <> {}
; :: thesis: contradiction

then consider x being object such that

A15: x in Roots p by XBOOLE_0:def 1;

reconsider x = x as Element of L by A15;

x is_a_root_of p by A15, POLYNOM5:def 10;

hence contradiction by A13; :: thesis: verum

end;
then consider x being object such that

A15: x in Roots p by XBOOLE_0:def 1;

reconsider x = x as Element of L by A15;

x is_a_root_of p by A15, POLYNOM5:def 10;

hence contradiction by A13; :: thesis: verum

( n = card (Roots p) & n < len p )

take 0 ; :: thesis: ( 0 = card (Roots p) & 0 < len p )

thus 0 = card (Roots p) by A14; :: thesis: 0 < len p

thus 0 < len p by A4; :: thesis: verum

proof

for n being Nat st n >= 1 holds
let p be Polynomial of L; :: thesis: ( len p = 1 implies ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) ) )

assume A17: len p = 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

hence Roots p is finite by Th43; :: thesis: ex n being Element of NAT st

( n = card (Roots p) & n < len p )

take 0 ; :: thesis: ( 0 = card (Roots p) & 0 < len p )

thus 0 = card (Roots p) by A17, Th43, CARD_1:27; :: thesis: 0 < len p

thus 0 < len p by A17; :: thesis: verum

end;
( n = card (Roots p) & n < len p ) ) )

assume A17: len p = 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) )

hence Roots p is finite by Th43; :: thesis: ex n being Element of NAT st

( n = card (Roots p) & n < len p )

take 0 ; :: thesis: ( 0 = card (Roots p) & 0 < len p )

thus 0 = card (Roots p) by A17, Th43, CARD_1:27; :: thesis: 0 < len p

thus 0 < len p by A17; :: thesis: verum

S

hence ( Roots p is finite & ex n being Element of NAT st

( n = card (Roots p) & n < len p ) ) by A1; :: thesis: verum

registration

let L be domRing;

let p be non-zero Polynomial of L;

correctness

coherence

Roots p is finite ;

by Lm1;

end;
let p be non-zero Polynomial of L;

correctness

coherence

Roots p is finite ;

by Lm1;

definition

let L be non degenerated comRing;

let x be Element of L;

let p be non-zero Polynomial of L;

ex b_{1} being Element of NAT ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b_{1} = max F )

for b_{1}, b_{2} being Element of NAT st ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b_{1} = max F ) & ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b_{2} = max F ) holds

b_{1} = b_{2}
;

end;
let x be Element of L;

let p be non-zero Polynomial of L;

func multiplicity (p,x) -> Element of NAT means :Def7: :: UPROOTS:def 8

ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & it = max F );

existence ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & it = max F );

ex b

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b

proof end;

uniqueness for b

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b

b

:: deftheorem Def7 defines multiplicity UPROOTS:def 8 :

for L being non degenerated comRing

for x being Element of L

for p being non-zero Polynomial of L

for b_{4} being Element of NAT holds

( b_{4} = multiplicity (p,x) iff ex F being non empty finite Subset of NAT st

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b_{4} = max F ) );

for L being non degenerated comRing

for x being Element of L

for p being non-zero Polynomial of L

for b

( b

( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b

theorem Th49: :: UPROOTS:52

for L being non degenerated comRing

for p being non-zero Polynomial of L

for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

for p being non-zero Polynomial of L

for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

proof end;

theorem Th50: :: UPROOTS:53

for L being non degenerated comRing

for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1

for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1

proof end;

definition

let L be domRing;

let p be non-zero Polynomial of L;

ex b_{1} being bag of the carrier of L st

( support b_{1} = Roots p & ( for x being Element of L holds b_{1} . x = multiplicity (p,x) ) )

for b_{1}, b_{2} being bag of the carrier of L st support b_{1} = Roots p & ( for x being Element of L holds b_{1} . x = multiplicity (p,x) ) & support b_{2} = Roots p & ( for x being Element of L holds b_{2} . x = multiplicity (p,x) ) holds

b_{1} = b_{2}

end;
let p be non-zero Polynomial of L;

func BRoots p -> bag of the carrier of L means :Def8: :: UPROOTS:def 9

( support it = Roots p & ( for x being Element of L holds it . x = multiplicity (p,x) ) );

existence ( support it = Roots p & ( for x being Element of L holds it . x = multiplicity (p,x) ) );

ex b

( support b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines BRoots UPROOTS:def 9 :

for L being domRing

for p being non-zero Polynomial of L

for b_{3} being bag of the carrier of L holds

( b_{3} = BRoots p iff ( support b_{3} = Roots p & ( for x being Element of L holds b_{3} . x = multiplicity (p,x) ) ) );

for L being domRing

for p being non-zero Polynomial of L

for b

( b

theorem Th52: :: UPROOTS:55

for L being domRing

for x being Element of L

for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))

for x being Element of L

for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))

proof end;

theorem Th53: :: UPROOTS:56

for L being domRing

for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)

for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)

proof end;

Lm2: now :: thesis: for L being domRing

for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))

for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))

let L be domRing; :: thesis: for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))

let p, q be non-zero Polynomial of L; :: thesis: degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))

BRoots (p *' q) = (BRoots p) + (BRoots q) by Th53;

hence degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th12; :: thesis: verum

end;
let p, q be non-zero Polynomial of L; :: thesis: degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))

BRoots (p *' q) = (BRoots p) + (BRoots q) by Th53;

hence degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th12; :: thesis: verum

theorem Th55: :: UPROOTS:58

for L being domRing

for x being Element of L

for n being Nat holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n

for x being Element of L

for n being Nat holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n

proof end;

theorem :: UPROOTS:59

for L being algebraic-closed domRing

for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1

for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1

proof end;

definition

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

let c be Element of L;

let n be Element of NAT ;

ex b_{1} being FinSequence of (Polynom-Ring L) st

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

b_{1} . i = <%(- c),(1. L)%> ) )

for b_{1}, b_{2} being FinSequence of (Polynom-Ring L) st len b_{1} = n & ( for i being Element of NAT st i in dom b_{1} holds

b_{1} . i = <%(- c),(1. L)%> ) & len b_{2} = n & ( for i being Element of NAT st i in dom b_{2} holds

b_{2} . i = <%(- c),(1. L)%> ) holds

b_{1} = b_{2}

end;
let c be Element of L;

let n be Element of NAT ;

func fpoly_mult_root (c,n) -> FinSequence of (Polynom-Ring L) means :Def9: :: UPROOTS:def 10

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

it . i = <%(- c),(1. L)%> ) );

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

it . i = <%(- c),(1. L)%> ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines fpoly_mult_root UPROOTS:def 10 :

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

for c being Element of L

for n being Element of NAT

for b_{4} being FinSequence of (Polynom-Ring L) holds

( b_{4} = fpoly_mult_root (c,n) iff ( len b_{4} = n & ( for i being Element of NAT st i in dom b_{4} holds

b_{4} . i = <%(- c),(1. L)%> ) ) );

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

for c being Element of L

for n being Element of NAT

for b

( b

b

definition

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

let b be bag of the carrier of L;

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

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b_{1} = Product (FlattenSeq f) )

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

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b_{1} = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b_{2} = Product (FlattenSeq f) ) holds

b_{1} = b_{2}

end;
let b be bag of the carrier of L;

func poly_with_roots b -> Polynomial of L means :Def10: :: UPROOTS:def 11

ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it = Product (FlattenSeq f) );

existence ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it = Product (FlattenSeq f) );

ex b

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b

proof end;

uniqueness for b

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b

b

proof end;

:: deftheorem Def10 defines poly_with_roots UPROOTS:def 11 :

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

for b being bag of the carrier of L

for b_{3} being Polynomial of L holds

( b_{3} = poly_with_roots b iff ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b_{3} = Product (FlattenSeq f) ) );

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

for b being bag of the carrier of L

for b

( b

( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b

theorem Th57: :: UPROOTS:60

for L being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>

proof end;

theorem Th58: :: UPROOTS:61

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

for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>

for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>

proof end;

theorem Th59: :: UPROOTS:62

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

for b being bag of the carrier of L

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

for b being bag of the carrier of L

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

proof end;

theorem Th60: :: UPROOTS:63

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

for b being bag of the carrier of L

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L

for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )

for b being bag of the carrier of L

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L

for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )

proof end;

theorem Th61: :: UPROOTS:64

for L being comRing

for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)

for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)

proof end;

theorem :: UPROOTS:65

for L being algebraic-closed domRing

for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds

p = poly_with_roots (BRoots p)

for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds

p = poly_with_roots (BRoots p)

proof end;

theorem :: UPROOTS:66

for L being comRing

for s being non empty finite Subset of L

for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

for s being non empty finite Subset of L

for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

proof end;

theorem :: UPROOTS:67

for L being non trivial comRing

for s being non empty finite Subset of L

for x being Element of L

for f being FinSequence of L st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = eval (<%(- c),(1. L)%>,x) ) holds

eval ((poly_with_roots ((s,1) -bag)),x) = Product f

for s being non empty finite Subset of L

for x being Element of L

for f being FinSequence of L st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = eval (<%(- c),(1. L)%>,x) ) holds

eval ((poly_with_roots ((s,1) -bag)),x) = Product f

proof end;