:: On Roots of Polynomials and Algebraically Closed Fields
:: by Christoph Schwarzweller
::
:: Received August 30, 2017
:: Copyright (c) 2017-2026 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 ARYTM_3, POLYNOM2, POLYNOM1, ARYTM_1, FUNCT_1, ABIAN, POLYNOM3,
RELAT_1, FINSEQ_1, AFINSQ_1, VECTSP_1, INT_1, INT_2, ALGSEQ_1, TARSKI,
FUNCT_4, ALGSTR_0, POLYNOM5, PARTFUN1, HURWITZ, ORDINAL1, UPROOTS,
PRE_POLY, SGRAPH1, XCMPLX_0, VECTSP_2, FUNCSDOM, STRUCT_0, SUBSET_1,
SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1, XXREAL_0, RATFUNC1, XXREAL_2,
GROUP_1, FINSET_1, ZFMISC_1, XBOOLE_0, ORDINAL4, NEWTON, CARD_3,
VALUED_0, CAT_1, FUNCOP_1, RING_3, RING_5;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, FUNCT_4, XCMPLX_0, FINSET_1,
CARD_1, XXREAL_0, XXREAL_2, NAT_D, GROUP_4, RELAT_1, RELSET_1, VECTSP_2,
ORDINAL1, NUMBERS, VECTSP_1, FUNCT_1, PARTFUN1, NAT_1, INT_1, INT_2,
RLVECT_1, FINSEQ_1, POLYNOM1, ALGSEQ_1, RVSUM_1, RECDEF_1, ABIAN,
GROUP_1, BINOM, FUNCT_7, ALGSTR_0, STRUCT_0, PRE_POLY, TERMORD, POLYNOM3,
POLYNOM4, POLYNOM5, HURWITZ, RATFUNC1, UPROOTS, RING_2, RING_3, RING_4;
constructors BINOM, RECDEF_1, POLYNOM4, ALGSEQ_1, HURWITZ, FUNCT_4, WSIERP_1,
FVSUM_1, RELSET_1, ABIAN, NAT_D, GROUP_4, RATFUNC1, RING_3, RING_4,
BINOP_2, XXREAL_2, TERMORD;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, NAT_6, ALGSTR_1,
POLYNOM3, POLYNOM4, POLYNOM5, VALUED_0, FUNCT_1, POLYNOM1, ABIAN,
XXREAL_2, PRE_POLY, SUBSET_1, RLVECT_1, FINSET_1, CARD_1, RATFUNC1,
UPROOTS, HURWITZ2, PBOOLE, RING_3, RING_4, EC_PF_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions ALGSTR_0, ALGSEQ_1;
equalities STRUCT_0, VECTSP_1, POLYNOM3, RING_4, BINOM, RATFUNC1;
expansions STRUCT_0, ALGSEQ_1, UPROOTS, RING_4, RATFUNC1, TERMORD;
theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_2, XREAL_1, ORDINAL1,
INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, TARSKI, FUNCT_4, POLYNOM3, XBOOLE_1,
FUNCOP_1, POLYNOM5, XXREAL_0, XBOOLE_0, SUBSET_1, FINSEQ_3, HURWITZ,
GROUP_4, RATFUNC1, NAT_2, PARTFUN1, FINSEQ_2, STRUCT_0, INT_2, ALGSTR_0,
BINOM, RING_3, RING_4, PBOOLE, ABIAN, XXREAL_2, FUNCT_7, VECTSP_2,
XCMPLX_1, CARD_2, PRE_POLY, XREAL_0, NORMSP_1, FUNCT_1, CARD_1, UPROOTS,
POLYNOM1, RVSUM_1, NIVEN;
schemes NAT_1, INT_1, FINSEQ_2;
begin :: Preliminaries
reserve n for Nat;
registration
cluster non trivial non prime for Nat;
existence by NAT_2:def 1,INT_2:29;
end;
T8: for L being non empty ZeroStr, p being Polynomial of L
holds deg p is Element of NAT iff p <> 0_.(L)
proof
let L be non empty ZeroStr;let p be Polynomial of L;
now assume p <> 0_.(L);
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then len p - 1 is Element of NAT by INT_1:3;
hence deg(p) is Element of NAT by HURWITZ:def 2;
end;
hence thesis by HURWITZ:20;
end;
prl4: for R being Ring, a being Element of R holds a |^ 2 = a * a
proof
let R be Ring, a be Element of R;
a |^ (1+1) = (a|^ 1) * (a |^ 1) by BINOM:10
.= a * (a |^ 1) by BINOM:8
.= a * a by BINOM:8;
hence thesis;
end;
theorem XX:
for n being even Nat,
x being Element of F_Real holds x|^n >= 0.F_Real
proof
let n be even Nat, x be Element of F_Real;
defpred P[Nat] means x|^(2*($1)) >= 0.F_Real;
x|^0 = 1_F_Real by BINOM:8;
then IA: P[0];
XX1: for x being Element of F_Real holds x|^2 >= 0.F_Real
proof
let x be Element of F_Real;
per cases;
suppose x >= 0;
then x * x >= 0 * 0;
hence thesis by prl4;
end;
suppose x <= 0;
then x * x >= 0 * 0;
hence thesis by prl4;
end;
end;
IS: now let k be Nat;
assume AS: P[k];
H0: x|^(2*(k+1)) = x|^(2*k+2) .= x|^(2*k) * x|^2 by BINOM:10;
x|^2 >= 0.F_Real by XX1;
hence P[k+1] by H0,AS;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
ex k being Nat st n = 2 * k by ABIAN:def 2;
hence thesis by I;
end;
theorem prl3:
for R being Ring, a being Element of R holds 2 '*' a = a + a
proof
let R be Ring, a be Element of R;
thus 2 '*' a = (1 + 1) '*' a
.= 1 '*' a + 1 '*' a by RING_3:62
.= a + 1 '*' a by RING_3:60
.= a + a by RING_3:60;
end;
theorem
for R being Ring, a being Element of R holds a |^ 2 = a * a by prl4;
registration
let F be Field;
let a be Element of F;
reduce a / 1.F to a;
reducibility
proof
thus a = a * (1.F)" .= a / 1.F by ALGSTR_0:def 43;
end;
end;
registration
cluster Z/2 -> non trivial almost_left_invertible;
coherence by INT_2:28;
end;
registration
let n be non trivial non prime Nat;
cluster Z/n -> non domRing-like;
coherence
proof
set R = Z/n;
not(n = 0 or ... or n = 1) by NAT_2:def 1;
then n > 1;
then consider u being Nat such that
A: u divides n & u <> 1 & u <> n by INT_2:def 4;
consider v being Integer such that B: u * v = n by A,INT_1:def 3;
v >= 0 by B;
then v in NAT by INT_1:3;
then reconsider v as Nat;
A1: u > 1 & u < n
proof
not(u = 0 or ... or u = 1) by A,INT_2:3;
hence u > 1;
u <= n by A,INT_2:27;
hence u < n by A,XXREAL_0:1;
end;
then reconsider u as positive Nat;
B1: v > 1 & v < n
proof
reconsider m = n as Complex;
B2: now assume v = n;
then (u * m) / m = 1 by B,XCMPLX_1:60;
hence contradiction by A,XCMPLX_1:89;
end;
not(v = 0 or ... or v = 1) by A,B;
hence v > 1;
v <= n by B,INT_1:def 3,INT_2:27;
hence v < n by B2,XXREAL_0:1;
end;
then reconsider v as positive Nat;
V: Char R = n by RING_3:def 6;
then C: 0.R = (u * v) '*' 1.R by B,RING_3:def 5
.= (u '*' 1.R) * (v '*' 1.R) by RING_3:67;
D: u '*' 1.R <> 0.R by V,A1,RING_3:def 5;
v '*' 1.R <> 0.R by V,B1,RING_3:def 5;
hence thesis by C,D,VECTSP_2:def 1;
end;
end;
registration
cluster Z/6 -> non degenerated;
coherence
proof
6 is non trivial by NAT_2:def 1;
hence thesis;
end;
end;
begin :: Some More Properties of Polynomials
registration
let R be non degenerated Ring;
cluster -> non-zero for non zero Polynomial of R;
coherence;
cluster monic -> non zero for Polynomial of R;
coherence;
end;
registration
let R be non degenerated Ring;
let p be non zero Polynomial of R;
cluster deg p -> natural;
coherence;
end;
registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> zero;
coherence
proof
p = 0_.(R) by UPROOTS:def 5;
hence thesis by POLYNOM4:2;
end;
cluster q *' p -> zero;
coherence
proof
p = 0_.(R) by UPROOTS:def 5;
hence thesis by POLYNOM3:34;
end;
end;
registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
reduce p + q to q;
reducibility
proof
p = 0_.(R) by UPROOTS:def 5;
hence thesis by POLYNOM3:28;
end;
reduce q + p to q;
reducibility;
end;
registration
let R be Ring;
let p be Polynomial of R;
reduce p *' 0_.(R) to 0_.(R);
reducibility by POLYNOM3:34;
reduce p *' 1_.(R) to p;
reducibility by POLYNOM3:35;
reduce (0_.(R)) *' p to 0_.(R);
reducibility by POLYNOM4:2;
reduce (1_.(R)) *' p to p;
reducibility by RING_4:12;
end;
registration
let R be Ring;
let p be Polynomial of R;
reduce 1.R * p to p;
reducibility by POLYNOM5:27;
end;
Th28: for L be non empty ZeroStr, a be Element of L holds (a|L).0 = a
proof
let L be non empty ZeroStr, a be Element of L;
0 in NAT; then 0 in dom 0_.(L) by FUNCT_2:def 1;
hence a = (a|L).0 by FUNCT_7:31;
end;
Th25a: for R being domRing,
p being Polynomial of R
for a being non zero Element of R holds len(a*p) = len p
proof
let L be domRing, p be Polynomial of L; let v be non zero Element of L;
A2: now let n be Nat;
assume A3: n is_at_least_length_of v*p;
n is_at_least_length_of p
proof
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
assume i >= n;
then (v*p).i = 0.L by A3;
then v*p.i1 = 0.L by POLYNOM5:def 4;
hence thesis by VECTSP_2:def 1;
end;
hence len p <= n by ALGSEQ_1:def 3;
end;
len p is_at_least_length_of (v*p)
proof
let i be Nat;
assume A4: i >= len p;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus (v*p).i = v*p.ii by POLYNOM5:def 4
.= v*0.L by A4,ALGSEQ_1:8 .= 0.L;
end;
hence len(v*p) = len p by A2,ALGSEQ_1:def 3;
end;
theorem Th25:
for R being domRing,
p being Polynomial of R
for a being non zero Element of R holds deg(a*p) = deg p
proof
let L be domRing, p be Polynomial of L; let v be non zero Element of L;
len(v*p) = len p by Th25a;
hence deg(v*p) = len p - 1 by HURWITZ:def 2 .= deg p by HURWITZ:def 2;
end;
theorem prl0a:
for R being domRing,
p being Polynomial of R
for a being Element of R holds LC(a * p) = a * LC(p)
proof
let R be domRing, p be Polynomial of R; let a be Element of R;
per cases;
suppose A1: a = 0.R;
a * p = 0_.(R) by A1,POLYNOM5:26;
hence thesis by A1,FUNCOP_1:7;
end;
suppose a <> 0.R;
then A3: a is non zero;
thus LC(a * p) = a * (p.(len(a*p)-'1)) by POLYNOM5:def 4
.= a * LC(p) by A3,Th25a;
end;
end;
theorem
for R being domRing, a being Element of R holds LC(a|R) = a
proof
let R be domRing, a be Element of R;
thus LC(a|R) = LC(a*(1_.(R))) by RING_4:16
.= a * LC(1_.(R)) by prl0a
.= a * 1.R by RATFUNC1:def 7
.= a;
end;
theorem Th30:
for R being domRing,
p being Polynomial of R
for v,x being Element of R holds eval(v*p,x) = v * eval(p,x)
proof
let L be domRing; let p be Polynomial of L; let v,x be Element of L;
consider F1 be FinSequence of the carrier of L such that
A1: eval(p,x) = Sum F1 and
A2: len F1 = len p and
A3: for n be Element of NAT st n in dom F1
holds F1.n = p.(n-'1) * (power L).(x,n-'1) by POLYNOM4:def 2;
consider F2 be FinSequence of the carrier of L such that
A4: eval(v*p,x) = Sum F2 and
A5: len F2 = len (v*p) and
A6: for n be Element of NAT st n in dom F2
holds F2.n = (v*p).(n-'1) * (power L).(x,n-'1) by POLYNOM4:def 2;
per cases;
suppose v <> 0.L;
then reconsider v1 = v as non zero Element of L by STRUCT_0:def 12;
deg p = deg(v1*p) by Th25;
then len F1 - 1 = deg(v*p) by A2,HURWITZ:def 2
.= len F2 - 1 by A5,HURWITZ:def 2;
then A7: dom F1 = dom F2 by FINSEQ_3:29;
now let i be object;
assume A8: i in dom F1;
then reconsider i1=i as Element of NAT;
A9: p.(i1-'1) * (power L).(x,i1-'1) = F1.i by A3,A8
.= F1/.i by A8,PARTFUN1:def 6;
thus F2/.i = F2.i by A7,A8,PARTFUN1:def 6
.= (v*p).(i1-'1) * (power L).(x,i1-'1) by A6,A7,A8
.= v*p.(i1-'1) * (power L).(x,i1-'1) by POLYNOM5:def 4
.= v*(F1/.i) by A9,GROUP_1:def 3;
end;
then F2 = v*F1 by A7,POLYNOM1:def 1;
hence thesis by A1,A4,POLYNOM1:12;
end;
suppose A10: v = 0.L;
hence eval(v*p,x) = eval(0_.(L),x) by POLYNOM5:26
.= v*eval(p,x) by A10,POLYNOM4:17;
end;
end;
theorem evconst:
for R being Ring, a,b being Element of R holds eval(a|R,b) = a
proof
let R be Ring, a,x be Element of R;
set q = a|R;
consider F being FinSequence of R such that
A3: eval(q,x) = Sum F and
A4: len F = len q and
A5: for j be Element of NAT st j in dom F holds
F.j = q.(j-'1) * (power R).(x,j-'1) by POLYNOM4:def 2;
per cases;
suppose A0: q = 0_.(R);
then q = (0.R)|R by RING_4:13;
then a = 0.R by RING_4:19;
hence eval(q,x) = a by POLYNOM4:17,A0;
end;
suppose q <> 0_.(R);
then q <> (0.R)|R by RING_4:13;
then B: 0 = deg q by RING_4:21 .= len q - 1 by HURWITZ:def 2;
then 1 in Seg(len F) by A4,FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = q.(1-'1) * (power R).(x,1-'1) by A5;
then F = <*q.(1-'1) * (power R).(x,1-'1)*> by A4,B,FINSEQ_1:40
.= <*q.0 * (power R).(x,1-'1)*> by XREAL_1:232
.= <*q.0 * (power R).(x,0)*> by XREAL_1:232
.= <*a * (power R).(x,0)*> by Th28
.= <* a * 1_R *> by GROUP_1:def 7
.= <* a *>;
hence thesis by A3,RLVECT_1:44;
end;
end;
prl2:
for R being non degenerated comRing
for p,q being Polynomial of R
for a being Element of R st a is_a_root_of p holds a is_a_root_of p *' q
proof
let R be non degenerated comRing, p,q be Polynomial of R;
let a be Element of R;
assume a is_a_root_of p;
then eval(p,a) = 0.R by POLYNOM5:def 7;
then eval(p*'q,a) = 0.R * eval(q,a) by POLYNOM4:24 .= 0.R;
hence thesis by POLYNOM5:def 7;
end;
registration
let R be domRing;
let p,q be monic Polynomial of R;
cluster p *' q -> monic;
coherence
proof
LC(p*'q) = (LC p) * (LC q) by NIVEN:46
.= (LC p) * 1.R by RATFUNC1:def 7
.= 1.R * 1.R by RATFUNC1:def 7;
hence thesis;
end;
end;
registration
let R be domRing;
let a be Element of R;
let k be Nat;
cluster rpoly(1,a)`^k -> non zero monic;
coherence
proof
defpred P[Nat] means
rpoly(1,a)`^($1) is non zero monic;
rpoly(1,a)`^0 = 1_.(R) by POLYNOM5:15; then
IA: P[0];
IS: now let k be Nat;
assume P[k];
then (rpoly(1,a)`^k) *' rpoly(1,a) is monic;
hence P[k+1] by POLYNOM5:19;
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
end;
theorem lcrpol:
for R being non degenerated Ring,
a being Element of R,
k being non zero Element of NAT holds LC rpoly(k,a) = 1.R
proof
let R be non degenerated Ring, a be Element of R, k be non zero Element of NAT;
deg rpoly(k,a) = len rpoly(k,a) - 1 by HURWITZ:def 2;
then k = len rpoly(k,a) - 1 by HURWITZ:27;
hence LC rpoly(k,a) = rpoly(k,a).k by XREAL_0:def 2
.= 1_R by HURWITZ:25
.= 1.R;
end;
theorem repr:
for R being non degenerated well-unital non empty doubleLoopStr
for a being Element of R holds <%-a, 1.R%> = rpoly(1,a)
proof
let R be non degenerated well-unital non empty doubleLoopStr,
a be Element of R;
set p = <%-a, 1.R%>, q = rpoly(1,a);
A: 1 = deg q by HURWITZ:27 .= len q - 1 by HURWITZ:def 2;
D: 1.R <> 0.R;
now let k be Nat;
assume k < len p;
then k < 1 + 1 by D,POLYNOM5:40;
then B: k <= 1 by NAT_1:13;
per cases by B,NAT_1:25;
suppose C: k = 0;
hence p.k = -(1_R * a) by POLYNOM5:38
.= -(power(R).(a,0) * a) by GROUP_1:def 7
.= -power(R).(a,0+1) by GROUP_1:def 7
.= q.k by C,HURWITZ:25;
end;
suppose C: k = 1;
hence p.k = 1_R by POLYNOM5:38 .= q.k by C,HURWITZ:25;
end;
end;
hence thesis by A,D,POLYNOM5:40,ALGSEQ_1:12;
end;
theorem Th9:
for R being domRing
for p being Polynomial of R
for x being Element of R holds eval(p,x) = 0.R iff rpoly(1,x) divides p
proof
let L be domRing; let p be Polynomial of L; let x be Element of L;
A1: now assume rpoly(1,x) divides p;
then consider u being Polynomial of L such that
A2: rpoly(1,x) *' u = p by RING_4:1;
A3: eval(rpoly(1,x),x) = x - x by HURWITZ:29 .= 0.L by RLVECT_1:15;
thus eval(p,x) = eval(rpoly(1,x),x) * eval(u,x) by A2,POLYNOM4:24
.= 0.L by A3;
end;
now assume eval(p,x) = 0.L;
then consider s being Polynomial of L
such that A4: p = rpoly(1,x) *' s by HURWITZ:33,POLYNOM5:def 7;
thus rpoly(1,x) divides p by RING_4:1,A4;
end;
hence thesis by A1;
end;
theorem
for F being domRing,
p,q being Polynomial of F
for a being Element of F
st rpoly(1,a) divides (p*'q) holds rpoly(1,a) divides p or rpoly(1,a) divides q
proof
let L be domRing, p,q be Polynomial of L; let x be Element of L;
assume rpoly(1,x) divides (p*'q);
then eval(p*'q,x) = 0.L by Th9;
then A1: eval(p,x) * eval(q,x) = 0.L by POLYNOM4:24;
per cases by A1,VECTSP_2:def 1;
suppose eval(p,x) = 0.L;
hence thesis by Th9;
end;
suppose eval(q,x) = 0.L;
hence thesis by Th9;
end;
end;
theorem prl25:
for R being domRing,
p being Polynomial of R
for q being non zero Polynomial of R st p divides q holds deg p <= deg q
proof
let R be domRing, p be Polynomial of R;
let q being non zero Polynomial of R;
assume p divides q;
then consider r being Polynomial of R such that
A: q = p *' r by RING_4:1;
C: p <> 0_.(R) & r <> 0_.(R) by A;
then reconsider dq = deg q, dr = deg r, dp = deg p as Element of NAT by T8;
dq = dr + dp by A,C,HURWITZ:23;
hence thesis by NAT_1:11;
end;
theorem divi1:
for R being non degenerated comRing,
q being Polynomial of R
for p being non zero Polynomial of R
for b being non zero Element of R st q divides p holds q divides (b*p)
proof
let F be non degenerated comRing, q be Polynomial of F;
let p be non zero Polynomial of F; let b be non zero Element of F;
assume q divides p;
then consider r being Polynomial of F such that
A: p = q *' r by RING_4:1;
b * (r *' q) = (b * r) *' q by HURWITZ:19;
hence q divides (b*p) by A,RING_4:1;
end;
theorem
for F being Field,
q being Polynomial of F
for p being non zero Polynomial of F
for b being non zero Element of F holds q divides p iff q divides (b*p)
proof
let F be Field, q be Polynomial of F;
let p be non zero Polynomial of F; let b be non zero Element of F;
X: b <> 0.F;
now assume q divides (b*p);
then consider r being Polynomial of F such that
A: b * p = q *' r by RING_4:1;
q *' (b" * r) = b" * (q *' r) by HURWITZ:19
.= (b" * b) * p by A,HURWITZ:14
.= 1.F * p by X,VECTSP_1:def 10
.= p;
hence q divides p by RING_4:1;
end;
hence thesis by divi1;
end;
theorem divi1b:
for R being domRing,
p being non zero Polynomial of R
for a being Element of R,
b being non zero Element of R
holds rpoly(1,a) divides p iff rpoly(1,a) divides (b * p)
proof
let F be domRing, p be non zero Polynomial of F;
let a be Element of F, b be non zero Element of F;
set q = rpoly(1,a);
now assume q divides (b*p);
then 0.F = eval(b*p,a) by Th9 .= b * eval(p,a) by Th30;
then eval(p,a) = 0.F by VECTSP_2:def 1;
hence q divides p by Th9;
end;
hence thesis by divi1;
end;
theorem divi1ad:
for R being domRing,
p being non zero Polynomial of R
for a being Element of R,
b being non zero Element of R
holds rpoly(1,a)`^n divides p iff rpoly(1,a)`^n divides (b * p)
proof
let R be domRing, p be non zero Polynomial of R;
let a be Element of R, b be non zero Element of R;
defpred P[Nat] means
rpoly(1,a)`^($1) divides (b*p) implies rpoly(1,a)`^($1) divides p;
now assume rpoly(1,a)`^0 divides (b*p);
rpoly(1,a)`^0 = 1_.(R) by POLYNOM5:15;
then (rpoly(1,a)`^0) *' p = p;
hence rpoly(1,a)`^0 divides p by RING_4:1;
end;
then IA: P[0];
IS: now let k be Nat;
assume AS: P[k];
now assume rpoly(1,a)`^(k+1) divides (b*p);
then consider r being Polynomial of R such that
A1: (rpoly(1,a)`^(k+1)) *' r = b*p by RING_4:1;
C: (rpoly(1,a)`^k) *' (rpoly(1,a) *' r)
= ((rpoly(1,a)`^k) *' rpoly(1,a)) *' r by POLYNOM3:33
.= b*p by A1,POLYNOM5:19;
then consider r1 being Polynomial of R such that
A2: (rpoly(1,a)`^k) *' r1 = p by AS,RING_4:1;
reconsider r1 as non zero Polynomial of R by A2;
(b*r1) *' (rpoly(1,a)`^k)
= (rpoly(1,a) *' r) *' (rpoly(1,a)`^k) by C,A2,RATFUNC1:5;
then b * r1 = rpoly(1,a) *' r by RATFUNC1:7;
then rpoly(1,a) divides r1 by divi1b,RING_4:1;
then consider r2 being Polynomial of R such that
A3: rpoly(1,a) *' r2 = r1 by RING_4:1;
p = ((rpoly(1,a)`^k) *' rpoly(1,a)) *' r2 by A2,A3,POLYNOM3:33
.= (rpoly(1,a)`^(k+1)) *' r2 by POLYNOM5:19;
hence rpoly(1,a)`^(k+1) divides p by RING_4:1;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis by divi1;
end;
registration
let R be domRing;
let p be non zero Polynomial of R;
let b be non zero Element of R;
cluster b * p -> non zero;
coherence
proof
for p being Polynomial of R
st (for a being Element of NAT holds p.a = 0.R) holds p = 0_.(R)
proof
let p be Polynomial of R;
assume AS: for a being Element of NAT holds p.a = 0.R;
now assume len p <> 0;
then consider k being Nat such that D3: len p = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
p.k <> 0.R by D3,ALGSEQ_1:10;
hence contradiction by AS;
end;
hence thesis by POLYNOM4:5;
end;
then consider a being Element of NAT such that A: p.a <> 0.R;
b * (p.a) <> 0.R by A,VECTSP_2:def 1;
then (b*p).a <> 0.R by POLYNOM5:def 4;
hence thesis by FUNCOP_1:7;
end;
end;
begin :: On Roots of Polynomials
registration
let R be non degenerated Ring;
cluster 1_.(R) -> non with_roots;
coherence
proof
set p = 1_.(R);
assume p is with_roots;
then consider x being Element of R such that
A: x is_a_root_of p by POLYNOM5:def 8;
0.R = eval(p,x) by A,POLYNOM5:def 7 .= 1.R by POLYNOM4:18;
hence contradiction;
end;
end;
registration
let R be non degenerated Ring;
let a be non zero Element of R;
cluster a|R -> non with_roots;
coherence
proof
set p = a|R;
assume p is with_roots;
then consider x being Element of R such that
A: x is_a_root_of p by POLYNOM5:def 8;
0.R = eval(p,x) by A,POLYNOM5:def 7 .= a by evconst;
hence contradiction;
end;
end;
registration
let R be non degenerated Ring;
cluster non zero with_roots -> non constant for Polynomial of R;
coherence
proof
let q be Polynomial of R;
assume AS: q is non zero with_roots;
reconsider p = q as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
reconsider degp = deg p as Element of NAT by AS,T8;
consider x being Element of R such that
X: x is_a_root_of p by AS,POLYNOM5:def 8;
H: eval(p,x) = 0.R by X,POLYNOM5:def 7;
now assume A: p is constant;
then consider a being Element of R such that B: p = a|R by RING_4:20;
degp = 0 by A;
then a <> 0.R by B,RING_4:21;
hence contradiction by H,B,evconst;
end;
hence thesis;
end;
end;
registration
let R be non degenerated Ring;
cluster non with_roots -> non zero for Polynomial of R;
coherence;
end;
registration
let R be non degenerated Ring;
let a be Element of R;
cluster rpoly(1,a) -> non zero with_roots;
coherence by HURWITZ:30,POLYNOM5:def 8;
end;
registration
let R be non degenerated Ring;
cluster non zero non with_roots for Polynomial of R;
existence
proof
take 1_.(R);
thus thesis;
end;
cluster non zero with_roots for Polynomial of R;
existence
proof
take rpoly(1,1.R);
thus thesis;
end;
end;
registration
let R be domRing;
let p be non with_roots Polynomial of R;
let a be non zero Element of R;
cluster a * p -> non with_roots;
coherence
proof
now assume a * p is with_roots;
then consider b being Element of R such that
A: b is_a_root_of (a*p) by POLYNOM5:def 8;
0.R = eval(a*p,b) by A,POLYNOM5:def 7
.= a * eval(p,b) by Th30;
then eval(p,b) = 0.R by VECTSP_2:def 1;
hence contradiction by POLYNOM5:def 8,POLYNOM5:def 7;
end;
hence thesis;
end;
end;
registration
let R be domRing;
let p be with_roots Polynomial of R;
let a be Element of R;
cluster a * p -> with_roots;
coherence
proof
consider b being Element of R such that
A: b is_a_root_of p by POLYNOM5:def 8;
eval(a*p,b) = a * eval(p,b) by Th30 .= a * 0.R by A,POLYNOM5:def 7;
hence thesis by POLYNOM5:def 8,POLYNOM5:def 7;
end;
end;
registration
let R be non degenerated comRing;
let p be with_roots Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> with_roots;
coherence
proof
consider a being Element of R such that A: a is_a_root_of p by POLYNOM5:def 8;
thus thesis by A,prl2,POLYNOM5:def 8;
end;
end;
registration
let R be domRing;
let p,q be non with_roots Polynomial of R;
cluster p *' q -> non with_roots;
coherence
proof
now assume p *' q is with_roots;
then consider a being Element of R such that
H: a is_a_root_of (p *' q) by POLYNOM5:def 8;
A: 0.R = eval(p*'q,a) by H,POLYNOM5:def 7
.= eval(p,a) * eval(q,a) by POLYNOM4:24;
per cases by A,VECTSP_2:def 1;
suppose eval(p,a) = 0.R;
hence contradiction by POLYNOM5:def 8,POLYNOM5:def 7;
end;
suppose eval(q,a) = 0.R;
hence contradiction by POLYNOM5:def 8,POLYNOM5:def 7;
end;
end;
hence thesis;
end;
end;
registration
let R be non degenerated comRing;
let a be Element of R;
let k be non zero Element of NAT;
cluster rpoly(k,a) -> non constant monic with_roots;
coherence
proof
set p = rpoly(k,a);
thus p is non constant by HURWITZ:27;
deg p >= 0;
then len p - 1 >= 0 by HURWITZ:def 2;
then 0 + 1 <= (len p - 1) + 1 by XREAL_1:6;
then A: len p -' 1 = len p - 1 by XREAL_1:233 .= deg p by HURWITZ:def 2;
LC p = p.k by A,HURWITZ:27 .= 1_R by HURWITZ:25 .= 1.R;
hence p is monic;
per cases by NAT_1:53;
suppose k = 1;
hence p is with_roots;
end;
suppose k > 1;
then rpoly(1,a) *' qpoly(k,a) = rpoly(k,a) by HURWITZ:32;
hence p is with_roots;
end;
end;
end;
registration
let R be non degenerated Ring;
cluster non constant monic for Polynomial of R;
existence
proof
take rpoly(1,1.R);
thus thesis;
end;
end;
registration
let R be domRing;
let a be Element of R;
let k be non zero Nat;
let n be non zero Element of NAT;
cluster rpoly(n,a)`^k -> non constant monic with_roots;
coherence
proof
defpred P[Nat] means
rpoly(n,a)`^($1) is non constant monic with_roots;
IA: P[1] by POLYNOM5:16;
IS: now let k be Nat;
assume 1 <= k;
assume P[k];
then (rpoly(n,a)`^k) *' rpoly(n,a) is non constant monic with_roots;
hence P[k+1] by POLYNOM5:19;
end;
I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(IA,IS);
1 <= k by NAT_1:53;
hence thesis by I;
end;
end;
registration
let R be Ring;
let p be with_roots Polynomial of R;
cluster Roots(p) -> non empty;
coherence
proof
ex x being Element of R st x is_a_root_of p by POLYNOM5:def 8;
hence thesis by POLYNOM5:def 10;
end;
end;
registration
let R be non degenerated Ring;
let p be non with_roots Polynomial of R;
cluster Roots(p) -> empty;
coherence
proof
now assume A: Roots p <> {};
let u be Element of Roots(p);
u in Roots(p) by A;
then reconsider x = u as Element of R;
x is_a_root_of p by A,POLYNOM5:def 10;
hence contradiction by POLYNOM5:def 8;
end;
hence thesis;
end;
end;
registration
let R be domRing;
cluster monic with_roots for Polynomial of R;
existence
proof
take rpoly(1,0.R);
thus thesis;
end;
cluster monic non with_roots for Polynomial of R;
existence
proof
take 1_.(R);
thus thesis;
end;
end;
theorem ro4:
for R being non degenerated Ring,
a being Element of R holds Roots rpoly(1,a) = {a}
proof
let R be non degenerated Ring, a be Element of R;
set p = rpoly(1,a);
A: now let u be object;
assume u in {a};
then A: u = a by TARSKI:def 1;
eval(p,a) = a - a by HURWITZ:29 .= 0.R by RLVECT_1:15;
then a is_a_root_of p by POLYNOM5:def 7;
hence u in Roots(p) by A,POLYNOM5:def 10;
end;
now let u be object;
assume B: u in Roots(p);
then reconsider x = u as Element of R;
x is_a_root_of p by B,POLYNOM5:def 10;
then 0.R = eval(p,x) by POLYNOM5:def 7 .= x - a by HURWITZ:29;
then a = x by RLVECT_1:21;
hence u in {a} by TARSKI:def 1;
end;
hence thesis by A,TARSKI:2;
end;
theorem
for F being domRing,
p being Polynomial of F
for b being non zero Element of F holds Roots(b * p) = Roots p
proof
let R be domRing, p be Polynomial of R; let b be non zero Element of R;
A: now let o be object;
assume B0: o in Roots p;
then reconsider a = o as Element of R;
a is_a_root_of p by B0,POLYNOM5:def 10;
then 0.R = eval(p,a) by POLYNOM5:def 7;
then eval(b*p,a) = b * 0.R by Th30 .= 0.R;
then a is_a_root_of (b*p) by POLYNOM5:def 7;
hence o in Roots(b*p) by POLYNOM5:def 10;
end;
now let o be object;
assume B0: o in Roots(b*p);
then reconsider a = o as Element of R;
a is_a_root_of (b*p) by B0,POLYNOM5:def 10;
then 0.R = eval(b*p,a) by POLYNOM5:def 7
.= b * eval(p,a) by Th30;
then eval(p,a) = 0.R by VECTSP_2:def 1;
then a is_a_root_of p by POLYNOM5:def 7;
hence o in Roots p by POLYNOM5:def 10;
end;
hence thesis by A,TARSKI:2;
end;
theorem
ex p,q being Polynomial of Z/6 st not Roots(p*'q) c= Roots(p) \/ Roots(q)
proof
set R = Z/6, z = 2 '*' 1.(Z/6), d = 3 '*' 1.(Z/6);
take p = rpoly(1,z), q = rpoly(1,d);
C: Char R = 6 by RING_3:77;
eval(p*'q,0.R) = eval(p,0.R) * eval(q,0.R) by POLYNOM4:24
.= (0.R - z) * eval(q,0.R) by HURWITZ:29
.= (0.R - z) * (0.R - d) by HURWITZ:29
.= (-z) * (0.R - d) by RLVECT_1:14
.= (-z) * (- d) by RLVECT_1:14
.= z * d by VECTSP_1:10
.= (2 * 3) '*' 1.R by RING_3:67
.= 0.R by C,RING_3:def 5;
then 0.R is_a_root_of (p*'q) by POLYNOM5:def 7;
then B: 0.R in Roots(p*'q) by POLYNOM5:def 10;
now assume AS: 0.R in Roots(p) \/ Roots(q);
per cases by AS,XBOOLE_0:def 3;
suppose 0.R in Roots(p);
then 0.R is_a_root_of p by POLYNOM5:def 10;
then B: 0.R = eval(p,0.R) by POLYNOM5:def 7
.= 0.R - z by HURWITZ:29
.= - z by RLVECT_1:14;
z = --z .= 0.R by B;
hence contradiction by C,RING_3:def 5;
end;
suppose 0.R in Roots(q);
then 0.R is_a_root_of q by POLYNOM5:def 10;
then B: 0.R = eval(q,0.R) by POLYNOM5:def 7
.= 0.R - d by HURWITZ:29
.= - d by RLVECT_1:14;
d = --d .= 0.R by B;
hence contradiction by C,RING_3:def 5;
end;
end;
hence thesis by B;
end;
theorem div100:
for R being domRing,
a,b being Element of R holds rpoly(1,a) divides rpoly(1,b) iff a = b
proof
let R be domRing, a,b be Element of R;
X: now assume rpoly(1,a) divides rpoly(1,b);
then consider p being Polynomial of R such that
A: rpoly(1,a) *' p = rpoly(1,b) by RING_4:1;
B: {b} = Roots rpoly(1,b) by ro4 .= Roots rpoly(1,a) \/ Roots p
by A,UPROOTS:23;
a in {a} by TARSKI:def 1;
then a in Roots rpoly(1,a) by ro4;
then a in {b} by B,XBOOLE_0:def 3;
hence a = b by TARSKI:def 1;
end;
now assume a = b;
then rpoly(1,a) *' 1_.(R) = rpoly(1,b);
hence rpoly(1,a) divides rpoly(1,b) by RING_4:1;
end;
hence thesis by X;
end;
degpol:
for R being domRing
for p being non zero Polynomial of R
ex n being natural number st n = card(Roots p) & n <= deg p
proof
let R be domRing, p be non zero Polynomial of R;
defpred P[Nat] means
for p being non zero Polynomial of R st deg p = $1
ex n being natural number st n = card(Roots p) & n <= deg p;
IA: P[0]
proof
let p be non zero Polynomial of R;
assume A1: deg p = 0;
reconsider q = p as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
consider a being Element of R such that
A2: q = a|R by A1,RING_4:def 4,RING_4:20;
now assume A3: Roots(p) <> {};
let u be Element of Roots(p);
u in Roots(p) by A3;
then reconsider u as Element of R;
u is_a_root_of p by A3,POLYNOM5:def 10;
then eval(p,u) = 0.R by POLYNOM5:def 7;
then a = 0.R by A2,evconst;
hence contradiction by A2;
end;
hence ex n being natural number st n = card(Roots p) & n <= deg p;
end;
IS: now let k be Nat;
assume IV: P[k];
now let p be non zero Polynomial of R;
assume A1: deg p = k+1;
per cases;
suppose ex x being Element of R st x is_a_root_of p;
then consider x being Element of R such that A2: x is_a_root_of p;
consider q being Polynomial of R such that
A3: p = rpoly(1,x) *' q by A2,HURWITZ:33;
A4: q <> 0_.(R) by A3;
reconsider q as non zero Polynomial of R by A3;
A7: deg p = deg q + deg rpoly(1,x) by HURWITZ:23,A3,A4
.= deg q + 1 by HURWITZ:27;
then consider m being natural number such that
A5: m = card(Roots q) & m <= deg q by A1,IV;
reconsider RQ = Roots q as finite Subset of R;
now per cases;
case x in Roots q;
then for o being object st o in {x} holds o in Roots q by TARSKI:def 1;
then A6: card(RQ \/ {x}) = m by A5,XBOOLE_1:12,TARSKI:def 3;
Roots(rpoly(1,x)) = {x} by ro4;
then A8: card(Roots p) = m by A3,A6,UPROOTS:23;
deg q <= deg q + 1 by NAT_1:11;
hence ex n being natural number st n = card(Roots p) & n <= deg p
by A7,A8,A5,XXREAL_0:2;
end;
case not(x in Roots q);
then A6: card(RQ \/ {x}) = m + 1 by A5,CARD_2:41;
Roots(rpoly(1,x)) = {x} by ro4;
then card(Roots p) = m + 1 by A3,A6,UPROOTS:23;
hence ex n being natural number st n = card(Roots p) & n <= deg p
by A7,A5,XREAL_1:6;
end;
end;
hence ex n being natural number st n = card(Roots p) & n <= deg p;
end;
suppose A2: not ex x being Element of R st x is_a_root_of p;
now assume A3: Roots(p) <> {};
let x be Element of Roots(p);
x in Roots(p) by A3; then
reconsider x as Element of R;
x is_a_root_of p by A3,POLYNOM5:def 10;
hence contradiction by A2;
end;
hence ex n being natural number st n = card(Roots p) & n <= deg p;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
p <> 0_.(R);
then deg p is Element of NAT by T8;
hence thesis by I;
end;
theorem degpoly:
for R being domRing,
p being non zero Polynomial of R holds card(Roots p) <= deg p
proof
let R be domRing, p be non zero Polynomial of R;
ex n being natural number st n = card(Roots p) & n <= deg p by degpol;
hence thesis;
end;
begin :: More about Bags
notation
let X be non empty set;
let B be bag of X;
synonym card B for Sum B;
end;
bbbag: for X being non empty set,
b being bag of X holds b is zero iff rng b = {0}
proof
let X be non empty set, b be bag of X;
A: now assume B: b is zero;
C: now let o be object;
assume o in rng b;
then consider y being object such that
D: y in dom b & b.y = o by FUNCT_1:def 3;
o = 0 by B,D;
hence o in {0} by TARSKI:def 1;
end;
now let o be object;
assume o in {0};
then D: o = 0 by TARSKI:def 1;
set y = the Element of X;
E: dom b = X by PARTFUN1:def 2;
b.y = 0 by B;
hence o in rng b by D,E,FUNCT_1:def 3;
end;
hence rng b = {0} by C,TARSKI:2;
end;
now assume B: rng b = {0};
now let o be object;
assume o in X;
then o in dom b by PARTFUN1:def 2;
then b.o in rng b by FUNCT_1:3;
hence b.o = {} by B,TARSKI:def 1;
end;
hence b is zero by PBOOLE:6;
end;
hence thesis by A;
end;
registration
let X be non empty set;
cluster zero for bag of X;
existence
proof
take EmptyBag X; thus thesis;
end;
cluster non zero for bag of X;
existence
proof
set x = the Element of X;
reconsider b = ({x},1)-bag as bag of X;
take b;
D: support b c= dom b by PRE_POLY:37;
x in {x} by TARSKI:def 1;
then A: b.x = 1 by UPROOTS:7;
then C: x in support b by PRE_POLY:def 7;
now assume rng b = {0};
then b.x in {0} by C,D,FUNCT_1:3;
hence contradiction by A,TARSKI:def 1;
end;
hence thesis by bbbag;
end;
end;
registration
let X be non empty set;
let b1 be bag of X;
let b2 be bag of X;
cluster b1 + b2 -> X-defined;
coherence;
end;
registration
let X be non empty set;
let b1 be bag of X;
let b2 be bag of X;
cluster b1 + b2 -> total;
coherence;
end;
theorem bag1a:
for X being non empty set,
b being bag of X holds card b = 0 iff support b = {}
proof
let X be non empty set, b be bag of X;
A: now assume support b = {};
then b = EmptyBag X by PRE_POLY:81;
hence card b = 0 by UPROOTS:11;
end;
now assume card b = 0;
then b = EmptyBag X by UPROOTS:12;
hence support b = {};
end;
hence thesis by A;
end;
theorem bbag:
for X being non empty set,
b being bag of X holds b is zero iff support b = {}
proof
let X being non empty set, b being bag of X;
now assume support b = {};
then for o be object st o in X holds b.o = {} by PRE_POLY:def 7;
hence b is zero by PBOOLE:6;
end;
hence thesis;
end;
theorem
for X being non empty set,
b being bag of X holds b is zero iff rng b = {0} by bbbag;
registration
let X be non empty set;
let b1 be non zero bag of X;
let b2 be bag of X;
cluster b1 + b2 -> non zero;
coherence
proof
A: support b1 <> {} by bbag;
set o = the Element of support b1;
D: b1.o <> 0 by A,PRE_POLY:def 7;
set b = b1 + b2;
b.o = b1.o + b2.o by PRE_POLY:def 5;
hence thesis by D;
end;
end;
theorem bb7a:
for X being non empty set,
b being bag of X,
x being Element of X holds support b = {x} implies b = ({x},b.x)-bag
proof
let X be non empty set, b be bag of X, x be Element of X;
assume AS: support b = {x};
now let o be object;
assume o in X;
per cases;
suppose A: o = x;
then o in {x} by TARSKI:def 1;
hence b.o = (({x},b.x)-bag).o by A,UPROOTS:7;
end;
suppose o <> x;
then B: not o in {x} by TARSKI:def 1;
hence (({x},b.x)-bag).o = 0 by UPROOTS:6
.= b.o by AS,B,PRE_POLY:def 7;
end;
end;
hence b = ({x},b.x)-bag by PBOOLE:3;
end;
theorem bb7:
for X being non empty set,
b being non empty bag of X,
x being Element of X
holds support b = {x} iff (b = ({x},b.x)-bag & b.x <> 0)
proof
let X be non empty set, b be non empty bag of X, x be Element of X;
now assume AS: support b = {x};
then x in support b by TARSKI:def 1;
hence b = ({x},b.x)-bag & b.x <> 0 by AS,bb7a,PRE_POLY:def 7;
end;
hence thesis by UPROOTS:8;
end;
definition
let X be set;
let S be finite Subset of X;
func Bag S -> bag of X equals
(S,1)-bag;
coherence;
end;
registration
let X be non empty set;
let S be non empty finite Subset of X;
cluster Bag S -> non zero;
coherence
proof
set x = the Element of S;
reconsider x as Element of X;
B: dom(Bag S) = X by PARTFUN1:def 2;
(Bag S).x = 1 by UPROOTS:7;
then 1 in rng(Bag S) by B,FUNCT_1:3;
then rng(Bag S) <> {0} by TARSKI:def 1;
hence thesis by bbbag;
end;
end;
definition
let X be non empty set;
let b be bag of X;
let a be Element of X;
func b \ a -> bag of X equals
b +* (a,0);
coherence;
end;
bb1:for X being non empty set, b being bag of X,
a being Element of X holds (b \ a).a = 0
proof
let X be non empty set, b be bag of X, a be Element of X;
X = dom b by PARTFUN1:def 2;
hence thesis by FUNCT_7:31;
end;
theorem
for X being non empty set,
b being bag of X,
a being Element of X holds b \ a = b iff not a in support b
proof
let X be non empty set, b be bag of X, a be Element of X;
A: now assume B: not a in support b;
now let o be object;
assume o in X;
per cases;
suppose D: o = a;
hence (b\a).o = 0 by bb1 .= b.o by B,D,PRE_POLY:def 7;
end;
suppose o <> a;
hence (b\a).o = b.o by FUNCT_7:32;
end;
end;
hence b \ a = b by PBOOLE:3;
end;
now assume b \ a = b;
then b.a = 0 by bb1;
hence not a in support b by PRE_POLY:def 7;
end;
hence thesis by A;
end;
theorem bb3a:
for X being non empty set,
b being bag of X,
a being Element of X holds support(b \ a) = support b \ {a}
proof
let X be non empty set, b be bag of X, a be Element of X;
A: now let o be object;
assume X: o in support(b \ a);
then reconsider c = o as Element of X;
B: (b\a).o <> 0 by X,PRE_POLY:def 7;
then D: a <> o by bb1;
then b.c = (b\a).c by FUNCT_7:32;
then C: o in support b by B,PRE_POLY:def 7;
not o in {a} by D,TARSKI:def 1;
hence o in support b \ {a} by C,XBOOLE_0:def 5;
end;
now let o be object;
assume X: o in support b \ {a};
then reconsider c = o as Element of X;
B: o in support b & not o in {a} by X,XBOOLE_0:def 5;
then o <> a by TARSKI:def 1;
then (b\a).c = b.c by FUNCT_7:32;
then (b\a).o <> 0 by B,PRE_POLY:def 7;
hence o in support(b \ a) by PRE_POLY:def 7;
end;
hence thesis by A,TARSKI:2;
end;
theorem bb3:
for X being non empty set,
b being bag of X,
a being Element of X holds (b \ a) + ({a},b.a)-bag = b
proof
let X be non empty set, b be bag of X, a be Element of X;
set c = (b \ a) + ({a},b.a)-bag;
now let o be object;
assume o in X;
X: c.o = (b \ a).o + (({a},b.a)-bag).o by PRE_POLY:def 5;
per cases;
suppose A: o = a;
then B: o in {a} by TARSKI:def 1;
thus c.o = 0 + (({a},b.a)-bag).o by A,X,bb1
.= b.o by A,B,UPROOTS:7;
end;
suppose A: o <> a;
then not o in {a} by TARSKI:def 1;
hence c.o = (b \ a).o + 0 by X,UPROOTS:6
.= b.o by A,FUNCT_7:32;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem bb4:
for X being non empty set,
a being Element of X,
n being Element of NAT holds card(({a},n)-bag) = n
proof
let X be non empty set, a be Element of X, n be Element of NAT;
reconsider b = ({a},n)-bag as bag of X;
consider F being FinSequence of NAT such that
H: degree b = Sum F & F = b*canFS(support b) by UPROOTS:def 4;
I: a in {a} by TARSKI:def 1;
per cases;
suppose X: n = 0;
then b = EmptyBag X by UPROOTS:9;
then support b = {};
hence thesis by X,bag1a;
end;
suppose n <> 0;
then A: support b = {a} by UPROOTS:8;
then C: a in support b by TARSKI:def 1;
B: support b c= dom b by PRE_POLY:37;
F = b * <*a*> by A,H,FINSEQ_1:94
.= <*b.a*> by C,B,FINSEQ_2:34
.= <*n*> by I,UPROOTS:7;
hence thesis by H,RVSUM_1:73;
end;
end;
begin :: On Multiple Roots of Polynomials
registration
let R be domRing;
let p be non zero with_roots Polynomial of R;
cluster BRoots p -> non zero;
coherence
proof
consider x being Element of R such that
A: x is_a_root_of p by POLYNOM5:def 8;
multiplicity(p,x) >= 1 by A,UPROOTS:52;
then (BRoots p).x >= 1 by UPROOTS:def 9;
hence thesis;
end;
end;
theorem multipp0:
for R being non degenerated comRing,
p being non zero Polynomial of R
for a being Element of R
holds multiplicity(p,a) = 0 iff not rpoly(1,a) divides p
proof
let R be non degenerated comRing, p be non zero Polynomial of R;
let a be Element of R;
A: now assume multiplicity(p,a) = 0;
then C: not(a is_a_root_of p) by UPROOTS:52;
now assume rpoly(1,a) divides p;
then consider s being Polynomial of R such that
B: p = rpoly(1,a) *' s by RING_4:1;
thus contradiction by C,B,prl2,HURWITZ:30;
end;
hence not rpoly(1,a) divides p;
end;
now assume multiplicity(p,a) <> 0;
then multiplicity(p,a) + 1 > 0 + 1 by XREAL_1:6;
then multiplicity(p,a) >= 1 by NAT_1:13; then
ex s being Polynomial of R st p = rpoly(1,a) *' s by UPROOTS:52,HURWITZ:33;
hence rpoly(1,a) divides p by RING_4:1;
end;
hence thesis by A;
end;
theorem multip:
for R being domRing,
p being non zero Polynomial of R
for a being Element of R
holds multiplicity(p,a) = n
iff (rpoly(1,a)`^n divides p & not rpoly(1,a)`^(n+1) divides p)
proof
let R be domRing, p be non zero Polynomial of R;
let a be Element of R;
A: now assume multiplicity(p,a) = n;
then consider F being finite non empty Subset of NAT such that
B: F = {k where k is Element of NAT : ex q being Polynomial of R
st p = (<%-a, 1.R%>`^k) *' q} & n = max F by UPROOTS:def 8;
n in F by B,XXREAL_2:def 6; then
consider k being Element of NAT such that
C: k = n & ex q being Polynomial of R st p = (<%-a, 1.R%>`^k) *' q by B;
consider q being Polynomial of R such that
D: p = (<%-a, 1.R%>`^n) *' q by C;
p = (rpoly(1,a)`^n) *' q by D,repr;
hence rpoly(1,a)`^n divides p by RING_4:1;
F: n is UpperBound of F by B,XXREAL_2:def 3;
now assume rpoly(1,a)`^(n+1) divides p;
then consider q being Polynomial of R such that
E: p = (rpoly(1,a)`^(n+1)) *' q by RING_4:1;
p = (<%-a, 1.R%>`^(n+1)) *' q by E,repr;
then n+1 in F by B;
hence contradiction by F,XXREAL_2:def 1,NAT_1:16;
end;
hence not rpoly(1,a)`^(n+1) divides p;
end;
now assume X: rpoly(1,a)`^n divides p & not rpoly(1,a)`^(n+1) divides p;
set n0 = multiplicity(p,a);
consider F being finite non empty Subset of NAT such that
B: F = {k where k is Element of NAT : ex q being Polynomial of R
st p = (<%-a, 1.R%>`^k) *' q} & n0 = max F by UPROOTS:def 8;
consider q being Polynomial of R such that
E: p = (rpoly(1,a)`^n) *' q by X,RING_4:1;
K: n in NAT by ORDINAL1:def 12;
p = (<%-a, 1.R%>`^n) *' q by E,repr;
then C: n in F by B,K;
now let k be ExtReal;
assume k in F;
then consider k0 being Element of NAT such that
C: k0 = k & ex q being Polynomial of R st p = (<%-a, 1.R%>`^k0) *' q by B;
consider q being Polynomial of R such that
D: p = (<%-a, 1.R%>`^k0) *' q by C;
now assume k0 >= n + 1;
then consider j being Nat such that
E: k0 = (n + 1) + j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
p = (rpoly(1,a)`^k0) *' q by D,repr
.= ((rpoly(1,a)`^(n+1)) *' (rpoly(1,a)`^j)) *' q by E,UPROOTS:30
.= (rpoly(1,a)`^(n+1)) *' ((rpoly(1,a)`^j) *' q) by POLYNOM3:33;
hence contradiction by X,RING_4:1;
end;
hence k <= n by C,NAT_1:13;
end;
hence multiplicity(p,a) = n by B,C,XXREAL_2:def 8;
end;
hence thesis by A;
end;
theorem BR5aa:
for R being domRing,
a being Element of R holds multiplicity(rpoly(1,a),a) = 1
proof
let R be domRing, a be Element of R;
set p = rpoly(1,a);
p *' 1_.(R) = p;
then p divides p by RING_4:1;
then A: p`^1 divides p by POLYNOM5:16;
p <> 0_.(R);
then deg(p *' p) = deg(p) + deg(p) by HURWITZ:23
.= deg(p) + 1 by HURWITZ:27
.= 1 + 1 by HURWITZ:27;
then deg(p *' p) > 1;
then B: deg(p *' p) > deg(p) by HURWITZ:27;
p *' p = p`^2 by POLYNOM5:17;
then not p`^(1+1) divides p by B,prl25;
hence multiplicity(p,a) = 1 by A,multip;
end;
theorem BR5aaa:
for R being domRing,
a,b being Element of R st b <> a holds multiplicity(rpoly(1,a),b) = 0
proof
let R be domRing, a,b be Element of R;
set p = rpoly(1,a);
assume a <> b;
then not rpoly(1,b) divides rpoly(1,a) by div100;
hence multiplicity(p,b) = 0 by multipp0;
end;
theorem multip1d:
for R being domRing,
p being non zero Polynomial of R
for b being non zero Element of R,
a being Element of R holds multiplicity(p,a) = multiplicity(b*p,a)
proof
let F be domRing, p be non zero Polynomial of F;
let b be non zero Element of F, a be Element of F;
set r = rpoly(1,a), np = multiplicity(p,a);
r`^np divides (b*p) & not r`^(np+1) divides p by multip,divi1;
then r`^np divides (b*p) & not r`^(np+1) divides (b*p) by divi1ad;
hence thesis by multip;
end;
BR3:for R being domRing,
a being non zero Element of R holds support(BRoots a|R) = {}
proof
let R be domRing, a be non zero Element of R;
now assume A: support(BRoots a|R) <> {};
let b be Element of support(BRoots a|R);
b in Roots(a|R) by A,UPROOTS:def 9;
hence contradiction;
end;
hence thesis;
end;
theorem llll:
for R being domRing,
p being non zero Polynomial of R
for b being non zero Element of R holds BRoots(b * p) = BRoots p
proof
let F be domRing, p be non zero Polynomial of F;
let b be non zero Element of F;
now let a be Element of F;
multiplicity(p,a) = multiplicity(b*p,a) by multip1d;
hence (BRoots(b*p)).a = multiplicity(p,a) by UPROOTS:def 9
.= (BRoots p).a by UPROOTS:def 9;
end;
then for o be object holds o in the carrier of F implies
(BRoots(b*p)).o = (BRoots p).o;
hence thesis by PBOOLE:3;
end;
theorem lemacf1:
for R being domRing,
p being non zero non with_roots Polynomial of R
holds BRoots p = EmptyBag(the carrier of R)
proof
let R be domRing, p be non zero non with_roots Polynomial of R;
Roots p is empty;
then support BRoots p = {} by UPROOTS:def 9;
hence thesis by PRE_POLY:81;
end;
theorem bag1:
for R being domRing,
a being non zero Element of R holds card BRoots a|R = 0
proof
let R be domRing, a be non zero Element of R;
support(BRoots a|R) = {} by BR3;
hence thesis by bag1a;
end;
theorem bag2:
for R being domRing,
a being Element of R holds card BRoots rpoly(1,a) = 1
proof
let R be domRing, a be Element of R;
BRoots rpoly(1,a) = BRoots <%-a, 1.R%> by repr
.= ({a}, 1)-bag by UPROOTS:54;
then card BRoots rpoly(1,a) = card {a} by UPROOTS:13;
hence thesis by CARD_1:30;
end;
theorem
for R being domRing,
p,q being non zero Polynomial of R
holds card BRoots(p*'q) = card BRoots p + card BRoots q
proof
let R be domRing, p,q be non zero Polynomial of R;
thus card BRoots(p*'q)
= card(BRoots p + BRoots q) by UPROOTS:56
.= card BRoots p + card BRoots q by UPROOTS:15;
end;
theorem
for R being domRing,
p being non zero Polynomial of R holds card(BRoots p) <= deg p
proof
let R be domRing, p be non zero Polynomial of R;
defpred P[Nat] means
for p being non zero Polynomial of R st deg p = $1
holds card(BRoots p) <= deg p;
IA: P[0]
proof
let p be non zero Polynomial of R;
assume A1: deg p = 0;
reconsider q = p as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
consider a being Element of R such that
A2: q = a|R by A1,RING_4:def 4,RING_4:20;
a <> 0.R by A2;
then reconsider a as non zero Element of R by STRUCT_0:def 12;
q = a|R by A2;
hence card(BRoots p) <= deg p by bag1;
end;
IS: now let k be Nat;
assume IV: P[k];
now let p be non zero Polynomial of R;
assume A1: deg p = k+1;
per cases;
suppose ex x being Element of R st x is_a_root_of p;
then consider x being Element of R such that A2: x is_a_root_of p;
consider q being Polynomial of R such that
A3: p = rpoly(1,x) *' q by A2,HURWITZ:33;
A4: q <> 0_.(R) by A3;
reconsider q as non zero Polynomial of R by A3;
BRoots(p) = BRoots(rpoly(1,x)) + BRoots(q) by A3,UPROOTS:56;
then A6: card BRoots(p)
= card(BRoots(rpoly(1,x))) + card BRoots(q) by UPROOTS:15
.= 1 + card BRoots(q) by bag2;
deg p = deg q + deg rpoly(1,x) by HURWITZ:23,A3,A4
.= deg q + 1 by HURWITZ:27;
hence card(BRoots p) <= deg p by IV,A1,A6,XREAL_1:6;
end;
suppose A2: not ex x being Element of R st x is_a_root_of p;
now assume A3: Roots(p) <> {};
let x be Element of Roots(p);
x in Roots(p) by A3; then
reconsider x as Element of R;
x is_a_root_of p by A3,POLYNOM5:def 10;
hence contradiction by A2;
end;
then support(BRoots p) = {} by UPROOTS:def 9;
hence card(BRoots p) <= deg p by bag1a;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
p <> 0_.(R);
then deg p is Element of NAT by T8;
hence thesis by I;
end;
begin :: The polynomials x^n + 1
Lm10: for L being unital non empty doubleLoopStr holds
(0_.(L) +* (0,n)-->(1.L,1.L)).0 = 1.L &
(0_.(L) +* (0,n)-->(1.L,1.L)).n = 1.L
proof
let L be unital non empty doubleLoopStr;
set t = 0_.(L) +* (0,n)-->(1.L,1.L), f = (0,n)-->(1.L,1.L);
A3: dom(0_.(L)) = NAT by FUNCT_2:def 1;
A4: for u being object holds u in {0,n} implies u in NAT
by ORDINAL1:def 12;
A7: dom f = {0,n} by FUNCT_4:62; then
A5: dom(0_.(L)) \/ dom(f) = NAT by A3,A4,TARSKI:def 3,XBOOLE_1:12;
n in dom f &
n in dom(0_.(L)) \/ dom(f) by A5,A7,TARSKI:def 2,ORDINAL1:def 12;
then A10: t.n = f.n by FUNCT_4:def 1
.= 1.L by FUNCT_4:63;
per cases;
suppose n = 0;
hence thesis by A10;
end;
suppose A6: n <> 0;
0 in dom f by A7,TARSKI:def 2;
hence t.0 = f.0 by A5,FUNCT_4:def 1
.= 1.L by A6,FUNCT_4:63;
thus thesis by A10;
end;
end;
Lm11: for L being unital non empty doubleLoopStr,
i,n being Nat st i <> 0 & i <> n holds
(0_.(L) +* (0,n)-->(1.L,1.L)).i = 0.L
proof
let L be unital non empty doubleLoopStr; let i,n be Nat;
assume that
A1: i <> 0 and
A2: i <> n;
set t = 0_.(L) +* (0,n)-->(1.L,1.L), f = (0,n)-->(1.L,1.L);
A3: dom(0_.(L)) = NAT by FUNCT_2:def 1;
A4: for u being object holds u in {0,n} implies u in NAT
by ORDINAL1:def 12;
dom f = {0,n} by FUNCT_4:62; then
A5: dom(0_.(L)) \/ dom(f) = NAT by A3,A4,TARSKI:def 3,XBOOLE_1:12;
A6: i in NAT by ORDINAL1:def 12;
not i in dom f by A1,A2,TARSKI:def 2;
hence t.i = (0_.(L)).i by A5,A6,FUNCT_4:def 1
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
definition
let R be unital non empty doubleLoopStr;
let n be Nat;
func npoly(R,n) -> sequence of R equals
0_.(R) +* (0,n) --> (1.R,1.R);
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
set f = (0,n)-->(1.R,1.R);
set q = 0_.(R) +* f;
A2: dom f = {0,n} by FUNCT_4:62;
A5: now let xx be object;
assume xx in NAT;
then reconsider x = xx as Element of NAT;
per cases;
suppose x = 0;
then q.x = 1.R by Lm10;
hence q.xx in the carrier of R;
end;
suppose x = n;
then q.x = 1.R by Lm10;
hence q.xx in the carrier of R;
end;
suppose x <> 0 & x <> n;
then q.x = 0.R by Lm11;
hence q.xx in the carrier of R;
end;
end;
dom(0_.(R)) = NAT by FUNCT_2:def 1;
then dom(0_.(R)) \/ dom(f) = NAT by A2,XBOOLE_1:12;
then dom q = NAT by FUNCT_4:def 1;
hence thesis by A5,FUNCT_2:3;
end;
end;
registration
let R be unital non empty doubleLoopStr;
let n be Nat;
cluster npoly(R,n) -> finite-Support;
coherence
proof
take n+1;
let i be Nat;
assume i >= n + 1;
then i > n by NAT_1:13;
hence thesis by Lm11;
end;
end;
lem6: for R being unital non degenerated doubleLoopStr holds deg npoly(R,n) = n
proof
let R be unital non degenerated doubleLoopStr;
set q = npoly(R,n);
A9: now let i be Nat; assume i >= n+1;
then i <> n & i <> 0 by NAT_1:13;
hence q.i = 0.R by Lm11;
end;
now let m be Nat; assume X: m is_at_least_length_of q;
now assume Y: n+1 > m;
q.n = 1.R by Lm10;
hence contradiction by X,Y,NAT_1:13;
end;
hence n+1 <= m;
end;
then len q = n+1 by A9,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
then deg q = (n+1) - 1 by HURWITZ:def 2;
hence thesis;
end;
registration
let R be unital non degenerated doubleLoopStr,
n be Nat;
cluster npoly(R,n) -> non zero;
coherence
proof
deg npoly(R,n) = n by lem6;
hence thesis by HURWITZ:20;
end;
end;
theorem
for R being unital non degenerated doubleLoopStr holds deg npoly(R,n) = n
by lem6;
theorem
for R being unital non degenerated doubleLoopStr holds LC npoly(R,n) = 1.R
proof
let R be unital non degenerated doubleLoopStr;
set q = npoly(R,n);
A: n = deg q by lem6 .= len q - 1 by HURWITZ:def 2;
then n + 1 = len q;
then len q -' 1 = n by A,XREAL_1:233,NAT_1:11;
hence thesis by Lm10;
end;
theorem lem1e:
for R being non degenerated Ring,
x being Element of R holds eval(npoly(R,0),x) = 1.R
proof
let L be non degenerated Ring, x be Element of L;
set q = npoly(L,0);
consider F be FinSequence of L such that
A3: eval(q,x) = Sum F and
A4: len F = len q and
A5: for n be Element of NAT st n in dom F holds
F.n = q.(n-'1) * (power L).(x,n-'1) by POLYNOM4:def 2;
0 = deg q by lem6 .= len q - 1 by HURWITZ:def 2;
then C: F = <*F.1*> by A4,FINSEQ_1:40;
then Seg 1 = dom F by FINSEQ_1:38;
then F.1 = q.(1-'1) * (power L).(x,1-'1) by A5,FINSEQ_1:3
.= q.0 * (power L).(x,1-'1) by NAT_2:8
.= q.0 * (power L).(x,0) by NAT_2:8
.= 1.L * (power L).(x,0) by Lm10
.= 1.L * 1_L by GROUP_1:def 7
.= 1.L;
hence thesis by A3,C,RLVECT_1:44;
end;
theorem lem1a:
for R being non degenerated Ring,
n being non zero Nat,
x being Element of R holds eval(npoly(R,n),x) = x|^n + 1.R
proof
let R be non degenerated Ring, n be non zero Nat,
x be Element of R;
set q = npoly(R,n);
consider F be FinSequence of R such that
A3: eval(q,x) = Sum F and
A4: len F = len q and
A5: for j be Element of NAT st j in dom F holds
F.j = q.(j-'1) * (power R).(x,j-'1) by POLYNOM4:def 2;
A: n = deg q by lem6 .= len q - 1 by HURWITZ:def 2; then
B: len q = n + 1;
C: dom F = Seg(n+1) by A,A4,FINSEQ_1:def 3;
D: 1 <= n + 1 by NAT_1:11;
E: n+1-'1 = n+1-1 by NAT_1:11,XREAL_1:233;
B1: F.(n+1) = q.n * (power R).(x,n+1-'1) by E,A5,D,C,FINSEQ_1:1
.= 1.R * (power R).(x,(n+1)-'1) by Lm10
.= x |^ n by E;
B2: now let j be Element of NAT;
assume H0: 1 < j & j <= n;
reconsider j1 = j -' 1 as Element of NAT;
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
n <= n + 1 by NAT_1:11;
then H1: j <= n + 1 by H0,XXREAL_0:2;
H4: j1 = j - 1 by H0,XREAL_1:233;
then H2: j1 <> 0 by H0;
j1 + 1 <= n1 + 1 by H4,H0;
then H3: j1 <> n by NAT_1:13;
thus F.j = q.(j1) * (power R).(x,j-'1) by A5,H1,C,H0,FINSEQ_1:1
.= 0.R * (power R).(x,j-'1) by H2,H3,Lm11
.= 0.R;
end;
B3: F.1 = q.(1-'1) * (power R).(x,1-'1) by A5,C,D,FINSEQ_1:1
.= q.0 * (power R).(x,1-'1) by NAT_2:8
.= q.0 * (power R).(x,0) by NAT_2:8
.= 1.R * (power R).(x,0) by Lm10
.= 1.R * 1_R by GROUP_1:def 7
.= 1.R;
B4: len F <> 0 by A,A4;
consider fp being sequence of the carrier of R such that
A6: Sum F = fp.(len F) and
A7: fp.0 = 0.R and
A8: for j being Nat, v being Element of R
st j < len F & v = F.(j + 1)
holds fp.(j + 1) = fp.j + v by RLVECT_1:def 12;
defpred P[Element of NAT] means
($1 = 0 & fp.($1) = 0.R) or
(0 < $1 & $1 < len F & fp.($1) = 1.R) or ($1 = len F & fp.($1) = x|^n + 1.R);
IA: P[0] by A7;
IS: now let j be Element of NAT;
assume C1: 0 <= j & j < len F;
assume C2: P[j];
per cases;
suppose D1: j = 0 & j < len F - 1;
then D2: fp.(j+1) = fp.0 + 1.R by B3,A8,C1 .= 1.R by A7;
j + 1 < (len F - 1) + 1 by D1,XREAL_1:6;
hence P[j+1] by D2;
end;
suppose j = 0 & j >= len F - 1;
hence P[j+1] by A,A4;
end;
suppose D1: 0 < j & j < len F - 1;
then D3: j + 1 <= n by A,A4,INT_1:7;
j + 1 > 0 + 1 by D1,XREAL_1:8;
then F.(j+1) = 0.R by D3,B2;
then fp.(j+1) = 1.R + 0.R by C2,D1,C1,A8;
hence P[j+1] by D3,B,A4,XXREAL_0:2,NAT_1:16;
end;
suppose D1: 0 < j & j >= len F - 1;
j + 1 <= len F by INT_1:7,C1;
then (j + 1) - 1 <= len F - 1 by XREAL_1:9;
then D3: j = n by A4,A,D1,XXREAL_0:1;
then fp.(j+1) = 1.R + x|^n by B1,C1,C2,A8
.= x|^n + 1.R by RLVECT_1:def 2;
hence P[j+1] by D3,A4,A;
end;
end;
I: for j being Element of NAT st 0 <= j & j <= len F holds P[j]
from INT_1:sch 7(IA,IS);
thus eval(q,x) = x|^n + 1.R by I,A6,A3,B4;
end;
theorem lem1:
for n being even Nat,
x being Element of F_Real holds eval(npoly(F_Real,n),x) > 0.F_Real
proof
let n be even Nat, x be Element of F_Real;
per cases;
suppose n = 0;
hence thesis by lem1e;
end;
suppose S: n is non zero;
x|^n + 1 >= 0.F_Real + 1 by XX,XREAL_1:6;
then x|^n + 1.F_Real >= 1;
hence thesis by lem1a,S;
end;
end;
theorem lem1c:
for n being odd Nat
holds eval(npoly(F_Real,n),-1.F_Real) = 0.F_Real
proof
let n be odd Nat;
consider k being Nat such that H: n-1 = 2 * k by ABIAN:def 2;
A: k is Element of NAT by ORDINAL1:def 12;
(-1.F_Real)|^n = (power F_Real).(-1.F_Real,2*k+1) by H
.= -1_F_Real by A,HURWITZ:4
.= -1.F_Real;
hence eval(npoly(F_Real,n),-1.F_Real) = -1.F_Real + 1.F_Real by lem1a
.= 0.F_Real;
end;
theorem lem1b:
eval(npoly(Z/2,2),1.(Z/2)) = 0.(Z/2)
proof
Char(Z/2) = 2 by RING_3:def 6;
then A: 2 '*' 1.(Z/2) = 0.(Z/2) by RING_3:def 5;
thus eval(npoly(Z/2,2),1.(Z/2))
= (1.(Z/2)) |^ 2 + 1.(Z/2) by lem1a
.= 1.(Z/2) * 1.(Z/2) + 1.(Z/2) by prl4
.= 0.(Z/2) by A,prl3;
end;
registration
let n be even Nat;
cluster npoly(F_Real,n) -> non with_roots;
coherence
proof
set q = npoly(F_Real,n);
now assume q is with_roots;
then consider r being Element of F_Real such that
H: r is_a_root_of q by POLYNOM5:def 8;
eval(q,r) = 0.F_Real by H,POLYNOM5:def 7;
hence contradiction by lem1;
end;
hence thesis;
end;
end;
registration
let n be odd Nat;
cluster npoly(F_Real,n) -> with_roots;
coherence
proof
eval(npoly(F_Real,n),-1.F_Real) = 0.F_Real by lem1c;
hence thesis by POLYNOM5:def 8,POLYNOM5:def 7;
end;
end;
registration
cluster npoly(Z/2,2) -> with_roots;
coherence by POLYNOM5:def 7,POLYNOM5:def 8,lem1b;
end;
begin :: the polynomials (x-a1) * (x-a2) * ... * (x-an)
definition
let R be Ring;
mode Ppoly of R -> Polynomial of R means :dpp1:
ex F being non empty FinSequence of Polynom-Ring R
st it = Product F &
for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a);
existence
proof
reconsider p = rpoly(1,1.R) as
Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
set F = <*p*>;
reconsider q = Product F as Polynomial of R by POLYNOM3:def 10;
A: now let i be Nat; assume AS: i in dom F;
dom F = { 1 } by FINSEQ_1:2,FINSEQ_1:38;
then i = 1 by AS,TARSKI:def 1;
hence ex a being Element of R st F.i = rpoly(1,a);
end;
take q,F;
thus thesis by A;
end;
end;
lemppoly:
for R being domRing,
F being non empty FinSequence of Polynom-Ring R,
p being Polynomial of R
st p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a))
holds deg p = len F
proof
let R be domRing, F be non empty FinSequence of Polynom-Ring R,
p be Polynomial of R;
assume AS: p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a));
defpred P[Nat] means
for F being non empty FinSequence of Polynom-Ring R
for p being Polynomial of R st len F = $1 & p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a))
holds deg p = len F;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
per cases;
suppose S: k = 0;
now let F be non empty FinSequence of Polynom-Ring R,
p being Polynomial of R;
assume A: len F = 1 & p = Product F &
(for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a));
then 1 in Seg(len F) by FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then consider a being Element of R such that A0: F.1 = rpoly(1,a) by A;
reconsider q = rpoly(1,a) as Element of Polynom-Ring R
by POLYNOM3:def 10;
F = <*q*> by A0,A,FINSEQ_1:40;
then q = p by A,GROUP_4:9;
hence deg p = 1 by HURWITZ:27;
end;
hence P[k+1] by S;
end;
suppose S: k > 0;
now let F be non empty FinSequence of Polynom-Ring R,
p being Polynomial of R;
assume A: len F = k + 1 & p = Product F &
(for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a));
consider G being FinSequence, y being object such that
B2: F = G^<*y*> by FINSEQ_1:46;
B2a: rng G c= rng F by B2,FINSEQ_1:29;
B2b: rng F c= the carrier of Polynom-Ring R by FINSEQ_1:def 4;
then reconsider G as FinSequence of Polynom-Ring R
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
B3: len F = len G + len<*y*> by B2,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39; then
reconsider G as non empty FinSequence of Polynom-Ring R by S,A;
C: dom G c= dom F by B2,FINSEQ_1:26;
now let i be Nat;
assume C0: i in dom G;
then G.i = F.i by B2,FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by C,C0,A;
end;
then F: deg q = k by IV,B3,A;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng F by B2,FINSEQ_1:30;
then y in rng F by G5;
then reconsider y as Element of Polynom-Ring R by B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: F.(k+1) = <*y*>.1 by B2,B3,A,FINSEQ_1:def 7
.= y;
dom F = Seg(k+1) by A,FINSEQ_1:def 3;
then consider a being Element of R such that
B9: y = rpoly(1,a) by A,B6,FINSEQ_1:4;
B10: p = (Product G) * y by A,B2,GROUP_4:6
.= q *' rpoly(1,a) by B9,POLYNOM3:def 10;
q <> 0_.(R) & rpoly(1,a) <> 0_.(R) by F,HURWITZ:20;
hence deg p = deg q + deg rpoly(1,a) by B10,HURWITZ:23
.= k + 1 by F,HURWITZ:27;
end;
hence P[k+1];
end;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
thus thesis by I,AS;
end;
cc2: for R being domRing, p being Ppoly of R holds LC p = 1.R
proof
let R be domRing, p be Ppoly of R;
defpred P[Nat] means
for q being Polynomial of R
for F being non empty FinSequence of Polynom-Ring R
st len F = $1 & q = Product F & (for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a))
holds LC q = 1.R;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
now let q be Polynomial of R;
let F be non empty FinSequence of Polynom-Ring R;
assume AS: len F = k+1 & q = Product F & (for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a));
then consider G being FinSequence of Polynom-Ring R,
x being Element of Polynom-Ring R such that
A1: F = G ^ <*x*> by FINSEQ_2:19;
reconsider p = Product G as Polynomial of R by POLYNOM3:def 10;
A4: len F = len G + 1 by A1,FINSEQ_2:16;
A5: x = F.(len F) by A1,A4,FINSEQ_1:42;
len F in Seg(len F) by FINSEQ_1:3;
then len F in dom F by FINSEQ_1:def 3;
then consider a being Element of R such that
A2: x = rpoly(1,a) by AS,A5;
per cases;
suppose G = {};
then F = <*x*> by A1,FINSEQ_1:34;
then Product F = rpoly(1,a) by A2,GROUP_4:9;
hence LC q = 1.R by AS,lcrpol;
end;
suppose B1: G is non empty;
B2: now let i be Nat;
assume C1: i in dom G;
C2: dom G c= dom F by A1,FINSEQ_1:26;
G.i = F.i by A1,C1,FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by C1,C2,AS;
end;
deg p = len G by B1,B2,lemppoly;
then p <> 0_.(R) by HURWITZ:20;
then reconsider p as non zero Polynomial of R by UPROOTS:def 5;
Product F = Product G * Product<*x*> by A1,GROUP_4:5
.= Product G * x by GROUP_4:9
.= p *' rpoly(1,a) by A2,POLYNOM3:def 10;
hence LC q = LC p * LC rpoly(1,a) by AS,NIVEN:46
.= LC p * 1.R by lcrpol
.= 1.R by AS,A4,B1,B2,IV;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider F being non empty FinSequence of Polynom-Ring R such that
H: p = Product F &
for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a)
by dpp1;
consider k being Nat such that J: len F = k;
thus thesis by H,I,J;
end;
registration
let R be domRing;
cluster -> non constant monic with_roots for Ppoly of R;
coherence
proof
let p be Ppoly of R;
consider F being non empty FinSequence of Polynom-Ring R such that
H: p = Product F &
for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a)
by dpp1;
A0: len F >= 1 + 0 by NAT_1:13;
hence p is non constant by H,lemppoly;
thus p is monic by cc2;
consider G being FinSequence of Polynom-Ring R,
x being Element of Polynom-Ring R such that
A1: F = G ^ <*x*> by A0,FINSEQ_2:19;
A3: F.(len G + 1) = x by A1,FINSEQ_1:42;
A4: len F = len G + len<*x*> by A1,FINSEQ_1:22 .= len G + 1 by FINSEQ_1:40;
len F in Seg(len F) by FINSEQ_1:3;
then len F in dom F by FINSEQ_1:def 3;
then consider a being Element of R such that A2: x = rpoly(1,a) by H,A3,A4;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
p = (Product G) * x by H,A1,GROUP_4:6 .= q *' rpoly(1,a) by A2,POLYNOM3:def 10;
hence p is with_roots;
end;
end;
theorem
for R being domRing, p being Ppoly of R holds LC p = 1.R by cc2;
theorem lemppoly1:
for R being domRing, a being Element of R holds rpoly(1,a) is Ppoly of R
proof
let R being domRing, a be Element of R;
reconsider p = rpoly(1,a) as
Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
set F = <*p*>;
A: now let i be Nat; assume AS: i in dom F;
dom F = { 1 } by FINSEQ_1:2,FINSEQ_1:38;
then i = 1 by AS,TARSKI:def 1;
hence ex a being Element of R st F.i = rpoly(1,a);
end;
Product F = p by GROUP_4:9;
hence thesis by A,dpp1;
end;
theorem lemppoly3:
for R being domRing,
p,q being Ppoly of R holds p *' q is Ppoly of R
proof
let R be domRing, p,q be Ppoly of R;
consider Fp being non empty FinSequence of Polynom-Ring R such that
B0: p = Product Fp & for i being Nat st i in dom Fp
ex a being Element of R st Fp.i = rpoly(1,a) by dpp1;
consider Fq being non empty FinSequence of Polynom-Ring R such that
B1: q = Product Fq & for i being Nat st i in dom Fq
ex a being Element of R st Fq.i = rpoly(1,a) by dpp1;
set G = Fp ^ Fq;
A: now let i be Nat;
assume AS: i in dom G;
per cases by AS,FINSEQ_1:25;
suppose B2: i in dom Fp;
then Fp.i = G.i by FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by B0,B2;
end;
suppose ex n being Nat st n in dom Fq & i =len Fp + n;
then consider n being Nat such that
B2: n in dom Fq & i = len Fp + n;
G.i = Fq.n by B2,FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by B1,B2;
end;
end;
Product G = (Product Fp) * (Product Fq) by GROUP_4:5
.= p *' q by B0,B1,POLYNOM3:def 10;
hence thesis by A,dpp1;
end;
lempolybag1:
for R being domRing,
a being Element of R
for F being non empty FinSequence of Polynom-Ring R
st (for k being Nat st k in dom F holds F.k = rpoly(1,a))
for p being Polynomial of R st p = Product F
holds p = rpoly(1,a) `^ (len F) & Roots p = {a}
proof
let R be domRing, a be Element of R,
F be non empty FinSequence of Polynom-Ring R;
assume AS1: for k being Nat st k in dom F holds F.k = rpoly(1,a);
let p be Polynomial of R;
assume AS2: p = Product F;
defpred P[Nat] means
for F being FinSequence of Polynom-Ring R
st len F = $1 & for k being Nat st k in dom F holds F.k = rpoly(1,a)
for p being Polynomial of R st p = Product F
holds p = rpoly(1,a) `^ (len F) & Roots p = {a};
IA: P[1]
proof
now let F be FinSequence of Polynom-Ring R;
assume AS1: len F = 1 &
for k being Nat st k in dom F holds F.k = rpoly(1,a);
let p be Polynomial of R;
assume AS2: p = Product F;
B: F = <*F.1*> by AS1,FINSEQ_1:40;
then A: dom F = Seg 1 by FINSEQ_1:38;
then C: F.1 in rng F by FUNCT_1:3,FINSEQ_1:3;
rng F c= the carrier of Polynom-Ring R by FINSEQ_1:def 4; then
reconsider x = F.1 as Element of the carrier of Polynom-Ring R by C;
thus p = x by AS2,B,GROUP_4:9
.= rpoly(1,a) by A,AS1,FINSEQ_1:3
.= rpoly(1,a) `^ (len F) by AS1,POLYNOM5:16;
then p = rpoly(1,a) by AS1,POLYNOM5:16;
hence Roots p = {a} by ro4;
end;
hence thesis;
end;
IS: now let k be Nat;
assume 1 <= k;
assume IV: P[k];
now let F be FinSequence of Polynom-Ring R;
assume AS1: len F = k+1 &
for i being Nat st i in dom F holds F.i = rpoly(1,a);
let p be Polynomial of R;
assume AS2: p = Product F;
consider G being FinSequence of Polynom-Ring R,
x being Element of Polynom-Ring R such that
A1: F = G ^ <*x*> by AS1,FINSEQ_2:19;
A3: F.(len G + 1) = x by A1,FINSEQ_1:42;
A4: len F = len G + len<*x*> by A1,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:40;
len F in Seg(len F) by AS1,FINSEQ_1:3;
then len F in dom F by FINSEQ_1:def 3;
then A2: x = rpoly(1,a) by AS1,A3,A4;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
now let i be Nat;
assume A6: i in dom G;
A7: dom G c= dom F by A1,FINSEQ_1:26;
thus G.i = F.i by A1,A6,FINSEQ_1:def 7 .= rpoly(1,a) by AS1,A7,A6;
end;
then A6: q = rpoly(1,a) `^ (len G) & Roots q = {a} by AS1,A4,IV;
A7: p = (Product G) * x by AS2,A1,GROUP_4:6
.= q *' rpoly(1,a) by A2,POLYNOM3:def 10;
hence p = rpoly(1,a) `^ (len F) by A4,A6,POLYNOM5:19;
thus Roots p = Roots(q) \/ Roots rpoly(1,a) by A7,UPROOTS:23
.= {a} \/ {a} by A6,ro4
.= {a};
end;
hence P[k+1];
end;
I: for k being Nat st k >= 1 holds P[k] from NAT_1:sch 8(IA,IS);
len F >= 1 by FINSEQ_1:20;
hence thesis by I,AS1,AS2;
end;
lempolybag:
for R being domRing,
B be bag of (the carrier of R) st card(support B) = 1
ex p being Ppoly of R
st deg p = card B &
for a being Element of R holds multiplicity(p,a) = B.a
proof
let R be domRing, B be bag of (the carrier of R);
assume card(support B) = 1;
then consider x being object such that A1: support B = {x} by CARD_2:42;
x in support B by A1,TARSKI:def 1;
then reconsider a = x as Element of the carrier of R;
reconsider q = rpoly(1,a) as Element of Polynom-Ring R by POLYNOM3:def 10;
deffunc f(set) = q;
consider F being FinSequence of Polynom-Ring R such that
A2: len F = B.a & for k being Nat st k in dom F holds F.k = f(k)
from FINSEQ_2: sch 1;
reconsider F as non empty FinSequence of Polynom-Ring R by A1,A2,bb7;
reconsider p = Product F as Polynomial of R by POLYNOM3:def 10;
AS: B = ({a},B.a)-bag by A1,bb7;
A3: for i be Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a) by A2;
then reconsider p as Ppoly of R by dpp1;
take p;
thus deg p = B.a by A2,A3,lemppoly .= card B by AS,bb4;
A5: rpoly(1,a)`^(B.a) = p by lempolybag1,A2;
now let o be Element of R;
per cases;
suppose C: o = a;
rpoly(1,a)`^(B.a) = (rpoly(1,a)`^(B.a)) *' 1_.(R);
then B: rpoly(1,a)`^(B.a) divides p by A5,RING_4:1;
E: rpoly(1,a)`^(B.a) <> 0_.(R);
rpoly(1,a)`^((B.a)+1) = (rpoly(1,a)`^(B.a)) *' rpoly(1,a) by POLYNOM5:19;
then deg(rpoly(1,a)`^((B.a)+1))
= deg(rpoly(1,a)`^(B.a)) + deg rpoly(1,a) by E,HURWITZ:23
.= deg(rpoly(1,a)`^(B.a)) + 1 by HURWITZ:27;
then deg(rpoly(1,a)`^((B.a)+1)) > deg(rpoly(1,a)`^(B.a)) by XREAL_1:29;
hence multiplicity(p,o) = B.o by C,B,A5,prl25,multip;
end;
suppose C: o <> a;
then C1: not o in support B by A1,TARSKI:def 1;
rpoly(1,o)`^0 = 1_.(R) by POLYNOM5:15;
then B: (rpoly(1,o)`^0) *' p = p;
now assume rpoly(1,o)`^(0+1) divides p;
then rpoly(1,o) divides p by POLYNOM5:16;
then eval(p,o) = 0.R by Th9;
then o is_a_root_of p by POLYNOM5:def 7;
then o in Roots p by POLYNOM5:def 10;
then o in {a} by lempolybag1,A2;
hence contradiction by C,TARSKI:def 1;
end;
hence multiplicity(p,o) = 0 by B,multip,RING_4:1
.= B.o by C1,PRE_POLY:def 7;
end;
end;
hence thesis;
end;
definition
let R be domRing;
let B be non zero bag of the carrier of R;
mode Ppoly of R,B -> Ppoly of R means :dpp:
deg it = card B &
for a being Element of R holds multiplicity(it,a) = B.a;
existence
proof
defpred P[Nat] means
for B being non zero bag of the carrier of R
st card(support B) = $1
ex p being Ppoly of R st deg p = card B &
for a being Element of R holds multiplicity(p,a) = B.a;
IA: P[1] by lempolybag;
IS: now let k be Nat;
assume AS: 1 <= k;
assume IV: P[k];
now let B be non zero bag of the carrier of R;
assume X: card(support B) = k + 1;
now assume A: not ex x being Element of R st x in support B;
let o be Element of support B;
now assume support B <> {};
then o in support B;
hence contradiction by A;
end;
hence contradiction by X;
end;
then consider x being Element of R such that A: x in support B;
H1: for o be object holds o in {x} implies o in support B
by A,TARSKI:def 1;
set b = ({x},B.x)-bag, b1 = B \ x;
B.x <> 0 by A,PRE_POLY:def 7;
then support b = {x} by UPROOTS:8;
then card support b = 1 by CARD_1:30;
then consider p1 being Ppoly of R such that
A1: deg p1 = card b &
for a being Element of R holds multiplicity(p1,a) = b.a
by lempolybag;
A3: card support b1 = card(support B \ {x}) by bb3a
.= card support B - card {x} by TARSKI:def 3,H1,CARD_2:44
.= (card support B) - 1 by CARD_1:30;
then support b1 <> {} by X,AS;
then reconsider b1 as non zero bag of the carrier of R
by bbag;
consider p2 being Ppoly of R such that
A5: deg p2 = card b1 &
for a being Element of R holds multiplicity(p2,a) = b1.a
by A3,X,IV;
reconsider q = p1 *' p2 as Ppoly of R by lemppoly3;
p1 <> 0_.(R) & p2 <> 0_.(R); then
A2: deg q = deg p1 + deg p2 by HURWITZ:23
.= card(b + b1) by A1,A5,UPROOTS:15
.= card B by bb3;
now let a be Element of R;
thus multiplicity(q,a)
= multiplicity(p1,a) + multiplicity(p2,a) by UPROOTS:55
.= b.a + multiplicity(p2,a) by A1
.= b.a + b1.a by A5
.= (b+b1).a by PRE_POLY:def 5
.= B.a by bb3;
end;
hence ex p being Ppoly of R st deg p = card B &
for a being Element of R holds multiplicity(p,a) = B.a by A2;
end;
hence P[k+1];
end;
I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(IA,IS);
consider n being Nat such that H: card support B = n;
now assume n = 0;
then support B = {} by H;
hence contradiction by bbag;
end;
then n + 1 > 0 + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
hence thesis by H,I;
end;
end;
theorem
for R being domRing,
B being non zero bag of the carrier of R,
p being Ppoly of R,B
for a being Element of R st a in support B holds eval(p,a) = 0.R
proof
let R be domRing, F be non zero bag of the carrier of R,
p be Ppoly of R,F; let a being Element of R;
assume a in support F;
then F.a <> 0 by PRE_POLY:def 7;
then F.a + 1 > 0 + 1 by XREAL_1:6;
then F.a >= 1 by NAT_1:13;
then multiplicity(p,a) >= 1 by dpp;
then consider s being Polynomial of R such that
A: p = rpoly(1,a) *' s by HURWITZ:33,UPROOTS:52;
thus thesis by A,RING_4:1,Th9;
end;
theorem pf1:
for R being domRing,
B being non zero bag of the carrier of R,
p being Ppoly of R,B
for a being Element of R
holds rpoly(1,a) `^ (B.a) divides p & not rpoly(1,a) `^ (B.a + 1) divides p
proof
let R be domRing, F be non zero bag of the carrier of R,
p be Ppoly of R,F; let a being Element of R;
multiplicity(p,a) = F.a by dpp;
hence thesis by multip;
end;
theorem pf2:
for R being domRing,
B being non zero bag of the carrier of R,
p being Ppoly of R,B holds BRoots(p) = B
proof
let R be domRing, B be non zero bag of the carrier of R,
p be Ppoly of R,B;
set b = BRoots p;
now let o be object;
assume o in the carrier of R;
then reconsider a = o as Element of the carrier of R;
B.a = multiplicity(p,a) by dpp .= b.a by UPROOTS:def 9;
hence b.o = B.o;
end;
hence thesis by PBOOLE:3;
end;
theorem lemacf5:
for R being domRing,
B being non zero bag of the carrier of R
for p being Ppoly of R,B holds deg p = card BRoots p
proof
let R be domRing, B be non zero bag of the carrier of R;
let p be Ppoly of R,B;
thus card(BRoots p) = card B by pf2 .= deg p by dpp;
end;
theorem lemacf:
for R being domRing,
a being Element of R holds rpoly(1,a) is Ppoly of R,Bag{a}
proof
let R be domRing, a be Element of R;
reconsider p = rpoly(1,a) as Ppoly of R by lemppoly1;
A: deg p = 1 by HURWITZ:27 .= card {a} by CARD_1:30
.= card ({a},1)-bag by UPROOTS:13;
now let c be Element of R;
per cases;
suppose B: c = a;
then C: c in {a} by TARSKI:def 1;
thus multiplicity(p,c) = 1 by B,BR5aa .= (Bag{a}).c by C,UPROOTS:7;
end;
suppose B: c <> a;
then C: not c in {a} by TARSKI:def 1;
thus multiplicity(p,c) = 0 by B,BR5aaa .= (Bag{a}).c by C,UPROOTS:6;
end;
end;
hence thesis by A,dpp;
end;
theorem lemacf2:
for R being domRing,
B1,B2 being non zero bag of the carrier of R
for p being (Ppoly of R,B1),
q being Ppoly of R,B2 holds p *' q is Ppoly of R,(B1+B2)
proof
let R be domRing, B1,B2 be non zero bag of the carrier of R;
set B = B1 + B2;
let p be (Ppoly of R,B1), q be Ppoly of R,B2;
reconsider r = p *' q as Ppoly of R by lemppoly3;
p <> 0_.(R) & q <> 0_.(R); then
A: deg r = deg p + deg q by HURWITZ:23
.= card BRoots p + deg q by lemacf5
.= card B1 + deg q by pf2
.= card B1 + card BRoots q by lemacf5
.= card B1 + card B2 by pf2
.= card B by UPROOTS:15;
now let c be Element of R;
thus multiplicity(r,c)
= multiplicity(p,c) + multiplicity(q,c) by UPROOTS:55
.= (BRoots p).c + multiplicity(q,c) by UPROOTS:def 9
.= B1.c + multiplicity(q,c) by pf2
.= B1.c + (BRoots q).c by UPROOTS:def 9
.= B1.c + B2.c by pf2
.= B.c by PRE_POLY:def 5;
end;
hence thesis by A,dpp;
end;
theorem lll:
for R being domRing, p being Ppoly of R holds p is Ppoly of R,(BRoots p)
proof
let R be domRing, p be Ppoly of R;
defpred P[Nat] means
for p being Ppoly of R st deg p = $1 holds p is Ppoly of R,(BRoots p);
IA: P[1]
proof
now let p be Ppoly of R;
assume A0: deg p = 1;
consider F being non empty FinSequence of Polynom-Ring R such that
A1: p = Product F &
for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a) by dpp1;
len F = 1 by A0,A1,lemppoly;
then A2: F = <*F.1*> by FINSEQ_1:40;
then A3: dom F = Seg 1 by FINSEQ_1:38;
then consider a being Element of R such that
A4: F.1 = rpoly(1,a) by A1,FINSEQ_1:1;
reconsider e = 1 as Element of dom F by A3,FINSEQ_1:1;
A5: Product F = F.e by A2,GROUP_4:9;
rpoly(1,a) = <%-a, 1.R%> by repr;
then BRoots rpoly(1,a) = Bag{a} by UPROOTS:54;
hence p is Ppoly of R,(BRoots p) by A1,A4,A5,lemacf;
end;
hence thesis;
end;
IS: now let k be Nat;
assume AS: k >= 1;
assume IV: P[k];
now let p be Ppoly of R;
assume B0: deg p = k+1;
consider F being non empty FinSequence of Polynom-Ring R such that
B1: p = Product F &
for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a) by dpp1;
B1a: len F = k+1 by B0,B1,lemppoly;
consider G being FinSequence, y being object such that
B2: F = G^<*y*> by FINSEQ_1:46;
B2a: rng G c= rng F by B2,FINSEQ_1:29;
B2b: rng F c= the carrier of Polynom-Ring R by FINSEQ_1:def 4;
then reconsider G as FinSequence of Polynom-Ring R
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
B3: len F = len G + len<*y*> by B2,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39; then
reconsider G as non empty FinSequence of Polynom-Ring R by B1a,AS;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
C: dom G c= dom F by B2,FINSEQ_1:26;
D: now let i be Nat;
assume C0: i in dom G;
then G.i = F.i by B2,FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by C,C0,B1;
end;
then reconsider q as Ppoly of R by dpp1;
set B = BRoots q;
deg q = k by B1a,B3,D,lemppoly;
then reconsider q as Ppoly of R,B by IV;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng F by B2,FINSEQ_1:30;
then y in rng F by G5;
then reconsider y as Element of Polynom-Ring R by B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: F.(k+1) = <*y*>.1 by B2,B3,B1a,FINSEQ_1:def 7
.= y;
dom F = Seg(k+1) by B1a,FINSEQ_1:def 3;
then consider a being Element of R such that
B9: y = rpoly(1,a) by B1,B6,FINSEQ_1:4;
reconsider r = y as Ppoly of R,Bag{a} by lemacf,B9;
B10: p = (Product G) * y by B1,B2,GROUP_4:6
.= q *' r by POLYNOM3:def 10;
reconsider B1 = B + Bag{a} as non zero bag of the carrier of R;
rpoly(1,a) = <%-a, 1.R%> by repr;
then BRoots rpoly(1,a) = Bag{a} by UPROOTS:54;
then BRoots p = B + Bag{a} by B9,B10,UPROOTS:56;
hence p is Ppoly of R,(BRoots p) by B10,lemacf2;
end;
hence P[k+1];
end;
I: for k being Nat st k >= 1 holds P[k] from NAT_1:sch 8(IA,IS);
reconsider n = deg p as Element of NAT by INT_1:3;
n + 1 > 0 + 1 by RATFUNC1:def 2,XREAL_1:6;
then n >= 1 by NAT_1:13;
hence thesis by I;
end;
definition
let R be domRing;
let S be non empty finite Subset of R;
mode Ppoly of R,S is Ppoly of R,Bag S;
end;
theorem m00:
for R being domRing,
S being non empty finite Subset of R
for p being Ppoly of R,S holds deg p = card S
proof
let R be domRing, S be non empty finite Subset of R;
let p being Ppoly of R,S;
thus deg p = card (Bag S) by dpp .= card S by UPROOTS:13;
end;
theorem m0:
for R being domRing,
S being non empty finite Subset of R
for p being Ppoly of R,S
for a being Element of R st a in S
holds rpoly(1,a) divides p & not rpoly(1,a)`^2 divides p
proof
let R be domRing, S be non empty finite Subset of R;
let p being Ppoly of R,S; let a being Element of R;
assume a in S;
then A: (Bag S).a = 1 by UPROOTS:7;
X: rpoly(1,a) `^ ((Bag S).a) divides p &
not rpoly(1,a) `^ ((Bag S).a + 1) divides p by pf1;
hence rpoly(1,a) divides p by A,POLYNOM5:16;
thus thesis by A,X;
end;
theorem m1:
for R being domRing,
S being non empty finite Subset of R,
p being Ppoly of R,S
for a being Element of R st a in S holds eval(p,a) = 0.R
proof
let R be domRing, S be non empty finite Subset of R,
p be Ppoly of R,S; let a be Element of R;
assume a in S;
then consider q being Polynomial of R such that
H: rpoly(1,a) *' q = p by m0,RING_4:1;
a is_a_root_of p by H,prl2,HURWITZ:30;
hence eval(p,a) = 0.R by POLYNOM5:def 7;
end;
theorem
for R being domRing,
S being non empty finite Subset of R,
p being Ppoly of R,S
holds Roots(p) = S
proof
let R be domRing, S be non empty finite Subset of R,
p be Ppoly of R,S;
A0: now let o be object;
assume AS: o in S;
then reconsider x = o as Element of R;
eval(p,x) = 0.R by AS,m1;
then x is_a_root_of p by POLYNOM5:def 7;
hence o in Roots(p) by POLYNOM5:def 10;
end;
then card(Roots(p) \ S) = card Roots(p) - card S by TARSKI:def 3,CARD_2:44;
then B: (card Roots(p) - card S) + card S >= 0 + card S by XREAL_1:6;
card Roots(p) <= deg p by degpoly;
then card Roots(p) <= card S by m00;
then card S = card Roots(p) by B,XXREAL_0:1;
hence thesis by A0,CARD_2:102,TARSKI:def 3;
end;
begin :: Main Theorems
theorem acf:
for R being domRing,
p being non zero with_roots Polynomial of R
ex q being (Ppoly of R,BRoots p),
r being non with_roots Polynomial of R st p = q *' r & Roots q = Roots p
proof
let R be domRing, p be non zero with_roots Polynomial of R;
defpred P[Nat] means
for p being non zero with_roots Polynomial of R
st deg p = $1 ex q being (Ppoly of R,BRoots p),
r being non with_roots Polynomial of R
st p = q *' r & Roots q = Roots p;
IA: P[1]
proof
let p be non zero with_roots Polynomial of R;
assume AS: deg p = 1;
consider a being Element of R such that
A1: a is_a_root_of p by POLYNOM5:def 8;
eval(p,a) = 0.R by A1,POLYNOM5:def 7;
then consider p1 being Polynomial of R such that
A2: p = rpoly(1,a) *' p1 by Th9,RING_4:1;
reconsider q = rpoly(1,a) as Ppoly of R by lemppoly1;
reconsider B = BRoots p as non zero bag of the carrier of R;
p1 <> 0_.(R) & rpoly(1,a) <> 0_.(R) by A2;
then deg p = deg rpoly(1,a) + deg p1 by A2,HURWITZ:23
.= 1 + deg p1 by HURWITZ:27;
then reconsider p1 as non with_roots Polynomial of R
by AS,HURWITZ:24;
reconsider p1 as non zero non with_roots Polynomial of R;
A7: rpoly(1,a) = <%-a, 1.R%> by repr;
BRoots p = BRoots rpoly(1,a) + BRoots p1 by A2,UPROOTS:56
.= ({a}, 1)-bag + BRoots p1 by A7,UPROOTS:54
.= ({a}, 1)-bag + EmptyBag(the carrier of R) by lemacf1
.= Bag{a} by PRE_POLY:53;
then reconsider q = rpoly(1,a) as Ppoly of R,BRoots p by lemacf;
take q,p1;
thus q *' p1 = p by A2;
thus Roots p = Roots q \/ Roots p1 by A2,UPROOTS:23 .= Roots q;
end;
IS: now let k be Nat;
assume 1 <= k;
assume IV: P[k];
now let p be non zero with_roots Polynomial of R;
assume AS1: deg p = k+1;
consider a being Element of R such that
A1: a is_a_root_of p by POLYNOM5:def 8;
consider s being Polynomial of R such that
A2: p = rpoly(1,a) *' s by A1,HURWITZ:33;
reconsider s as non zero Polynomial of R by A2;
per cases;
suppose A4: s is non with_roots;
then A5: Roots s = {};
reconsider q = rpoly(1,a) as Ppoly of R,Bag{a} by lemacf;
A7: rpoly(1,a) = <%-a, 1.R%> by repr;
A6: BRoots p = BRoots rpoly(1,a) + BRoots s by A2,UPROOTS:56
.= BRoots rpoly(1,a) + EmptyBag(the carrier of R) by A4,lemacf1
.= BRoots rpoly(1,a) by PRE_POLY:53
.= Bag{a} by A7,UPROOTS:54;
Roots p = Roots q \/ Roots s by A2,UPROOTS:23 .= Roots q by A5;
hence ex q being (Ppoly of R,BRoots p),
r being non with_roots Polynomial of R
st p = q *' r & Roots q = Roots p by A2,A4,A6;
end;
suppose s is with_roots;
then reconsider s as non zero with_roots Polynomial of R;
s <> 0_.(R) & rpoly(1,a) <> 0_.(R); then
deg p = (deg rpoly(1,a)) + (deg s) by A2,HURWITZ:23
.= 1 + (deg s) by HURWITZ:27;
then consider qs being (Ppoly of R,BRoots s),
rs being non with_roots Polynomial of R such that
B1: s = qs *' rs & Roots qs = Roots s by AS1,IV;
reconsider rs as non zero non with_roots Polynomial of R;
set q = rpoly(1,a) *' qs;
B2: p = q *' rs by A2,B1,POLYNOM3:33;
reconsider B = Bag{a} + BRoots s
as non zero bag of the carrier of R;
rpoly(1,a) is Ppoly of R,Bag{a} by lemacf;
then reconsider q as Ppoly of R,B by lemacf2;
B7: rpoly(1,a) = <%-a, 1.R%> by repr;
B4: BRoots p = BRoots q + BRoots rs by B2,UPROOTS:56
.= BRoots q + EmptyBag(the carrier of R) by lemacf1
.= BRoots q by PRE_POLY:53
.= BRoots(rpoly(1,a)) + BRoots qs by UPROOTS:56
.= Bag{a} + BRoots qs by B7,UPROOTS:54
.= B by pf2;
B3: Roots p = Roots q \/ Roots rs by B2,UPROOTS:23
.= Roots q;
thus ex q being (Ppoly of R,BRoots p),
r being non with_roots Polynomial of R
st p = q *' r & Roots q = Roots p by B2,B3,B4;
end;
end;
hence P[k+1];
end;
I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(IA,IS);
K: deg p >= 0 + 1 by INT_1:7,RATFUNC1:def 2;
p <> 0_.(R);
then deg p is Element of NAT by T8;
then consider d being Nat such that H: deg p = d;
thus thesis by K,H,I;
end;
theorem
for R being domRing,
p being non zero Polynomial of R holds card(Roots p) <= card(BRoots p)
proof
let R be domRing, p be non zero Polynomial of R;
per cases;
suppose p is with_roots;
then reconsider p1 = p as non zero with_roots Polynomial of R;
consider q being (Ppoly of R,BRoots p1),
r being non with_roots Polynomial of R such that
A: p1 = q *' r & Roots q = Roots p1 by acf;
deg q = card(BRoots q) by lemacf5 .= card(BRoots p1) by pf2;
hence thesis by A,degpoly;
end;
suppose A: p is non with_roots;
then card(Roots p) = 0 .= card(EmptyBag(the carrier of R)) by UPROOTS:11
.= card(BRoots p) by A,lemacf1;
hence thesis;
end;
end;
theorem
for R being domRing,
p being non constant Polynomial of R
holds card(BRoots p) = deg p iff
ex a being Element of R, q being Ppoly of R st p = a * q
proof
let R be domRing, p be non constant Polynomial of R;
per cases;
suppose p is with_roots;
then reconsider p1 = p as non zero with_roots Polynomial of R;
consider q being (Ppoly of R,BRoots p1),
r being non with_roots Polynomial of R such that
H: p1 = q *' r & Roots q = Roots p1 by acf;
reconsider r1 = r as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
A: now assume A1: card(BRoots p) = deg p;
r <> 0_.(R) & q <> 0_.(R); then
deg p = deg q + deg r by H,HURWITZ:23
.= card(BRoots q) + deg r by lemacf5
.= deg p + deg r by A1,pf2;
then r1 is constant;
then consider a being Element of R such that B: r1 = a|R by RING_4:20;
p = q *' (a * 1_.(R)) by H,B,RING_4:16
.= a * (q *' 1_.(R)) by RATFUNC1:6
.= a * q;
hence ex a being Element of R, q being Ppoly of R st p = a * q;
end;
now assume ex a being Element of R, q being Ppoly of R st p = a * q;
then consider a being Element of R, q being Ppoly of R such that
A1: p = a * q;
set B = BRoots q;
reconsider q as Ppoly of R,B by lll;
p <> 0_.(R); then A3: a is non zero by A1,POLYNOM5:26;
hence deg p = deg q by A1,Th25
.= card B by lemacf5 .= card(BRoots p) by A1,A3,llll;
end;
hence thesis by A;
end;
suppose A: p is non with_roots;
then reconsider p1 = p as non zero non with_roots Polynomial of R;
card(BRoots p) = card(EmptyBag(the carrier of R)) by A,lemacf1
.= 0 by UPROOTS:11;
hence thesis by A,RATFUNC1:def 2;
end;
end;
theorem
for R being domRing,
p,q being Polynomial of R
st (ex S being Subset of R
st card S = max(deg p,deg q) + 1 &
for a being Element of R st a in S holds eval(p,a) = eval(q,a))
holds p = q
proof
let R be domRing, p,q be Polynomial of R;
assume ex S being Subset of R
st card S = max(deg p,deg q) + 1 &
for a being Element of R st a in S holds eval(p,a) = eval(q,a);
then consider S being Subset of R such that
A0: card S = max(deg p,deg q) + 1 &
for a being Element of R st a in S holds eval(p,a) = eval(q,a);
now assume HH: p <> q;
max(deg p,deg q) + 1 is Element of NAT
proof
D: max(deg p,deg q) >= deg p by XXREAL_0:25;
deg p >= - 1
proof
per cases;
suppose p = 0_.(R); hence thesis by HURWITZ:20; end;
suppose p <> 0_.(R); hence thesis by T8; end;
end;
then max(deg p,deg q) >= -1 by D,XXREAL_0:2;
then max(deg p,deg q) + 1 >= -1 + 1 by XREAL_1:6;
hence thesis by INT_1:3;
end;
then reconsider S as finite Subset of the carrier of R by A0;
per cases;
suppose AS: p is zero;
then q is non zero by HH; then
reconsider q as non zero Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
reconsider n = deg q as Element of NAT by AS,T8;
deg p = -1 by AS,HURWITZ:20; then
C0: max(deg p,deg q) + 1 = n + 1 by XXREAL_0:def 10;
now let x be object;
assume C: x in S;
then reconsider a = x as Element of R;
eval(q,a) = eval(p,a) by A0,C .= 0.R by AS,POLYNOM4:17;
then a is_a_root_of q by POLYNOM5:def 7;
hence x in Roots q by POLYNOM5:def 10;
end;
then C2: n + 1 <= card(Roots q) by A0,C0,NAT_1:43,TARSKI:def 3;
card(Roots q) <= deg q by degpoly;
then C4: n + 1 <= n by C2,XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4,XXREAL_0:1;
hence contradiction;
end;
suppose p is non zero;
then reconsider n = deg p as Element of NAT by T8;
H2: n = len p - 1 by HURWITZ:def 2;
then H2a: len p = n + 1;
per cases by XXREAL_0:1;
suppose D: len q < len p;
then len q + 1 <= len p by INT_1:7;
then len q + 1 - 1 <= len p - 1 by XREAL_1:9;
then q.n = 0.R by H2,ALGSEQ_1:8;
then H3: q.n <> p.n by H2a,ALGSEQ_1:10;
deg q = len q - 1 & deg p = len p - 1 by HURWITZ:def 2; then
H4: max(deg p,deg q) = n by D,XREAL_1:9,XXREAL_0:def 10;
defpred P[Nat] means p.($1) <> q.($1);
A2: for k being Nat st P[k] holds k <= n
proof
let k be Nat; assume B0: P[k];
now let i be Nat; assume i > n;
then B1: i >= len p by H2a,NAT_1:13;
hence p.i = 0.R by ALGSEQ_1:8
.= q.i by B1,D,XXREAL_0:2,ALGSEQ_1:8;
end;
hence thesis by B0;
end;
A3: ex k being Nat st P[k] by H3;
consider m being Nat such that
A4: P[m] & for i being Nat st P[i] holds i <= m from NAT_1:sch 6(A2,A3);
A5: p.m <> q.m & m <= n by A2,A4;
A6: now assume A7: (p - q).m = 0.R;
p.m + 0.R = p.m + (-q.m + q.m) by RLVECT_1:5
.= (p.m + -q.m) + q.m by RLVECT_1:def 3
.= (p.m - q.m) + q.m by RLVECT_1:def 11
.= 0.R + q.m by A7,NORMSP_1:def 3;
hence contradiction by A4;
end;
then p - q <> 0_.(R) by FUNCOP_1:7,ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;
now let x be object;
assume C2: x in S;
then reconsider a = x as Element of R;
eval(r,a) = eval(p,a) - eval(q,a) by POLYNOM4:21
.= eval(p,a) - eval(p,a) by C2,A0
.= 0.R by RLVECT_1:15;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10;
end;
then C2: n + 1 <= card Roots r by A0,H4,NAT_1:43,TARSKI:def 3;
len r = m + 1
proof
E1: now let i be Nat;
assume i >= m+1;
then not(i <= m) by NAT_1:13;
then X: p.i = q.i by A4;
thus r.i = p.i - q.i by NORMSP_1:def 3 .= 0.R by X,RLVECT_1:15;
end;
for k be Nat st k is_at_least_length_of r holds m+1 <= k by A6,NAT_1:13;
hence thesis by E1,ALGSEQ_1:def 2,ALGSEQ_1:def 3;
end;
then len r - 1 = m;
then C3: deg r = m by HURWITZ:def 2;
card(Roots r) <= deg r by degpoly;
then n + 1 <= m by C2,C3,XXREAL_0:2;
then C4: n + 1 <= n by A5,XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4,XXREAL_0:1;
hence contradiction;
end;
suppose D: len p < len q;
then len p + 1 <= len q by INT_1:7;
then D1: len p + 1 - 1 <= len q - 1 by XREAL_1:9;
len p - 1 < len q - 1 by D,XREAL_1:9;
then deg p < len q - 1 by HURWITZ:def 2;
then deg p < deg q & 0 <= n by HURWITZ:def 2;
then reconsider l = deg q as Element of NAT by INT_1:3;
H2b: l = len q - 1 by HURWITZ:def 2;
then H2c: len q = l + 1;
p.l = 0.R by D1,H2b,ALGSEQ_1:8;
then H3: q.l <> p.l by H2c,ALGSEQ_1:10;
deg q = len q - 1 & deg p = len p - 1 by HURWITZ:def 2; then
H4: max(deg p,deg q) = l by D,XREAL_1:9,XXREAL_0:def 10;
defpred P[Nat] means p.($1) <> q.($1);
A2: for k being Nat st P[k] holds k <= l
proof
let k be Nat; assume B0: P[k];
now let i be Nat; assume i > l;
then B1: i >= len q by H2c,NAT_1:13;
hence q.i = 0.R by ALGSEQ_1:8
.= p.i by B1,D,XXREAL_0:2,ALGSEQ_1:8;
end;
hence thesis by B0;
end;
A3: ex k being Nat st P[k] by H3;
consider m being Nat such that
A4: P[m] & for i being Nat st P[i] holds i <= m from NAT_1:sch 6(A2,A3);
A5: p.m <> q.m & m <= l by A2,A4;
A6: now assume A7: (p - q).m = 0.R;
p.m + 0.R = p.m + (-q.m + q.m) by RLVECT_1:5
.= (p.m + -q.m) + q.m by RLVECT_1:def 3
.= (p.m - q.m) + q.m by RLVECT_1:def 11
.= 0.R + q.m by A7,NORMSP_1:def 3;
hence contradiction by A4;
end;
then p - q <> 0_.(R) by FUNCOP_1:7,ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;
now let x be object;
assume C2: x in S;
then reconsider a = x as Element of R;
eval(r,a) = eval(p,a) - eval(q,a) by POLYNOM4:21
.= eval(p,a) - eval(p,a) by C2,A0
.= 0.R by RLVECT_1:15;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10;
end;
then C2: l + 1 <= card Roots r by A0,H4,NAT_1:43,TARSKI:def 3;
len r = m + 1
proof
E1: now let i be Nat;
assume i >= m+1; then not(i <= m) by NAT_1:13;
then X: p.i = q.i by A4;
thus r.i = p.i - q.i by NORMSP_1:def 3 .= 0.R by X,RLVECT_1:15;
end;
for k be Nat st k is_at_least_length_of r holds m+1 <= k by A6,NAT_1:13;
hence thesis by E1,ALGSEQ_1:def 2,ALGSEQ_1:def 3;
end;
then len r - 1 = m;
then C3: deg r = m by HURWITZ:def 2;
card(Roots r) <= deg r by degpoly;
then l + 1 <= m by C2,C3,XXREAL_0:2;
then C4: l + 1 <= l by A5,XXREAL_0:2;
l <= l + 1 by NAT_1:11;
then l + 1 = l by C4,XXREAL_0:1;
hence contradiction;
end;
suppose D: len p = len q;
n = len p - 1 by HURWITZ:def 2;
then H2: len p = n + 1;
H4: deg q = len q - 1 & deg p = len p - 1 by HURWITZ:def 2;
consider k being Nat such that
A1: k < len p & p.k <> q.k by HH,D,ALGSEQ_1:12;
defpred P[Nat] means p.($1) <> q.($1);
A2: for k being Nat st P[k] holds k <= n
proof
let k be Nat; assume B0: P[k];
now let i be Nat; assume i > n;
then B1: i >= len p by H2,NAT_1:13;
hence p.i = 0.R by ALGSEQ_1:8 .= q.i by D,B1,ALGSEQ_1:8;
end;
hence thesis by B0;
end;
A3: ex k being Nat st P[k] by A1;
consider m being Nat such that
A4: P[m] & for i being Nat st P[i] holds i <= m from NAT_1:sch 6(A2,A3);
A5: p.m <> q.m & m <= n by A2,A4;
A6: now assume A7: (p - q).m = 0.R;
p.m + 0.R = p.m + (-q.m + q.m) by RLVECT_1:5
.= (p.m + -q.m) + q.m by RLVECT_1:def 3
.= (p.m - q.m) + q.m by RLVECT_1:def 11
.= 0.R + q.m by A7,NORMSP_1:def 3;
hence contradiction by A4;
end;
then p - q <> 0_.(R) by FUNCOP_1:7,ORDINAL1:def 12;
then reconsider r = p - q as non zero Polynomial of R by UPROOTS:def 5;
now let x be object;
assume C2: x in S;
then reconsider a = x as Element of R;
eval(r,a) = eval(p,a) - eval(q,a) by POLYNOM4:21
.= eval(p,a) - eval(p,a) by C2,A0
.= 0.R by RLVECT_1:15;
then a is_a_root_of r by POLYNOM5:def 7;
hence x in Roots r by POLYNOM5:def 10;
end;
then C2: n + 1 <= card Roots r by H4,A0,D,NAT_1:43,TARSKI:def 3;
len r = m + 1
proof
E1: now let i be Nat;
assume i >= m+1;
then not(i <= m) by NAT_1:13;
then X: p.i = q.i by A4;
thus r.i = p.i - q.i by NORMSP_1:def 3 .= 0.R by X,RLVECT_1:15;
end;
for k be Nat st k is_at_least_length_of r holds m+1 <= k by A6,NAT_1:13;
hence thesis by E1,ALGSEQ_1:def 2,ALGSEQ_1:def 3;
end;
then len r - 1 = m;
then C3: deg r = m by HURWITZ:def 2;
card(Roots r) <= deg r by degpoly;
then n + 1 <= m by C2,C3,XXREAL_0:2;
then C4: n + 1 <= n by A5,XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then n + 1 = n by C4,XXREAL_0:1;
hence contradiction;
end;
end;
end;
hence thesis;
end;
registration
let F be algebraic-closed Field;
cluster -> with_roots for non constant Polynomial of F;
coherence
proof
let p be non constant Polynomial of F;
deg p > 0 by RATFUNC1:def 2;
then len p - 1 > 0 by HURWITZ:def 2;
then (len p -1) + 1 > 0 + 1 by XREAL_1:6;
hence p is with_roots by POLYNOM5:def 9;
end;
end;
registration
cluster F_Real -> non algebraic-closed;
coherence
proof
set q = npoly(F_Real,2);
A: 0 + 2 is even;
now assume AS: F_Real is algebraic-closed;
len q - 1 = deg q by HURWITZ:def 2 .= 2 by lem6;
then len q = 3;
hence contradiction by A,AS,POLYNOM5:def 9;
end;
hence thesis;
end;
end;
registration
cluster -> non algebraic-closed for finite domRing;
coherence
proof
let R be finite domRing;
ex q being Polynomial of R st len q > 1 & not q is with_roots
proof
set p = the Ppoly of R,[#](the carrier of R);
take q = p + 1_.(R);
A: deg p >= card([#](the carrier of R)) by m00;
then B: deg p >= 1 by NAT_1:14;
C: deg p > deg(1_.(R)) by A,RATFUNC1:def 2;
then deg q = max(deg p,deg(1_.(R))) by HURWITZ:21
.= deg p by C,XXREAL_0:def 10;
then len q - 1 >= 1 by B,HURWITZ:def 2;
then len q - 1 + 1 >= 1 + 1 by XREAL_1:6;
hence len q > 1 by NAT_1:13;
D: now let a be Element of R;
a in the carrier of R; then
D1: a in [#](the carrier of R) by SUBSET_1:def 3;
thus eval(q,a) = eval(p,a) + eval(1_.(R),a) by POLYNOM4:19
.= 0.R + eval(1_.(R),a) by D1,m1
.= 0.R + 1.R by POLYNOM4:18;
end;
now assume q is with_roots;
then consider a being Element of R such that
H: a is_a_root_of q by POLYNOM5:def 8;
0.R = eval(q,a) by H,POLYNOM5:def 7 .= 1.R by D;
hence contradiction;
end;
hence thesis;
end;
hence thesis by POLYNOM5:def 9;
end;
end;
registration
cluster algebraic-closed -> almost_right_invertible for Ring;
coherence
proof
let R be Ring;
assume AS: R is algebraic-closed;
let a be Element of R;
set p = <%1.R,a%>;
assume a <> 0.R;
then len p = 2 by POLYNOM5:40;
then consider b being Element of R such that
A: b is_a_root_of p by AS,POLYNOM5:def 8,POLYNOM5:def 9;
0.R = eval(p,b) by A,POLYNOM5:def 7 .= 1.R + a * b by POLYNOM5:44;
then 1.R = -(a * b) by RLVECT_1:6 .= a * (-b) by VECTSP_1:8;
hence a is right_invertible by ALGSTR_0:def 28;
end;
end;
theorem cc4:
for F being algebraic-closed Field,
p being non constant Polynomial of F
ex a being Element of F, q being Ppoly of F,(BRoots p) st a * q = p
proof
let F be algebraic-closed Field, p be non constant Polynomial of F;
consider q being (Ppoly of F,BRoots p),
r being non with_roots Polynomial of F such that
A: p = q *' r & Roots q = Roots p by acf;
reconsider r1 = r as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
len r - 1 <= 1 - 1 by XREAL_1:9,POLYNOM5:def 9;
then r1 is constant by HURWITZ:def 2;
then consider a being Element of F such that B: r1 = a|F by RING_4:20;
take a,q;
thus p = q *' (a * 1_.(F)) by A,B,RING_4:16
.= a * (q *' 1_.(F)) by RATFUNC1:6
.= a * q;
end;
theorem cc3:
for F being algebraic-closed Field,
p being non constant monic Polynomial of F holds p is Ppoly of F,BRoots p
proof
let R be algebraic-closed Field,
p be non constant monic Polynomial of R;
consider a being Element of R, q being Ppoly of R,(BRoots p) such that
A: p = a * q by cc4;
1.R = LC p by RATFUNC1:def 7
.= a * LC q by A,RATFUNC1:18 .= a * 1.R by cc2 .= a;
hence thesis by A;
end;
theorem
for F being Field
holds F is algebraic-closed iff
(for p being non constant monic Polynomial of F holds p is Ppoly of F)
proof
let F be Field;
now assume AS: for p being non constant monic Polynomial of F
holds p is Ppoly of F;
now let p be Polynomial of F;
assume A: len p > 1;
then B: p is non zero by POLYNOM4:3;
set np = NormPolynomial(p);
(len np - 1) + 1 > 1 by A,POLYNOM5:57;
then len np - 1 >= 1 by NAT_1:13;
then np is non constant monic by B,HURWITZ:def 2;
then reconsider np as Ppoly of F by AS;
np is with_roots;
hence p is with_roots by A,POLYNOM5:60;
end;
hence F is algebraic-closed by POLYNOM5:def 9;
end;
hence thesis by cc3;
end;