:: UPROOTS semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: UPROOTS:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( ( n = 1 or n > 1 ) iff not n is empty )
proof end;

theorem Th2: :: UPROOTS:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of NAT st ( for i being Nat st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 )
proof end;

scheme :: UPROOTS:sch 1
IndFinSeq0{ F1() -> FinSequence, P1[ set , set ] } :
for i being Nat st 1 <= i & i <= len F1() holds
P1[i,F1() . i]
provided
A1: P1[1,F1() . 1] and
A2: for i being Nat st 1 <= i & i < len F1() & P1[i,F1() . i] holds
P1[i + 1,F1() . (i + 1)]
proof end;

theorem Th3: :: UPROOTS:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable LoopStr
for r being FinSequence of L st len r >= 2 & ( for k being Nat st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
proof end;

definition
let A be finite set ;
func canFS A -> FinSequence of A means :Def1: :: UPROOTS:def 1
( len it = card A & ex f being FinSequence st
( len f = card A & ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) & ( for i being Nat st 1 <= i & i < card A holds
for x being set st f . i = x holds
f . (i + 1) = [(choose (x `2 )),((x `2 ) \ {(choose (x `2 ))})] ) & ( for i being Nat st i in dom it holds
it . i = (f . i) `1 ) ) );
existence
ex b1 being FinSequence of A st
( len b1 = card A & ex f being FinSequence st
( len f = card A & ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) & ( for i being Nat st 1 <= i & i < card A holds
for x being set st f . i = x holds
f . (i + 1) = [(choose (x `2 )),((x `2 ) \ {(choose (x `2 ))})] ) & ( for i being Nat st i in dom b1 holds
b1 . i = (f . i) `1 ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of A st len b1 = card A & ex f being FinSequence st
( len f = card A & ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) & ( for i being Nat st 1 <= i & i < card A holds
for x being set st f . i = x holds
f . (i + 1) = [(choose (x `2 )),((x `2 ) \ {(choose (x `2 ))})] ) & ( for i being Nat st i in dom b1 holds
b1 . i = (f . i) `1 ) ) & len b2 = card A & ex f being FinSequence st
( len f = card A & ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) & ( for i being Nat st 1 <= i & i < card A holds
for x being set st f . i = x holds
f . (i + 1) = [(choose (x `2 )),((x `2 ) \ {(choose (x `2 ))})] ) & ( for i being Nat st i in dom b2 holds
b2 . i = (f . i) `1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines canFS UPROOTS:def 1 :
for A being finite set
for b2 being FinSequence of A holds
( b2 = canFS A iff ( len b2 = card A & ex f being FinSequence st
( len f = card A & ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) & ( for i being Nat st 1 <= i & i < card A holds
for x being set st f . i = x holds
f . (i + 1) = [(choose (x `2 )),((x `2 ) \ {(choose (x `2 ))})] ) & ( for i being Nat st i in dom b2 holds
b2 . i = (f . i) `1 ) ) ) );

theorem Th4: :: UPROOTS:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite set holds canFS A is one-to-one
proof end;

theorem Th5: :: UPROOTS:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite set holds rng (canFS A) = A
proof end;

theorem Th6: :: UPROOTS:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds canFS {a} = <*a*>
proof end;

theorem Th7: :: UPROOTS:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite set holds (canFS A) " is Function of A, Seg (card A)
proof end;

definition
let X be set ;
let S be finite Subset of X;
let n be Nat;
func S,n -bag -> Element of Bags X equals :: UPROOTS:def 2
(EmptyBag X) +* (S --> n);
correctness
coherence
(EmptyBag X) +* (S --> n) is Element of Bags X
;
proof end;
end;

:: deftheorem defines -bag UPROOTS:def 2 :
for X being set
for S being finite Subset of X
for n being Nat holds S,n -bag = (EmptyBag X) +* (S --> n);

theorem Th8: :: UPROOTS:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being finite Subset of X
for n being Nat
for i being set st not i in S holds
(S,n -bag ) . i = 0
proof end;

theorem Th9: :: UPROOTS:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being finite Subset of X
for n being Nat
for i being set st i in S holds
(S,n -bag ) . i = n
proof end;

theorem Th10: :: UPROOTS:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being finite Subset of X
for n being Nat st n <> 0 holds
support (S,n -bag ) = S
proof end;

theorem :: UPROOTS:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being finite Subset of X
for n being Nat st ( S is empty or n = 0 ) holds
S,n -bag = EmptyBag X
proof end;

theorem Th12: :: UPROOTS:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S, T being finite Subset of X
for n being Nat st S misses T holds
(S \/ T),n -bag = (S,n -bag ) + (T,n -bag )
proof end;

definition
let X be set ;
mode Rbag of X is real-yielding finite-support ManySortedSet of X;
end;

definition
let A be set ;
let b be Rbag of A;
func Sum b -> real number means :Def3: :: UPROOTS:def 3
ex f being FinSequence of REAL st
( it = Sum f & f = b * (canFS (support b)) );
existence
ex b1 being real number ex f being FinSequence of REAL st
( b1 = Sum f & f = b * (canFS (support b)) )
proof end;
uniqueness
for b1, b2 being real number st ex f being FinSequence of REAL st
( b1 = Sum f & f = b * (canFS (support b)) ) & ex f being FinSequence of REAL st
( b2 = Sum f & f = b * (canFS (support b)) ) holds
b1 = b2
;
end;

:: deftheorem Def3 defines Sum UPROOTS:def 3 :
for A being set
for b being Rbag of A
for b3 being real number holds
( b3 = Sum b iff ex f being FinSequence of REAL st
( b3 = Sum f & f = b * (canFS (support b)) ) );

notation
let A be set ;
let b be bag of A;
synonym degree b for Sum b;
end;

definition
let A be set ;
let b be bag of A;
:: original: Sum
redefine func degree b -> Nat means :Def4: :: UPROOTS:def 4
ex f being FinSequence of NAT st
( it = Sum f & f = b * (canFS (support b)) );
coherence
Sum b is Nat
proof end;
compatibility
for b1 being Nat holds
( b1 = Sum b iff ex f being FinSequence of NAT st
( b1 = Sum f & f = b * (canFS (support b)) ) )
proof end;
end;

:: deftheorem Def4 defines degree UPROOTS:def 4 :
for A being set
for b being bag of A
for b3 being Nat holds
( b3 = degree b iff ex f being FinSequence of NAT st
( b3 = Sum f & f = b * (canFS (support b)) ) );

theorem Th13: :: UPROOTS:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for b being Rbag of A st b = EmptyBag A holds
Sum b = 0
proof end;

theorem Th14: :: UPROOTS:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for b being bag of A st Sum b = 0 holds
b = EmptyBag A
proof end;

theorem Th15: :: UPROOTS:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th16: :: UPROOTS:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th17: :: UPROOTS:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
proof end;

theorem Th18: :: UPROOTS:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital associative commutative HGrStr
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;

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
attr p is non-zero means :Def5: :: UPROOTS:def 5
p <> 0_. L;
end;

:: deftheorem Def5 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 );

theorem Th19: :: UPROOTS:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff len p > 0 )
proof end;

registration
let L be non empty non trivial ZeroStr ;
cluster non-zero M5( NAT ,the carrier of L);
existence
ex b1 being Polynomial of L st b1 is non-zero
proof end;
end;

registration
let L be non empty non degenerated multLoopStr_0 ;
let x be Element of L;
cluster <%x,(1. L)%> -> non-zero ;
correctness
coherence
<%x,(1. L)%> is non-zero
;
proof end;
end;

theorem Th20: :: UPROOTS:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for p being Polynomial of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proof end;

theorem Th21: :: UPROOTS:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> & p . 0 <> 0. L )
proof end;

theorem Th22: :: UPROOTS:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p being Polynomial of L holds p *' (0_. L) = 0_. L
proof end;

registration
cluster non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non degenerated domRing-like algebraic-closed doubleLoopStr ;
existence
ex b1 being non empty unital doubleLoopStr st
( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is domRing-like & not b1 is degenerated )
proof end;
end;

theorem Th23: :: UPROOTS:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr
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 add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr ;
cluster Polynom-Ring L -> domRing-like ;
correctness
coherence
Polynom-Ring L is domRing-like
;
proof end;
end;

registration
let L be domRing;
let p, q be non-zero Polynomial of L;
cluster p *' q -> non-zero ;
correctness
coherence
p *' q is non-zero
;
proof end;
end;

theorem :: UPROOTS:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non degenerated comRing
for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)
proof end;

theorem Th25: :: UPROOTS:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)
proof end;

theorem Th26: :: UPROOTS:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p being Polynomial of L
for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc
proof end;

theorem Th27: :: UPROOTS:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive 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
proof end;

theorem Th28: :: UPROOTS:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)
proof end;

theorem Th29: :: UPROOTS:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p, q being Polynomial of L st p - q = 0_. L holds
p = q
proof end;

theorem Th30: :: UPROOTS:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr
for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds
q = r
proof end;

theorem Th31: :: UPROOTS:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for n being Nat
for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
proof end;

theorem Th32: :: UPROOTS:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being comRing
for i, j being Nat
for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
proof end;

theorem Th33: :: UPROOTS:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%>
proof end;

theorem :: UPROOTS:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for p being Polynomial of L holds p *' <%(1. L)%> = p
proof end;

theorem Th35: :: UPROOTS:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds
len (p *' q) = 0
proof end;

theorem Th36: :: UPROOTS:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
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:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital doubleLoopStr
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 Th38: :: UPROOTS:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital domRing-like doubleLoopStr
for p, q being Polynomial of L st 1 < len p & 1 < len q holds
len p < len (p *' q)
proof end;

theorem Th39: :: UPROOTS:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable left-distributive 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)) ) )
proof end;

theorem Th40: :: UPROOTS:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr
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 Th41: :: UPROOTS:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non degenerated comRing
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;
cluster <%x,(1. L)%> `^ n -> non-zero ;
correctness
coherence
<%x,(1. L)%> `^ n is non-zero
;
proof end;
end;

theorem Th42: :: UPROOTS:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th43: :: UPROOTS:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital associative commutative add-associative right_zeroed right_complementable distributive non degenerated 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
proof end;

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
let n be Nat;
func poly_shift p,n -> Polynomial of L means :Def6: :: UPROOTS:def 6
for i being Nat holds it . i = p . (n + i);
existence
ex b1 being Polynomial of L st
for i being Nat holds b1 . i = p . (n + i)
proof end;
uniqueness
for b1, b2 being Polynomial of L st ( for i being Nat holds b1 . i = p . (n + i) ) & ( for i being Nat holds b2 . i = p . (n + i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines poly_shift UPROOTS:def 6 :
for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat
for b4 being Polynomial of L holds
( b4 = poly_shift p,n iff for i being Nat holds b4 . i = p . (n + i) );

theorem Th44: :: UPROOTS:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for p being Polynomial of L holds poly_shift p,0 = p
proof end;

theorem Th45: :: UPROOTS:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for n being Nat
for p being Polynomial of L st n >= len p holds
poly_shift p,n = 0_. L
proof end;

theorem Th46: :: UPROOTS:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty non degenerated multLoopStr_0
for n being Nat
for p being Polynomial of L st n <= len p holds
(len (poly_shift p,n)) + n = len p
proof end;

theorem Th47: :: UPROOTS:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non degenerated comRing
for x being Element of L
for n being 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;

theorem Th48: :: UPROOTS:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non degenerated comRing
for p being Polynomial of L st len p = 1 holds
Roots p = {}
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 ;
func poly_quotient p,r -> Polynomial of L means :Def7: :: 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 p > 0 implies ex b1 being Polynomial of L st
( (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval (poly_shift p,(i + 1)),r ) ) ) & ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) )
proof end;
uniqueness
for b1, b2 being Polynomial of L holds
( ( len p > 0 & (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval (poly_shift p,(i + 1)),r ) & (len b2) + 1 = len p & ( for i being Nat holds b2 . i = eval (poly_shift p,(i + 1)),r ) implies b1 = b2 ) & ( not len p > 0 & b1 = 0_. L & b2 = 0_. L implies b1 = b2 ) )
proof end;
consistency
for b1 being Polynomial of L holds verum
;
end;

:: deftheorem Def7 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 b4 being Polynomial of L holds
( ( len p > 0 implies ( b4 = poly_quotient p,r iff ( (len b4) + 1 = len p & ( for i being Nat holds b4 . i = eval (poly_shift p,(i + 1)),r ) ) ) ) & ( not len p > 0 implies ( b4 = poly_quotient p,r iff b4 = 0_. L ) ) );

theorem Th49: :: UPROOTS:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th50: :: UPROOTS:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for x being Element of L holds Roots <%(- x),(1. L)%> = {x}
proof end;

theorem Th51: :: UPROOTS:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th52: :: UPROOTS:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: UPROOTS:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

Lm1: now
let L be domRing; :: thesis: for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being 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 Nat st
( n = Card (Roots p) & n < len p ) )

p <> 0_. L by Def5;
then len p <> 0 by POLYNOM4:8;
then len p > 0 ;
then A1: len p >= 0 + 1 by NAT_1:38;
defpred S1[ Nat] means for p being Polynomial of L st len p = $1 holds
( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) );
A2: S1[1]
proof
let p be Polynomial of L; :: thesis: ( len p = 1 implies ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) ) )

assume A3: len p = 1 ; :: thesis: ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) )

hence Roots p is finite by Th48; :: thesis: ex n being 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 A3, Th48, CARD_1:78; :: thesis: 0 < len p
thus 0 < len p by A3; :: thesis: verum
end;
A4: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A5: n >= 1 and
A6: S1[n] ; :: thesis: S1[n + 1]
let p be Polynomial of L; :: thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) ) )

assume A7: len p = n + 1 ; :: thesis: ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) )

then A8: len p > 1 by A5, NAT_1:38;
per cases ( p is with_roots or not p is with_roots ) ;
suppose p is with_roots ; :: thesis: ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) )

then consider x being Element of L such that
A9: x is_a_root_of p by POLYNOM5:def 7;
A10: len p > 0 by A8;
A11: p = <%(- x),(1. L)%> *' (poly_quotient p,x) by A9, Th52;
set r = <%(- x),(1. L)%>;
set pq = poly_quotient p,x;
A12: (len (poly_quotient p,x)) + 1 = len p by A9, A10, Def7;
then A13: len (poly_quotient p,x) = n by A7;
then A14: Roots (poly_quotient p,x) is finite by A6;
A15: Roots <%(- x),(1. L)%> = {x} by Th50;
Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient p,x)) by A11, Th25;
hence Roots p is finite by A14, A15, FINSET_1:14; :: thesis: ex n being Nat st
( n = Card (Roots p) & n < len p )

consider k being Nat such that
A16: k = Card (Roots (poly_quotient p,x)) and
A17: k < len (poly_quotient p,x) by A6, A13;
reconsider Rpq = Roots (poly_quotient p,x) as finite set by A6, A13;
reconsider Rr = Roots <%(- x),(1. L)%> as finite set by A15;
reconsider Rp = Rpq \/ Rr as finite set ;
take m = card Rp; :: thesis: ( m = Card (Roots p) & m < len p )
thus m = Card (Roots p) by A11, Th25; :: thesis: m < len p
card Rr = 1 by A15, CARD_1:79;
then A18: card Rp <= k + 1 by A16, CARD_2:62;
k + 1 < n + 1 by A7, A12, A17, XREAL_1:10;
hence m < len p by A7, A18, XREAL_1:2; :: thesis: verum
end;
suppose A19: not p is with_roots ; :: thesis: ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) )

A20: now
assume Roots p <> {} ; :: thesis: contradiction
then consider x being set such that
A21: x in Roots p by XBOOLE_0:def 1;
reconsider x = x as Element of L by A21;
x is_a_root_of p by A21, POLYNOM5:def 9;
hence contradiction by A19, POLYNOM5:def 7; :: thesis: verum
end;
hence Roots p is finite ; :: thesis: ex n being 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 A20, CARD_1:78; :: thesis: 0 < len p
thus 0 < len p by A8; :: thesis: verum
end;
end;
end;
for n being Nat st n >= 1 holds
S1[n] from INT_2:sch 1( 1 , A2, A4);
hence ( Roots p is finite & ex n being Nat st
( n = Card (Roots p) & n < len p ) ) by A1; :: thesis: verum
end;

registration
let L be domRing;
let p be non-zero Polynomial of L;
cluster Roots p -> finite ;
correctness
coherence
Roots p is finite
;
by Lm1;
end;

definition
let L be non degenerated comRing;
let x be Element of L;
let p be non-zero Polynomial of L;
func multiplicity p,x -> Nat means :Def8: :: UPROOTS:def 8
ex F being non empty finite Subset of NAT st
( F = { k where k is Nat : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & it = max F );
existence
ex b1 being Nat ex F being non empty finite Subset of NAT st
( F = { k where k is Nat : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b1 = max F )
proof end;
uniqueness
for b1, b2 being Nat st ex F being non empty finite Subset of NAT st
( F = { k where k is Nat : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b1 = max F ) & ex F being non empty finite Subset of NAT st
( F = { k where k is Nat : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b2 = max F ) holds
b1 = b2
;
end;

:: deftheorem Def8 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 b4 being Nat holds
( b4 = multiplicity p,x iff ex F being non empty finite Subset of NAT st
( F = { k where k is Nat : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b4 = max F ) );

theorem Th54: :: UPROOTS:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th55: :: UPROOTS:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non degenerated comRing
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;
func BRoots p -> bag of the carrier of L means :Def9: :: UPROOTS:def 9
( support it = Roots p & ( for x being Element of L holds it . x = multiplicity p,x ) );
existence
ex b1 being bag of the carrier of L st
( support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity p,x ) )
proof end;
uniqueness
for b1, b2 being bag of the carrier of L st support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity p,x ) & support b2 = Roots p & ( for x being Element of L holds b2 . x = multiplicity p,x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines BRoots UPROOTS:def 9 :
for L being domRing
for p being non-zero Polynomial of L
for b3 being bag of the carrier of L holds
( b3 = BRoots p iff ( support b3 = Roots p & ( for x being Element of L holds b3 . x = multiplicity p,x ) ) );

theorem Th56: :: UPROOTS:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for x being Element of L holds BRoots <%(- x),(1. L)%> = {x},1 -bag
proof end;

theorem Th57: :: UPROOTS:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th58: :: UPROOTS:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)
proof end;

Lm2: now
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 Th58;
hence degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th17; :: thesis: verum
end;

theorem Th59: :: UPROOTS:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for p being non-zero Polynomial of L st len p = 1 holds
degree (BRoots p) = 0
proof end;

theorem Th60: :: UPROOTS:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for x being Element of L
for n being Nat holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
proof end;

theorem :: UPROOTS:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being algebraic-closed domRing
for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1
proof end;

definition
let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c be Element of L;
let n be Nat;
func fpoly_mult_root c,n -> FinSequence of (Polynom-Ring L) means :Def10: :: UPROOTS:def 10
( len it = n & ( for i being Nat st i in dom it holds
it . i = <%(- c),(1. L)%> ) );
existence
ex b1 being FinSequence of (Polynom-Ring L) st
( len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of (Polynom-Ring L) st len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) & len b2 = n & ( for i being Nat st i in dom b2 holds
b2 . i = <%(- c),(1. L)%> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines fpoly_mult_root UPROOTS:def 10 :
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for c being Element of L
for n being Nat
for b4 being FinSequence of (Polynom-Ring L) holds
( b4 = fpoly_mult_root c,n iff ( len b4 = n & ( for i being Nat st i in dom b4 holds
b4 . i = <%(- c),(1. L)%> ) ) );

definition
let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let b be bag of the carrier of L;
func poly_with_roots b -> Polynomial of L means :Def11: :: 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 Nat st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & it = Product (FlattenSeq f) );
existence
ex b1 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 Nat st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & b1 = Product (FlattenSeq f) )
proof end;
uniqueness
for b1, b2 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 Nat st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & b1 = 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 Nat st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & b2 = Product (FlattenSeq f) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines poly_with_roots UPROOTS:def 11 :
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b being bag of the carrier of L
for b3 being Polynomial of L holds
( b3 = 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 Nat st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & b3 = Product (FlattenSeq f) ) );

theorem Th62: :: UPROOTS:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
proof end;

theorem Th63: :: UPROOTS:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for c being Element of L holds poly_with_roots ({c},1 -bag ) = <%(- c),(1. L)%>
proof end;

theorem Th64: :: UPROOTS:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive 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 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 Th65: :: UPROOTS:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive 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 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 Th66: :: UPROOTS:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: UPROOTS:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: UPROOTS:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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;