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