:: Little {B}ezout Theorem (Factor Theorem) :: by Piotr Rudnicki :: :: Received December 30, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3, FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, REAL_1, ARYTM_1, XBOOLE_0, RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, FUNCT_2, ZFMISC_1, PRE_POLY, FUNCT_4, FUNCOP_1, VALUED_0, PBOOLE, SGRAPH1, FINSOP_1, BINOP_1, GROUP_1, STRUCT_0, POLYNOM1, POLYNOM3, AFINSQ_1, MESFUNC1, ALGSEQ_1, VECTSP_1, POLYNOM5, LATTICES, VECTSP_2, COMPLFLD, POLYNOM2, FVSUM_1, MEMBERED, CLASSES1, UPROOTS, FUNCT_7; notations TARSKI, XBOOLE_0, XTUPLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XREAL_0, ZFMISC_1, REAL_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_2, DOMAIN_1, FUNCT_2, XXREAL_2, VALUED_0, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1, FINSOP_1, NORMSP_1, GROUP_4, RVSUM_1, ALGSEQ_1, COMPLFLD, POLYNOM3, POLYNOM4, POLYNOM5, FINSET_1, MCART_1, FUNCT_4, FUNCOP_1, CLASSES1, FVSUM_1, WSIERP_1, MEMBERED, GROUP_1, RECDEF_1, PRE_POLY; constructors WELLORD2, SETWISEO, REAL_1, FINSEQOP, FINSOP_1, NAT_D, WSIERP_1, VECTSP_2, REALSET2, ALGSTR_1, GROUP_4, MATRIX_1, GOBOARD1, POLYNOM2, POLYNOM4, POLYNOM5, RECDEF_1, BINOP_2, CLASSES1, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, XTUPLE_0, ALGSEQ_1, BINOP_1, NUMBERS, COMPLFLD; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4, POLYNOM5, FINSEQ_2, VALUED_0, XXREAL_2, FUNCT_2, RELSET_1, GROUP_1, VFUNCT_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin theorem :: 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; :: Stolen from POLYNOM2 scheme :: UPROOTS:sch 1 IndFinSeq0 { k() -> Nat, P[set]} : for i being Element of NAT st 1 <= i & i <= k() holds P[i] provided P[1] and for i being Element of NAT st 1 <= i & i < k() holds P[i] implies P[ i+1]; theorem :: UPROOTS:2 for L be add-associative right_zeroed right_complementable non empty addLoopStr, r be 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; begin :: More about bags definition ::$CD let X be set, S be finite Subset of X, n be Element of NAT; func (S, n)-bag -> Element of Bags X equals :: UPROOTS:def 2 (EmptyBag X) +* (S --> n); end; ::$CT 3 theorem :: UPROOTS:6 for X being set, S being finite Subset of X, n being Element of NAT, i being object st not i in S holds (S, n)-bag.i = 0; theorem :: UPROOTS:7 for X being set, S being finite Subset of X, n being Element of NAT, i being set st i in S holds (S, n)-bag.i = n; theorem :: UPROOTS:8 for X being set, S being finite Subset of X, n being Element of NAT st n <> 0 holds support (S, n)-bag = S; theorem :: UPROOTS:9 for X being set, S being finite Subset of X, n being Element of NAT st S is empty or n = 0 holds (S, n)-bag = EmptyBag X; theorem :: UPROOTS:10 for X being set, S, T being finite Subset of X, n being Element of NAT st S misses T holds (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag; definition let X be set; mode Rbag of X is real-valued finite-support ManySortedSet of X; end; definition let A be set, b be Rbag of A; func Sum b -> Real means :: UPROOTS:def 3 ex f being FinSequence of REAL st it = Sum f & f = b*canFS(support b); end; notation let A be set, b be bag of A; synonym degree b for Sum b; end; definition let A be set, b be bag of A; redefine func degree b -> Element of NAT means :: UPROOTS:def 4 ex f being FinSequence of NAT st it = Sum f & f = b*canFS(support b); end; theorem :: UPROOTS:11 for A being set, b being Rbag of A st b = EmptyBag A holds Sum b = 0; theorem :: UPROOTS:12 for A being set, b being bag of A st Sum b = 0 holds b = EmptyBag A; theorem :: UPROOTS:13 for A being set, S being finite Subset of A, b being bag of A holds S = support b & degree b = card S iff b = (S, 1)-bag; theorem :: UPROOTS:14 for A being set, S being finite Subset of A, b being Rbag of A st support b c= S ex f being FinSequence of REAL st f = b*canFS(S) & Sum b = Sum f; theorem :: UPROOTS:15 for A being set, b, b1, b2 being Rbag of A st b = b1 + b2 holds Sum b = Sum b1 + Sum b2; theorem :: UPROOTS:16 :: GROUP_4:18 but about a different Product for L being associative commutative unital non empty multMagma , f, g being FinSequence of L, p being Permutation of dom f st g = f * p holds Product(g) = Product(f); begin :: More on polynomials definition let L be non empty ZeroStr, p be Polynomial of L; attr p is non-zero means :: UPROOTS:def 5 p <> 0_. L; end; theorem :: UPROOTS:17 for L being non empty ZeroStr, p being Polynomial of L holds p is non-zero iff len p > 0; registration let L be non trivial ZeroStr; cluster non-zero for Polynomial of L; end; registration let L be non degenerated non empty multLoopStr_0, x be Element of L; cluster <%x, 1.L%> -> non-zero; end; theorem :: UPROOTS:18 for L being non empty ZeroStr, p being Polynomial of L st len p > 0 holds p.(len p -'1) <> 0.L; theorem :: UPROOTS:19 for L being non empty ZeroStr, p being AlgSequence of L st len p = 1 holds p = <%p.0%> & p.0 <> 0.L; theorem :: UPROOTS:20 :: from POLYNOM4:5 right-distributive for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L holds p*'( 0_.(L)) = 0_.(L); registration cluster algebraic-closed add-associative right_zeroed right_complementable Abelian commutative associative distributive domRing-like non degenerated for unital non empty doubleLoopStr; end; theorem :: UPROOTS:21 for L being add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q being Polynomial of L st p*'q = 0_. L holds p = 0_. L or q = 0_. L; registration let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr; cluster Polynom-Ring L -> domRing-like; end; registration let L be domRing, p, q be non-zero Polynomial of L; cluster p*'q -> non-zero; end; theorem :: UPROOTS:22 for L being non degenerated comRing, p, q being Polynomial of L holds Roots p \/ Roots q c= Roots (p*'q); theorem :: UPROOTS:23 for L being domRing, p, q being Polynomial of L holds Roots (p*' q) = Roots p \/ Roots q; theorem :: UPROOTS:24 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p being (Polynomial of L), pc being ( Element of Polynom-Ring L) st p = pc holds -p = -pc; theorem :: UPROOTS:25 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being (Polynomial of L), pc, qc being (Element of Polynom-Ring L) st p= pc & q = qc holds p-q = pc-qc; theorem :: UPROOTS:26 for L being Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q, r being ( Polynomial of L) holds p*'q-p*'r = p*'(q-r); theorem :: UPROOTS:27 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being (Polynomial of L) st p-q = 0_. L holds p = q; theorem :: UPROOTS:28 for L being Abelian add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q, r being Polynomial of L st p <> 0_. L & p*'q = p*'r holds q = r; theorem :: UPROOTS:29 for L being domRing, n being Element of NAT, p being Polynomial of L st p <> 0_. L holds p`^n <> 0_. L; theorem :: UPROOTS:30 for L being comRing, i, j being Nat, p being Polynomial of L holds (p`^i) *' (p`^j) = p `^(i+j); theorem :: UPROOTS:31 for L being non empty multLoopStr_0 holds 1_.(L) = <%1.L%>; theorem :: UPROOTS:32 for L being add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, p being Polynomial of L holds p*'<%1.L%> = p; theorem :: UPROOTS:33 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L st len p = 0 or len q = 0 holds len (p*'q) = 0; theorem :: UPROOTS:34 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L st p*'q is non-zero holds p is non-zero & q is non-zero; theorem :: UPROOTS:35 for L being add-associative right_zeroed right_complementable distributive commutative associative well-unital non empty doubleLoopStr, p, q being Polynomial of L st p.(len p -'1) * q.(len q -'1) <> 0.L holds 0 < len ( p*'q); theorem :: UPROOTS:36 for L being add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p, q being Polynomial of L st 1 < len p & 1 < len q holds len p < len (p*'q); theorem :: UPROOTS:37 for L being add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, a, b being Element of L, 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; theorem :: UPROOTS:38 for L being add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r being Element of L, q being non-zero Polynomial of L holds len (<%r, 1.L%>*'q) = len q + 1; theorem :: UPROOTS:39 for L being non degenerated comRing, x being Element of L, i being Nat holds len (<%x, 1.L%>`^i) = i+1; registration let L be non degenerated comRing, x be Element of L, n be Nat; cluster <%x, 1.L%>`^n -> non-zero; end; theorem :: UPROOTS:40 for L being non degenerated comRing, x being Element of L, q being non-zero (Polynomial of L), i being Nat holds len ((<%x, 1.L%> `^i)*'q) = i + len q; theorem :: UPROOTS:41 for L being add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r being Element of L, 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; begin :: Little Bezout theorem definition let L be non empty ZeroStr, p be Polynomial of L; let n be Nat; func poly_shift(p,n) -> Polynomial of L means :: UPROOTS:def 6 for i being Nat holds it.i = p.(n + i); end; theorem :: UPROOTS:42 for L being non empty ZeroStr,p being Polynomial of L holds poly_shift(p,0) = p; theorem :: UPROOTS:43 for L being non empty ZeroStr, n being Element of NAT, p being Polynomial of L st n >= len p holds poly_shift(p,n) = 0_. L; theorem :: UPROOTS:44 for L being non degenerated non empty multLoopStr_0, n being Element of NAT, p being Polynomial of L st n <= len p holds len poly_shift(p,n) + n = len p; theorem :: UPROOTS:45 for L being non degenerated comRing, x being Element of L, n being Element of NAT, 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; theorem :: UPROOTS:46 for L being non degenerated comRing, p being Polynomial of L st len p = 1 holds Roots p = {}; definition let L be non degenerated comRing, r be Element of L, p be Polynomial of L such that r is_a_root_of p; func poly_quotient(p,r) -> Polynomial of L means :: 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; end; theorem :: UPROOTS:47 for L being non degenerated comRing, r being Element of L, p being non-zero Polynomial of L st r is_a_root_of p holds len poly_quotient(p,r) > 0; theorem :: UPROOTS:48 for L being add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr, x being Element of L holds Roots <%-x, 1.L%> = {x}; theorem :: UPROOTS:49 for L being non trivial comRing, x being Element of L, p, q being Polynomial of L st p = <%-x,1.L%>*'q holds x is_a_root_of p; ::$N Little Bezout Theorem (Factor Theorem) theorem :: UPROOTS:50 :: Factor theorem (Bezout) for L being non degenerated comRing, r being Element of L, p being Polynomial of L st r is_a_root_of p holds p = <%-r,1.L%>*'poly_quotient(p ,r); theorem :: UPROOTS:51 :: Factor theorem (Bezout) for L being non degenerated comRing, r being Element of L, p, q being Polynomial of L st p = <%-r,1.L%>*'q holds r is_a_root_of p; begin :: Polynomials defined by roots registration let L be domRing, p be non-zero Polynomial of L; cluster Roots p -> finite; end; definition let L be non degenerated comRing, x be Element of L, p be non-zero ( Polynomial of L); func multiplicity(p,x) -> Element of NAT means :: UPROOTS:def 8 ex F being finite non empty 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; end; theorem :: UPROOTS:52 for L being non degenerated comRing, p being non-zero ( Polynomial of L), x being Element of L holds x is_a_root_of p iff multiplicity( p,x) >= 1; theorem :: UPROOTS:53 for L being non degenerated comRing, x being Element of L holds multiplicity(<%-x, 1.L%>,x) = 1; definition let L be domRing, p be non-zero Polynomial of L; func BRoots(p) -> bag of the carrier of L means :: UPROOTS:def 9 support it = Roots p & for x being Element of L holds it.x = multiplicity(p,x); end; theorem :: UPROOTS:54 for L being domRing, x being Element of L holds BRoots <%-x, 1.L %> = ({x}, 1)-bag; theorem :: UPROOTS:55 for L being domRing, x be Element of L, p, q being non-zero Polynomial of L holds multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q ,x); theorem :: UPROOTS:56 for L being domRing, p, q being non-zero Polynomial of L holds BRoots(p*'q) = BRoots(p) + BRoots(q); theorem :: UPROOTS:57 for L being domRing, p being non-zero Polynomial of L st len p = 1 holds degree BRoots p = 0; theorem :: UPROOTS:58 for L being domRing, x be Element of L, n being Nat holds degree BRoots (<%-x, 1.L%>`^n) = n; theorem :: UPROOTS:59 for L being algebraic-closed domRing, p being non-zero Polynomial of L holds degree BRoots p = len p -' 1; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c be Element of L, n be Element of NAT; func fpoly_mult_root(c,n) -> FinSequence of Polynom-Ring L means :: UPROOTS:def 10 len it = n & for i being Element of NAT st i in dom it holds it.i = <% -c, 1.L%>; end; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L; func poly_with_roots(b) -> Polynomial of L means :: UPROOTS:def 11 ex f being FinSequence of (the carrier of Polynom-Ring L)*, 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; end; theorem :: UPROOTS:60 for L being Abelian add-associative right_zeroed right_complementable commutative distributive well-unital non empty doubleLoopStr holds poly_with_roots(EmptyBag the carrier of L) = <%1.L%>; theorem :: UPROOTS:61 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c being Element of L holds poly_with_roots(({c},1)-bag) = <% -c, 1.L %>; theorem :: UPROOTS:62 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of (the carrier of Polynom-Ring L)*, 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; theorem :: UPROOTS:63 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L , 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); theorem :: 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); theorem :: UPROOTS:65 for L being algebraic-closed domRing, p being non-zero (Polynomial of L) st p.(len p-'1) = 1.L holds p = poly_with_roots(BRoots(p)); theorem :: UPROOTS:66 for L being comRing, s being non empty finite Subset of L, f being FinSequence of Polynom-Ring L st len f = card s & for i being Element of NAT, 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); theorem :: UPROOTS:67 for L being non trivial comRing, s being non empty finite Subset of L, x being Element of L, f being FinSequence of L st len f = card s & for i being Element of NAT, 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) ;