:: Vieta's Formula about the Sum of Roots of Polynomials
:: by Artur Korni{\l}owicz and Karol P\kak
::
:: Received May 25, 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 NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3,
FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, ARYTM_1, XBOOLE_0,
RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, ALGSTR_1, ZFMISC_1,
PRE_POLY, FUNCT_4, VALUED_0, BINOP_1, STRUCT_0, POLYNOM1, POLYNOM3,
AFINSQ_1, MESFUNC1, VECTSP_1, POLYNOM5, VECTSP_2, POLYNOM2, FUNCT_2,
UPROOTS, AOFA_I00, XCMPLX_0, POLYVIE1, BINOM, SGRAPH1, CLASSES1;
notations TARSKI, XBOOLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1,
NUMBERS, RVSUM_1,
RELAT_1, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2,
CARD_1, CLASSES1, FINSEQ_1, FINSEQ_2, FUNCT_7, XXREAL_2, NAT_1, NAT_D,
STRUCT_0, VECTSP_2, ALGSTR_0, ALGSTR_1, BINOM, RLVECT_1, RLAFFIN3,
VECTSP_1, PRE_POLY, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, FVSUM_1,
GROUP_1, UPROOTS, NIVEN;
constructors NAT_D, ALGSTR_1, POLYNOM4, POLYNOM5, RECDEF_1, XXREAL_2, FUNCT_7,
FVSUM_1, ALGSEQ_1, UPROOTS, RLAFFIN3, BINOM, FINSEQ_4, NIVEN, RVSUM_1,
CLASSES1, WSIERP_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1,
ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4, POLYNOM5, VALUED_0, XXREAL_2,
FUNCT_2, RELSET_1, UPROOTS, NAT_2, RLVECT_1, RING_3, ALGSTR_0, RATFUNC1,
NEWTON04, FINSEQ_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, POLYNOM5;
equalities FINSEQ_1, ALGSTR_0, BINOM;
expansions STRUCT_0, POLYNOM5;
theorems NAT_2, XREAL_0, TARSKI, PRE_POLY, UPROOTS, PBOOLE, POLYNOM5, NAT_1,
RLVECT_1, VECTSP_1, GROUP_1, VECTSP_2, XXREAL_0, XXREAL_2, POLYNOM4,
XREAL_1, POLYNOM3, INT_1, FINSEQ_2, FINSEQ_1, RELAT_1, RLVECT_2,
FINSEQ_4, BINOM, RLAFFIN3, FUNCT_2, NAT_D, ALGSEQ_1, NIVEN, CARD_2,
FINSEQ_3, FUNCT_1, FUNCT_7, PARTFUN1, STRUCT_0, ALGSTR_0, GRAPHSP,
ENUMSET1, ZFMISC_1, XBOOLE_1, FVSUM_1, MATRIX14, POLYNOM2, NEWTON02,
CARD_1, CLASSES1, RVSUM_1, RFINSEQ;
schemes NAT_2, FINSEQ_2;
begin
Lm1: 2-'1 = 2-1 by XREAL_0:def 2;
Lm2: 2-'2 = 2-2 by XREAL_0:def 2;
registration
let F be FinSequence;
let f be Function of dom F,dom F;
cluster F*f -> FinSequence-like;
coherence by FINSEQ_2:40;
end;
theorem
for a,b being object st a <> b holds
canFS({a,b}) = <*a,b*> or canFS({a,b}) = <*b,a*>
proof
let a,b be object;
rng canFS({a,b}) = {a,b} by FUNCT_2:def 3;
hence thesis by FINSEQ_3:99;
end;
theorem Th2:
for X being finite set holds canFS X is Enumeration of X
proof
let X be finite set;
rng canFS X = X by FUNCT_2:def 3;
hence thesis by RLAFFIN3:def 1;
end;
registration
let A be set;
let X be finite Subset of A;
cluster canFS X -> A-valued;
coherence
proof
rng canFS X = X by FUNCT_2:def 3;
hence rng canFS X c= A;
end;
end;
theorem
for L being right_zeroed non empty addLoopStr, a being Element of L
holds 2 * a = a + a
proof
let L be right_zeroed non empty addLoopStr;
let a be Element of L;
(Nat-mult-left(L)).(0+1,a) = a + (Nat-mult-left(L)).(0,a) by BINOM:def 3
.= a + 0.L by BINOM:def 3
.= a by RLVECT_1:def 4;
hence a+a = (Nat-mult-left(L)).(1+1,a) by BINOM:def 3
.= 2*a;
end;
registration
let L be almost_left_invertible multLoopStr_0;
cluster non zero -> left_invertible for Element of L;
coherence by ALGSTR_0:def 39;
end;
registration
let L be almost_right_invertible multLoopStr_0;
cluster non zero -> right_invertible for Element of L;
coherence by ALGSTR_0:def 40;
end;
registration
let L be almost_left_cancelable multLoopStr_0;
cluster non zero -> left_mult-cancelable for Element of L;
coherence by ALGSTR_0:def 36;
end;
registration
let L be almost_right_cancelable multLoopStr_0;
cluster non zero -> right_mult-cancelable for Element of L;
coherence by ALGSTR_0:def 37;
end;
theorem Th4:
for L being right_unital associative non trivial doubleLoopStr
for a,b being Element of L st b is left_invertible right_mult-cancelable
& b*(/b) = (/b)*b holds a*b/b = a
proof
let L be right_unital associative non trivial doubleLoopStr;
let a,b be Element of L;
assume
A1: b is left_invertible right_mult-cancelable;
assume b*(/b) = (/b)*b;
then b*(/b) = 1.L by A1,ALGSTR_0:def 30;
hence a = a*(b*(/b))
.= a*b/b by GROUP_1:def 3;
end;
registration
let L be non degenerated ZeroOneStr;
let z0 be Element of L;
let z1 be non zero Element of L;
cluster <%z0,z1%> -> non-zero;
coherence
proof
z1 <> 0.L;
then len <%z0,z1%> = 2 by POLYNOM5:40;
hence thesis by UPROOTS:17;
end;
cluster <%z1,z0%> -> non-zero;
coherence
proof
z0 <> 0.L or z0 = 0.L;
then len <%z1,z0%> = 2 or len <%z1,z0%> = 1 by POLYNOM5:40,41;
hence thesis by UPROOTS:17;
end;
end;
theorem
for L being non trivial ZeroStr, p being Polynomial of L st len p = 1
ex a being non zero Element of L st p = <%a%>
proof
let L be non trivial ZeroStr;
let p be Polynomial of L;
assume
A1: len p = 1;
1 = 1+0;
then p.0 <> 0.L by A1,ALGSEQ_1:10;
then reconsider a = p.0 as non zero Element of L by STRUCT_0:def 12;
take a;
let n be Element of NAT;
per cases;
suppose n = 0;
hence p.n = <%a%>.n by POLYNOM5:32;
end;
suppose n > 0;
then
A2: 0+1 <= n by NAT_1:13;
hence p.n = 0.L by A1,ALGSEQ_1:8
.= <%a%>.n by A2,POLYNOM5:32;
end;
end;
theorem Th6:
for L being non trivial ZeroStr, p being Polynomial of L st len p = 2
ex a being Element of L, b being non zero Element of L st p = <%a,b%>
proof
let L be non trivial ZeroStr;
let p be Polynomial of L;
assume
A1: len p = 2;
2 = 1+1;
then p.1 <> 0.L by A1,ALGSEQ_1:10;
then reconsider b = p.1 as non zero Element of L by STRUCT_0:def 12;
take a = p.0, b;
let n be Element of NAT;
(n = 0 or ... or n = 1) or n > 1;
then per cases;
suppose n = 0 or n = 1;
hence p.n = <%a,b%>.n by POLYNOM5:38;
end;
suppose n > 1;
then
A2: 1+1 <= n by NAT_1:13;
hence p.n = 0.L by A1,ALGSEQ_1:8
.= <%a,b%>.n by A2,POLYNOM5:38;
end;
end;
theorem
for L being non trivial ZeroStr, p being Polynomial of L st len p = 3
ex a,b being Element of L, c being non zero Element of L st p = <%a,b,c%>
proof
let L be non trivial ZeroStr;
let p be Polynomial of L;
assume
A1: len p = 3;
3 = 2+1;
then p.2 <> 0.L by A1,ALGSEQ_1:10;
then reconsider c = p.2 as non zero Element of L by STRUCT_0:def 12;
take a = p.0, b = p.1, c;
let n be Element of NAT;
(n = 0 or ... or n = 2) or n > 2;
then per cases;
suppose n = 0 or n = 1 or n = 2;
hence p.n = <%a,b,c%>.n by NIVEN:23,24,25;
end;
suppose n > 2;
then
A2: 2+1 <= n by NAT_1:13;
hence p.n = 0.L by A1,ALGSEQ_1:8
.= <%a,b,c%>.n by A2,NIVEN:26;
end;
end;
theorem Th8:
for L being add-associative right_zeroed right_complementable
associative commutative left-distributive well-unital
almost_left_invertible non empty doubleLoopStr
for a,b,x being Element of L st b <> 0.L
holds eval(<%a,b%>,-a/b) = 0.L
proof
let L be add-associative right_zeroed right_complementable
associative commutative left-distributive well-unital
almost_left_invertible non empty doubleLoopStr;
let a,b,x be Element of L;
assume b <> 0.L;
then
A1: b*(/b) = 1.L by VECTSP_1:def 10;
-a/b = (-a)/b by VECTSP_1:9;
then b*(-a/b) = (-a)*1.L by A1,GROUP_1:def 3
.= -a;
hence eval(<%a,b%>,-a/b) = a+-a by POLYNOM5:44
.= 0.L by RLVECT_1:5;
end;
theorem Th9:
for L being Field
for a,x being Element of L
for b being non zero Element of L holds
x is_a_root_of <%a,b%> iff x = -a/b
proof
let L be Field;
let a,x be Element of L;
let b be non zero Element of L;
set p = <%a,b%>;
hereby
assume
A1: x is_a_root_of p;
b*(/b) = (/b)*b;
then
A2: b*x/b = x by Th4;
a+b*x = 0.L by A1,POLYNOM5:44;
then b*x = -a by RLVECT_1:6;
hence x = -a/b by A2,VECTSP_1:9;
end;
assume x = -a/b;
hence eval(p,x) = 0.L by Th8;
end;
theorem Th10:
for L being Field
for a being Element of L
for b being non zero Element of L holds
Roots <%a,b%> = {-a/b}
proof
let L be Field;
let a be Element of L;
let b be non zero Element of L;
set p = <%a,b%>;
thus Roots p c= {-a/b}
proof
let x be object;
assume
A1: x in Roots p;
then reconsider x as Element of L;
x is_a_root_of p by A1,POLYNOM5:def 10;
then x = -a/b by Th9;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {-a/b};
then
A2: x = -a/b by TARSKI:def 1;
-a/b is_a_root_of p by Th9;
hence thesis by A2,POLYNOM5:def 10;
end;
theorem Th11:
for L being Field
for a being Element of L
for b being non zero Element of L holds
multiplicity(<%a,b%>,-a/b) = 1
proof
let L be Field;
let a be Element of L;
let b be non zero Element of L;
set p = <%a,b%>;
set x = -a/b;
set r = <%-x,1.L%>;
set j = multiplicity(p,x);
consider F being finite non empty Subset of NAT such that
A1: F = {k where k is Element of NAT : ex q being Polynomial of L st
p = (r`^k) *' q} and
A2: j = max F by UPROOTS:def 8;
j in F by A2,XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: k = j and
A4: ex q being Polynomial of L st p = (r`^k) *' q by A1;
consider q being Polynomial of L such that
A5: p = (r`^k) *' q by A4;
b <> 0.L;
then
A6: len p = 2 by POLYNOM5:40;
A7: now
assume len q = 0;
then q = 0_. L by POLYNOM4:5;
then p = 0_. L by A5,POLYNOM4:2;
hence contradiction by A6,POLYNOM4:3;
end;
then
A8: q is non-zero by UPROOTS:17;
A9: now
assume k > 1;
then k >= 1+1 by NAT_1:13;
then k+len q > 2+(0 qua Nat) by A7,XREAL_1:8;
hence contradiction by A6,A5,A8,UPROOTS:40;
end;
j >= 1 by Th9,UPROOTS:52;
then k = 1 by A3,A9,XXREAL_0:1;
then 1 in F by A1,A5;
then j >= 1 by A2,XXREAL_2:def 8;
hence thesis by A3,A9,XXREAL_0:1;
end;
theorem
for L being Field
for a being Element of L
for b being non zero Element of L holds
BRoots <%a,b%> = ({-a/b},1)-bag
proof
let L be Field;
let a be Element of L;
let b be non zero Element of L;
set r = <%a,b%>;
Roots r = {-a/b} by Th10;
then
A1: support BRoots r = {-a/b} by UPROOTS:def 9;
A2: -a/b in {-a/b} by TARSKI:def 1;
now
let i be object;
assume i in the carrier of L;
then reconsider i1 = i as Element of L;
per cases;
suppose
A3: i = -a/b;
thus (BRoots r).i = multiplicity(r,i1) by UPROOTS:def 9
.= 1 by A3,Th11
.= (({-a/b},1)-bag).i by A2,A3,UPROOTS:7;
end;
suppose i <> -a/b;
then
A4: not i in {-a/b} by TARSKI:def 1;
hence (BRoots r).i = 0 by A1,PRE_POLY:def 7
.= (({-a/b},1)-bag).i by A4,UPROOTS:6;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem
for L being Field
for a,c being Element of L
for b,d being non zero Element of L holds
Roots(<%a,b%>*'<%c,d%>) = {-a/b,-c/d}
proof
let L be Field;
let a,c be Element of L;
let b,d be non zero Element of L;
Roots(<%a,b%>) = {-a/b} & Roots(<%c,d%>) = {-c/d} by Th10;
hence {-a/b,-c/d} = Roots(<%a,b%>) \/ Roots(<%c,d%>) by ENUMSET1:1
.= Roots(<%a,b%>*'<%c,d%>) by UPROOTS:23;
end;
theorem Th14:
for L being Field
for a,x being Element of L
for b being non zero Element of L st x <> -a/b holds
multiplicity(<%a,b%>,x) = 0
proof
let L be Field;
let a,x be Element of L;
let b be non zero Element of L;
assume
A1: x <> -a/b;
set f = <%a,b%>;
Roots(f) = {-a/b} by Th10;
then not x in Roots(f) by A1,TARSKI:def 1;
then not x is_a_root_of f by POLYNOM5:def 10;
hence thesis by NAT_1:14,UPROOTS:52;
end;
theorem Th15:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not -a/b in Roots(p)
holds card Roots(<%a,b%>*'p) = 1 + card Roots(p)
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L;
A1: Roots(<%a,b%>*'p) = Roots(<%a,b%>) \/ Roots(p) by UPROOTS:23;
Roots <%a,b%> = {-a/b} by Th10;
hence thesis by A1,CARD_2:41;
end;
theorem Th16:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not -a/b in Roots(p)
holds (canFS Roots(p))^<*-a/b*> is Enumeration of Roots(<%a,b%>*'p)
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L such that
A1: not -a/b in Roots(p);
set C = canFS Roots(p);
A2: Roots(p) = rng C by FUNCT_2:def 3;
then
A3: C^<*-a/b*> is one-to-one by A1,GRAPHSP:1;
A4: rng <*-a/b*> = {-a/b} by FINSEQ_1:38;
Roots <%a,b%> = {-a/b} by Th10;
then Roots(<%a,b%>*'p) = rng C \/ rng <*-a/b*> by A2,A4,UPROOTS:23
.= rng(C^<*-a/b*>) by FINSEQ_1:31;
hence thesis by A3,RLAFFIN3:def 1;
end;
theorem Th17:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots(<%a,b%>*'p) st E = (canFS Roots(p))^<*-a/b*>
holds len E = 1 + card Roots(p) &
E.(1+card Roots(p)) = -a/b &
for n being Nat st 1 <= n <= card Roots(p) holds E.n = (canFS Roots(p)).n
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L;
set C = canFS Roots(p);
let E be Enumeration of Roots(<%a,b%>*'p) such that
A1: E = C^<*-a/b*>;
A2: len C = card Roots(p) by FINSEQ_1:93;
len <*-a/b*> = 1 by FINSEQ_1:39;
hence thesis by A1,A2,FINSEQ_1:22,64;
end;
definition
let L be non empty doubleLoopStr;
let B be bag of the carrier of L;
let E be (the carrier of L)-valued FinSequence;
func B(++)E -> FinSequence of L means :Def1:
len it = len E &
for n being Nat st 1 <= n <= len it holds it.n = (B*E).n * (E/.n);
existence
proof
deffunc F(Nat) = (B*E).$1*(E/.$1);
consider z being FinSequence of L such that
A1: len z = len E &
for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus thesis by A1,FINSEQ_3:25;
end;
uniqueness
proof
let f,g be FinSequence of L such that
A2: len f = len E and
A3: for n being Nat st 1 <= n <= len f holds f.n = (B*E).n*(E/.n) and
A4: len g = len E and
A5: for n being Nat st 1 <= n <= len g holds g.n = (B*E).n*(E/.n);
thus len f = len g by A2,A4;
let n be Nat;
assume
A6: 1 <= n <= len f;
hence f.n = (B*E).n*(E/.n) by A3
.= g.n by A2,A4,A5,A6;
end;
end;
theorem Th18:
for L being domRing
for p being non-zero Polynomial of L
for B being bag of the carrier of L
for E being Enumeration of Roots p st Roots p = {}
holds B(++)E = {}
proof
let L be domRing;
let p be non-zero Polynomial of L;
let B be bag of the carrier of L;
let E be Enumeration of Roots p such that
A1: Roots p = {};
A2: len(B(++)E) = len E by Def1;
rng E = Roots p by RLAFFIN3:def 1;
then E = {} by A1;
hence thesis by A2;
end;
theorem Th19:
for L being left_zeroed add-associative non empty doubleLoopStr
for B1,B2 being bag of the carrier of L
for E being (the carrier of L)-valued FinSequence
holds (B1+B2)(++)E = (B1(++)E) + (B2(++)E)
proof
let L be left_zeroed add-associative non empty doubleLoopStr;
let B1,B2 be bag of the carrier of L;
let E be (the carrier of L)-valued FinSequence;
A1: len(B1(++)E) = len E by Def1;
A2: len(B2(++)E) = len E by Def1;
A3: len((B1+B2)(++)E) = len E by Def1;
hence
A4: len((B1+B2)(++)E) = len((B1(++)E)+(B2(++)E)) by A1,A2,MATRIX14:2;
let n be Nat;
assume
A5: 1 <= n <= len((B1+B2)(++)E);
then
A6: n in dom((B1(++)E)+(B2(++)E)) by A4,FINSEQ_3:25;
A7: n in dom E by A3,A5,FINSEQ_3:25;
dom(B1(++)E) = dom(B2(++)E) by A1,A2,FINSEQ_3:29;
then
A8: (B1(++)E).n = (B1(++)E)/.n & (B2(++)E).n = (B2(++)E)/.n
by A1,A3,A5,FINSEQ_3:25,PARTFUN1:def 6;
A9: (B1(++)E).n = (B1*E).n * (E/.n) by A1,A3,A5,Def1;
A10: (B2(++)E).n = (B2*E).n * (E/.n) by A2,A3,A5,Def1;
A11: (B1*E).n = B1.(E.n) & (B2*E).n = B2.(E.n) by A7,FUNCT_1:13;
A12: ((B1+B2)*E).n = (B1+B2).(E.n) by A7,FUNCT_1:13
.= B1.(E.n) + B2.(E.n) by PRE_POLY:def 5;
thus ((B1+B2)(++)E).n = ((B1+B2)*E).n * (E/.n) by A5,Def1
.= (B1(++)E)/.n + (B2(++)E)/.n by A8,A9,A10,A11,A12,BINOM:15
.= ((B1(++)E)+(B2(++)E)).n by A6,A8,FVSUM_1:17;
end;
theorem Th20:
for L being left_zeroed add-associative non empty doubleLoopStr
for B being bag of the carrier of L
for E,F being (the carrier of L)-valued FinSequence
holds B(++)(E^F) = (B(++)E) ^ (B(++)F)
proof
let L be left_zeroed add-associative non empty doubleLoopStr;
let B be bag of the carrier of L;
let E,F be (the carrier of L)-valued FinSequence;
A1: len(B(++)(E^F)) = len(E^F) by Def1;
A2: len(B(++)E) = len E by Def1;
A3: len(B(++)F) = len F by Def1;
A4: len(B(++)E) + len(B(++)F) = len((B(++)E)^(B(++)F)) by FINSEQ_1:22;
A5: len(E^F) = len E + len F by FINSEQ_1:22;
then
A6: len(B(++)(E^F)) = len(B(++)E) + len(B(++)F) by A2,A3,Def1;
hence len(B(++)(E^F)) = len((B(++)E)^(B(++)F)) by FINSEQ_1:22;
let n be Nat;
assume that
A7: 1 <= n and
A8: n <= len(B(++)(E^F));
A9: (B(++)(E^F)).n = (B*(E^F)).n * ((E^F)/.n) by A7,A8,Def1;
A10: n in dom(E^F) by A1,A7,A8,FINSEQ_3:25;
then
A11: (B*(E^F)).n = B.((E^F).n) by FUNCT_1:13;
A12: E is FinSequence of L & F is FinSequence of L by NEWTON02:103;
A13: (E^F).n = (E^F)/.n by A10,PARTFUN1:def 6;
per cases;
suppose
A14: n <= len E;
then
A15: n in dom E by A7,FINSEQ_3:25;
A16: (E^F).n = E.n by A7,A14,FINSEQ_1:64;
A17: (E^F)/.n = E/.n by A15,A12,FINSEQ_4:68;
(B*E).n = B.(E.n) by A15,FUNCT_1:13;
hence (B(++)(E^F)).n = (B(++)E).n by A2,A7,A14,A9,A11,A16,A17,Def1
.= ((B(++)E)^(B(++)F)).n by A2,A7,A14,FINSEQ_1:64;
end;
suppose
A18: n > len E;
then
A19: (E^F).n = F.(n-len E) by A1,A8,FINSEQ_1:24;
set m = n-len(B(++)E);
A20: m in NAT by A2,A18,INT_1:5;
n-n < n-len E by A18,XREAL_1:15;
then
A21: 0+1 <= m by A2,A20,NAT_1:13;
A22: n-len E <= len E + len F - len E by A1,A8,A5,XREAL_1:9;
then
A23: m in dom F by A2,A20,A21,FINSEQ_3:25;
then
A24: (B*F).m = B.(F.m) by FUNCT_1:13;
F/.m = F.m by A23,PARTFUN1:def 6;
hence (B(++)(E^F)).n = (B(++)F).m
by A3,A20,A21,A22,A2,A13,A24,A19,A11,A9,Def1
.= ((B(++)E)^(B(++)F)).n by A2,A6,A4,A8,A18,FINSEQ_1:24;
end;
end;
theorem
for L being left_zeroed add-associative non empty doubleLoopStr
for B1,B2 being bag of the carrier of L
for E,F being (the carrier of L)-valued FinSequence
holds (B1+B2)(++)(E^F) = (B1(++)E)^(B1(++)F) + (B2(++)E)^(B2(++)F)
proof
let L be left_zeroed add-associative non empty doubleLoopStr;
let B1,B2 be bag of the carrier of L;
let E,F be (the carrier of L)-valued FinSequence;
thus (B1+B2)(++)(E^F) = (B1(++)(E^F)) + (B2(++)(E^F)) by Th19
.= (B1(++)E)^(B1(++)F) + (B2(++)(E^F)) by Th20
.= (B1(++)E)^(B1(++)F) + (B2(++)E)^(B2(++)F) by Th20;
end;
theorem Th22:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots(<%a,b%>*'p)
for P being Permutation of dom E
holds (BRoots(<%a,b%>*'p)(++)E)*P = BRoots(<%a,b%>*'p)(++)(E*P)
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L;
set q = <%a,b%>;
set B = BRoots(q*'p);
let E be Enumeration of Roots(q*'p);
let P be Permutation of dom E;
len E = len(B(++)E) by Def1;
then
A1: dom E = dom(B(++)E) by FINSEQ_3:29;
then reconsider P1 = P as Permutation of dom(B(++)E);
(B(++)E)*P1 = B(++)(E*P)
proof
A2: len(E*P) = len(B(++)(E*P)) by Def1;
A3: rng P = dom E by FUNCT_2:def 3;
then
A4: dom((B(++)E)*P1) = dom(P1) by A1,RELAT_1:27;
A5: dom(P1) = dom(E*P) by A3,RELAT_1:27;
hence
A6: len((B(++)E)*P1) = len(B(++)(E*P)) by A2,A4,FINSEQ_3:29;
let n be Nat such that
A7: 1 <= n and
A8: n <= len((B(++)E)*P1);
A9: n in dom((B(++)E)*P1) by A7,A8,FINSEQ_3:25;
A10: (B*E).(P1.n) = (B*E*P1).n by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
.= (B*(E*P)).n by RELAT_1:36;
A11: P1.n in rng P1 by A4,A9,FUNCT_1:def 3;
then
A12: 1 <= P1.n & P1.n <= len(B(++)E) by FINSEQ_3:25;
A13: E/.(P1.n) = E.(P1.n) by A3,A11,PARTFUN1:def 6
.= (E*P1).n by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
.= (E*P)/.n by A4,A5,A7,A8,FINSEQ_3:25,PARTFUN1:def 6;
thus ((B(++)E)*P1).n = (B(++)E).(P1.n) by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
.= (B*E).(P1.n) * (E/.(P1.n)) by A12,Def1
.= (B(++)(E*P)).n by A6,A7,A8,A10,A13,Def1;
end;
hence thesis;
end;
theorem Th23:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not -a/b in Roots(p)
for E being Enumeration of Roots(<%a,b%>*'p) st E = (canFS Roots(p))^<*-a/b*>
holds (canFS Roots(<%a,b%>*'p))" * E is Permutation of dom E
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L such that
A1: not -a/b in Roots(p);
set q = <%a,b%>;
set e = <*-a/b*>;
set B = BRoots(q*'p);
set C = canFS Roots(p);
set D = canFS Roots(q*'p);
let E be Enumeration of Roots(q*'p) such that
A2: E = C^e;
A3: dom E = Seg(len C + len e) by A2,FINSEQ_1:def 7;
A4: len C = card Roots(p) by FINSEQ_1:93;
A5: len e = 1 by FINSEQ_1:40;
A6: card Roots(q*'p) = 1 + card Roots(p) by A1,Th15;
A7: rng D = Roots(q*'p) by FUNCT_2:def 3;
A8: rng(D") = dom D by FUNCT_1:33;
A9: dom(D") = rng D by FUNCT_1:33;
A10: dom D = Seg len D by FINSEQ_1:def 3;
A11: len D = card Roots(q*'p) by FINSEQ_1:93;
A12: Roots(q*'p) = Roots(q) \/ Roots(p) by UPROOTS:23;
A13: rng C = Roots(p) by FUNCT_2:def 3;
A14: rng e = {-a/b} by FINSEQ_1:39;
A15: Roots(q) = {-a/b} by Th10;
A16: rng(E) = rng C \/ rng e by A2,FINSEQ_1:31;
then
A17: rng(D"*E) = rng(D") by A9,A12,A13,A14,A15,RELAT_1:28;
dom(D"*E) = dom(E) by A7,A9,A12,A13,A14,A15,A16,RELAT_1:27;
then D"*E is Function of dom E,dom E
by A3,A4,A5,A6,A8,A10,A11,A17,FUNCT_2:1;
hence D"*E is Permutation of dom E
by A3,A4,A5,A6,A8,A10,A11,A17,FUNCT_2:57;
end;
theorem Th24:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not -a/b in Roots(p)
for E being Enumeration of Roots(<%a,b%>*'p) st E = (canFS Roots(p))^<*-a/b*>
holds
Sum(BRoots(<%a,b%>*'p)(++)E) =
Sum(BRoots(<%a,b%>*'p)(++)canFS Roots(<%a,b%>*'p))
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L such that
A1: not -a/b in Roots(p);
set q = <%a,b%>;
set B = BRoots(q*'p);
set C = canFS Roots(p);
set D = canFS Roots(q*'p);
let E be Enumeration of Roots(q*'p);
assume E = C^<*-a/b*>;
then reconsider P = D"*E as Permutation of dom E by A1,Th23;
len(B(++)E) = len E by Def1;
then
A2: dom(B(++)E) = dom E by FINSEQ_3:29;
D"" = D by FUNCT_1:43;
then
A3: P" = E"*D by FUNCT_1:44;
A4: E*E"*D = D
proof
A5: rng D = Roots(q*'p) by FUNCT_2:def 3;
A6: rng E = Roots(q*'p) by RLAFFIN3:def 1;
dom(E*E") = rng E by FUNCT_1:37;
hence
A7: dom(E*E"*D) = dom D by A5,A6,RELAT_1:27;
let x be object such that
A8: x in dom(E*E"*D);
D.x in rng E by A5,A6,A7,A8,FUNCT_1:def 3;
hence D.x = (E*E").(D.x) by FUNCT_1:35
.= (E*E"*D).x by A8,FUNCT_1:12;
end;
(B(++)E)*P" = B(++)(E*P") by Th22;
hence Sum(B(++)E) = Sum(B(++)(E*P")) by A2,RLVECT_2:7
.= Sum(B(++)D) by A3,A4,RELAT_1:36;
end;
theorem Th25:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots(<%a,b%>*'p)
holds Sum(BRoots(<%a,b%>)(++)E) = -a/b
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L;
set q = <%a,b%>;
let E be Enumeration of Roots(q*'p);
set B = BRoots(q);
set F = B(++)E;
A1: len F = len E by Def1;
A2: -a/b in {-a/b} by TARSKI:def 1;
A3: Roots(q) = {-a/b} by Th10;
A4: Roots(q*'p) = Roots(q) \/ Roots(p) by UPROOTS:23;
A5: Roots(q) c= Roots(q) \/ Roots(p) by XBOOLE_1:7;
A6: dom E = dom F by A1,FINSEQ_3:29;
rng E = Roots(q*'p) by RLAFFIN3:def 1;
then consider j being object such that
A7: j in dom E and
A8: E.j = -a/b by A2,A3,A4,A5,FUNCT_1:def 3;
reconsider j as Element of NAT by A7;
A9: 1 <= j by A7,FINSEQ_3:25;
A10: j <= len F by A7,A1,FINSEQ_3:25;
A11: E.j = E/.j by A7,PARTFUN1:def 6;
A12: (B*E).j = B.(E.j) by A7,FUNCT_1:13
.= multiplicity(<%a,b%>,-a/b) by A8,UPROOTS:def 9
.= 1 by Th11;
now
let i be Element of NAT such that
A13: i in dom F and
A14: i <> j;
A15: 1 <= i & i <= len F by A13,FINSEQ_3:25;
A16: E.i = E/.i by A6,A13,PARTFUN1:def 6;
A17: (B*E).i = B.(E.i) by A6,A13,FUNCT_1:13
.= multiplicity(q,E/.i) by A16,UPROOTS:def 9
.= 0 by A16,A8,A6,A7,A13,A14,FUNCT_1:def 4,Th14;
thus F/.i = F.i by A13,PARTFUN1:def 6
.= (B*E).i * (E/.i) by A15,Def1
.= 0.L by A17,BINOM:12;
end;
hence Sum F = F/.j by A6,A7,POLYNOM2:3
.= F.j by A6,A7,PARTFUN1:def 6
.= (B*E).j * (E/.j) by A9,A10,Def1
.= -a/b by A8,A11,A12,BINOM:13;
end;
definition
let L be domRing;
let p be non-zero Polynomial of L;
func SumRoots(p) -> Element of L equals
Sum (BRoots(p)(++)canFS Roots p);
coherence;
end;
theorem
for L being domRing
for p being non-zero Polynomial of L st Roots p = {} holds
SumRoots p = 0.L
proof
let L be domRing;
let p be non-zero Polynomial of L such that
A1: Roots p = {};
canFS Roots p is Enumeration of Roots p by Th2;
then BRoots(p)(++)canFS Roots p = {} by A1,Th18;
then len (BRoots(p)(++)canFS Roots p) = 0;
hence thesis by RLVECT_1:75;
end;
theorem Th27:
for L being Field
for a being Element of L
for b being non zero Element of L holds
SumRoots <%a,b%> = -a/b
proof
let L be Field;
let a be Element of L;
let b be non zero Element of L;
set p = <%a,b%>;
set B = BRoots(p);
A1: Roots p = {-a/b} by Th10;
reconsider E = canFS Roots p as Enumeration of Roots p by Th2;
set F = B(++)E;
consider g being sequence of L such that
A2: Sum(F) = g.(len F) and
A3: g.0 = 0.L and
A4: for j being Nat, v being Element of L st j < len F & v = F.(j+1)
holds g.(j+1) = g.j + v by RLVECT_1:def 12;
A5: E = <*-a/b*> by A1,FINSEQ_1:94;
A6: len F = len E by Def1;
A7: len E = 1 by A5,FINSEQ_1:39;
A8: 1 in dom E by A7,FINSEQ_3:25;
A9: (B*E).1 = B.(E.1) by A8,FUNCT_1:13
.= multiplicity(p,-a/b) by A5,UPROOTS:def 9
.= 1 by Th11;
A10: F.1 = (B*E).1*(E/.1) by A6,A7,Def1
.= E/.1 by A9,BINOM:13;
then reconsider v = F.1 as Element of L;
A11: 0 < len F by A7,Def1;
thus SumRoots p = g.(0+1) by A2,A7,Def1
.= g.0 + v by A4,A11
.= -a/b by A5,A3,A10,FINSEQ_4:16;
end;
theorem Th28:
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
holds SumRoots(<%a,b%>*'p) = -a/b + SumRoots(p)
proof
let L be Field;
let p be non-zero Polynomial of L;
let a be Element of L;
let b be non zero Element of L;
set q = <%a,b%>;
set B = BRoots p;
set C = canFS Roots(p);
set E = canFS Roots(q*'p);
set F = BRoots(q*'p)(++)E;
set G = B(++)C;
consider g being sequence of L such that
A1: SumRoots(p) = g.(len G) and
A2: g.0 = 0.L and
A3: for j being Nat, v being Element of L st j < len G & v = G.(j+1)
holds g.(j+1) = g.j + v by RLVECT_1:def 12;
A4: len G = len C by Def1;
A5: len C = card Roots(p) by FINSEQ_1:93;
A6: dom g = NAT by FUNCT_2:def 1;
per cases;
suppose
A7: not -a/b in Roots(p);
then reconsider N = C^<*-a/b*> as Enumeration of Roots(q*'p) by Th16;
A8: len N = 1 + card Roots(p) by Th17;
set BN = BRoots(q*'p)(++)N;
A9: len BN = len N by Def1;
A10: Sum(BN) = SumRoots(q*'p) by A7,Th24;
set f = g+*(1+len G,-a/b+SumRoots(p));
A11: f.0 = g.0 by FUNCT_7:32;
A12: f.(len BN) = -a/b+SumRoots(p) by A5,A9,A8,A4,A6,FUNCT_7:31;
now
let j be Nat, v be Element of L such that
A13: j < len BN and
A14: v = BN.(j+1);
reconsider C as Enumeration of Roots(p) by Th2;
A15: f.j = g.j by A5,A9,A8,A4,A13,FUNCT_7:32;
A16: j+1 <= len BN by A13,NAT_1:13;
then
A17: BN.(j+1) = (BRoots(q*'p)*N).(j+1) * (N/.(j+1)) by Def1,NAT_1:11;
A18: j+1 in dom N by A9,A16,NAT_1:11,FINSEQ_3:25;
then
A19: N.(j+1) = N/.(j+1) by PARTFUN1:def 6;
A20: multiplicity(q*'p,N/.(j+1)) =
multiplicity(q,N/.(j+1))+multiplicity(p,N/.(j+1)) by UPROOTS:55;
j <= len G by A5,A9,A8,A4,A13,NAT_1:13;
then per cases by XXREAL_0:1;
suppose
A21: j < len G;
then j+1 < 1+len G by XREAL_1:8;
then
A22: f.(j+1) = g.(j+1) by FUNCT_7:32;
A23: j+1 <= len G by A21,NAT_1:13;
A24: j+1 in dom C by A4,A23,NAT_1:11,FINSEQ_3:25;
then
A25: C.(j+1) = C/.(j+1) by PARTFUN1:def 6;
A26: N/.(j+1) = C/.(j+1) by A4,A5,A23,A19,A25,Th17,NAT_1:11;
now
assume N/.(j+1) is_a_root_of q;
then
A27: N/.(j+1) in Roots(q) by POLYNOM5:def 10;
Roots(<%a,b%>) = {-a/b} by Th10;
then
A28: N/.(j+1) = -a/b by A27,TARSKI:def 1;
A29: C.(j+1) in rng C by A24,FUNCT_1:def 3;
rng C c= Roots(p) by FINSEQ_1:def 4;
hence contradiction by A7,A25,A26,A28,A29;
end;
then
A30: multiplicity(q,N/.(j+1)) = 0 by NAT_1:14,UPROOTS:52;
A31: (BRoots(q*'p)*N).(j+1) = (BRoots(q*'p)).(N.(j+1)) by A18,FUNCT_1:13
.= multiplicity(q*'p,N/.(j+1)) by A19,UPROOTS:def 9
.= (BRoots(p)).(C.(j+1)) by A25,A26,A20,A30,UPROOTS:def 9
.= (BRoots(p)*C).(j+1) by A24,FUNCT_1:13;
BN.(j+1) = G.(j+1) by A23,A26,A31,A17,Def1,NAT_1:11;
hence f.(j+1) = f.j + v by A21,A3,A14,A15,A22;
end;
suppose
A32: j = len G;
then
A33: f.(j+1) = -a/b+SumRoots(p) by A6,FUNCT_7:31;
A34: (BRoots(q*'p)*N).(j+1) = (BRoots(q*'p)).(N.(j+1)) by A18,FUNCT_1:13;
not -a/b is_a_root_of p by A7,POLYNOM5:def 10;
then
A35: multiplicity(p,-a/b) = 0 by NAT_1:14,UPROOTS:52;
(BRoots(q*'p)).(N.(j+1)) = multiplicity(q,-a/b)+multiplicity(p,-a/b)
by A4,A19,A20,A32,UPROOTS:def 9
.= 1 by A35,Th11;
hence f.(j+1) = f.j + v
by A1,A4,A14,A15,A17,A19,A32,A33,A34,BINOM:13;
end;
end;
hence thesis by A2,A12,A11,A10,RLVECT_1:def 12;
end;
suppose
A36: -a/b in Roots(p);
Roots(q) = {-a/b} by Th10;
then
A37: Roots(p) = Roots(q) \/ Roots(p) by A36,XBOOLE_1:12,ZFMISC_1:31
.= Roots(q*'p) by UPROOTS:23;
reconsider E as Enumeration of Roots(q*'p) by Th2;
A38: len(B(++)E) = len E by Def1;
A39: Sum(BRoots(q)(++)E) = -a/b by Th25;
len(BRoots(q)(++)E) = len E by Def1;
then
A40: (BRoots(q)(++)E) is Element of (len E)-tuples_on the carrier of L
by FINSEQ_2:92;
A41: (B(++)E) is Element of (len E)-tuples_on the carrier of L
by A38,FINSEQ_2:92;
BRoots(q*'p) = BRoots(q) + BRoots(p) by UPROOTS:56;
hence SumRoots(q*'p) = Sum((BRoots(q)(++)E)+(BRoots(p)(++)E)) by Th19
.= -a/b + SumRoots(p) by A37,A39,A40,A41,FVSUM_1:76;
end;
end;
theorem
for L being Field
for a,c being Element of L
for b,d being non zero Element of L
holds SumRoots(<%a,b%>*'<%c,d%>) = (-a/b) + (-c/d)
proof
let L be Field;
let a,c be Element of L;
let b,d be non zero Element of L;
SumRoots(<%a,b%>) = -a/b & SumRoots(<%c,d%>) = -c/d by Th27;
hence thesis by Th28;
end;
theorem
for L being algebraic-closed Field
for p,q being non-zero Polynomial of L st
len p >= 2 holds SumRoots(p*'q) = SumRoots(p) + SumRoots(q)
proof
let L be algebraic-closed Field;
let p,q be non-zero Polynomial of L;
assume len p >= 2;
then len p <> 0 & len p <> 1;
then
A1: len p is non trivial by NAT_2:28;
defpred P[Nat] means
for f being non-zero Polynomial of L st $1 = len f holds
SumRoots(f*'q) = SumRoots(f) + SumRoots(q);
A2: P[2]
proof
let f be non-zero Polynomial of L;
assume len f = 2;
then consider a being Element of L, b being non zero Element of L
such that
A3: f = <%a,b%> by Th6;
SumRoots f = -a/b by A3,Th27;
hence thesis by A3,Th28;
end;
A4: for k being non trivial Nat st P[k] holds P[k+1]
proof
let k be non trivial Nat such that
A5: P[k];
let p being non-zero Polynomial of L such that
A6: k+1 = len p;
A7: k >= 2 by NAT_2:29;
k+1 >= k by NAT_1:11;
then k+1 >= 2 by A7,XXREAL_0:2;
then len p > 1 by A6,XXREAL_0:2;
then p is with_roots by POLYNOM5:def 9;
then consider r being Element of L such that
A8: r is_a_root_of p;
set P = poly_quotient(p,r);
A9: len P + 1 = len p by A6,A8,UPROOTS:def 7;
then reconsider P as non-zero Polynomial of L by A6,UPROOTS:17;
A10: p = <%-r,1.L%>*'P by A8,UPROOTS:50;
then
A11: SumRoots(p) = -(-r)/1.L + SumRoots(P) by Th28;
p*'q = <%-r,1.L%>*'(P*'q) by A10,POLYNOM3:33;
hence SumRoots(p*'q) = -(-r)/1.L + SumRoots(P*'q) by Th28
.= r + (SumRoots(P) + SumRoots(q)) by A5,A6,A9
.= SumRoots(p) + SumRoots(q) by A11,RLVECT_1:def 3;
end;
for k being non trivial Nat holds P[k] from NAT_2:sch 2(A2,A4);
hence thesis by A1;
end;
theorem
for L being algebraic-closed domRing, p being non-zero Polynomial of L
for r being FinSequence of L st r is one-to-one & len r = len p-'1 &
Roots p = rng r holds Sum r = SumRoots p
proof
let L be algebraic-closed domRing, p be non-zero Polynomial of L;
let r be FinSequence of L such that
A1: r is one-to-one and
A2: len r = len p-'1 and
A3: Roots p = rng r;
set B = BRoots p, s = support B;
set L1 = (len r) |-> 1;
consider f being FinSequence of NAT such that
A4: degree B = Sum f & f = B * canFS s by UPROOTS:def 4;
A5: degree B = len p-'1 by UPROOTS:59;
A6: card dom r = card rng r & dom r = Seg len r by A1,CARD_1:70,FINSEQ_1:def 3;
A7: s = Roots p by UPROOTS:def 9;
A8: s c= dom B & rng canFS s = s by PRE_POLY:37,FUNCT_2:def 3;
then
A9: dom f = dom canFS s by A4,RELAT_1:27;
then
A10: len f = len canFS s = card s by FINSEQ_3:29,FINSEQ_1:93;
then
A11: len f = len r by A3,A6,UPROOTS:def 9;
A12: f is len r -element by A10,A6,A7,A3,CARD_1:def 7;
reconsider E = canFS s as FinSequence of L by A8,FINSEQ_1:def 4;
A13: dom f = dom r by A10,A6,A7,A3,FINSEQ_3:29;
A14: for j being Nat st j in Seg len r holds f.j >= L1.j
proof
let j be Nat such that
A15: j in Seg len r;
A16: (canFS s).j in s by A13,A9,A6,A8,A15,FUNCT_1:def 3;
then reconsider c = E.j as Element of L;
c is_a_root_of p by A16,A7,POLYNOM5:def 10;
then multiplicity(p,c) >= 1 by UPROOTS:52;
then B.c >= 1 by UPROOTS:def 9;
then f.j >= 1 by A13,A6,A4,A15,FUNCT_1:12;
hence thesis by A15,FINSEQ_2:57;
end;
A17: Sum L1 = 1*len r by RVSUM_1:80;
A18: len (B(++)E) = len E by Def1;
for j being Nat st 1 <= j <= len E holds (B(++)E).j = E.j
proof
let j be Nat such that
A19: 1 <=j <= len E;
A20: j in Seg len r by A19,A11,A10;
then f.j >= L1.j & f.j <= L1.j & L1.j = 1
by A2,A14,A12,A17,A4,A5,RVSUM_1:83,FINSEQ_2:57;
then
A21: f.j = 1 by XXREAL_0:1;
A22: E/.j = E.j by A20,A13,A9,A6,PARTFUN1:def 6;
(B(++)E).j = (f.j) * (E/.j) by A4,A19,A18,Def1;
hence thesis by BINOM:13,A21,A22;
end;
then
A23: B(++)E = E by A18,FINSEQ_1:14;
E,r are_fiberwise_equipotent by A1,A3,A8,UPROOTS:def 9,RFINSEQ:26;
then ex P be Permutation of dom E st E = r*P by CLASSES1:80,A13,A9;
hence thesis by A23,RLVECT_2:7,A13,A9,A7;
end;
::$N Vieta's formula about the sum of roots
theorem
for L being algebraic-closed Field, p being non-zero Polynomial of L holds
len p >= 2 implies SumRoots p = - p.(len p-'2) / p.(len p-'1)
proof
let L be algebraic-closed Field, p be non-zero Polynomial of L;
assume len p >= 2;
then len p <> 0 & len p <> 1;
then
A1: len p is non trivial by NAT_2:28;
defpred P[Nat] means
for p being non-zero Polynomial of L holds
$1 = len p implies SumRoots p = - p.($1-'2) / p.($1-'1);
A2: P[2]
proof
let p be non-zero Polynomial of L;
assume len p = 2;
then consider a being Element of L, b being non zero Element of L
such that
A3: p = <%a,b%> by Th6;
p.0 = a & p.1 = b by A3,POLYNOM5:38;
hence thesis by A3,Lm1,Lm2,Th27;
end;
A4: for k being non trivial Nat st P[k] holds P[k+1]
proof
let k be non trivial Nat such that
A5: P[k];
let p being non-zero Polynomial of L such that
A6: k+1 = len p;
A7: k+1-'1 = k by NAT_D:34;
k-1 >= 2-1 by XREAL_1:9,NAT_2:29;
then
A8: k+1-'2 = k+1-2 by XREAL_0:def 2
.= k-1;
then reconsider k1 = k-1 as Nat;
A9: k >= 2 by NAT_2:29;
k+1 >= k by NAT_1:11;
then k+1 >= 2 by A9,XXREAL_0:2;
then len p > 1 by A6,XXREAL_0:2;
then p is with_roots by POLYNOM5:def 9;
then consider r being Element of L such that
A10: r is_a_root_of p;
set P = poly_quotient(p,r);
A11: len P + 1 = len p by A6,A10,UPROOTS:def 7;
then reconsider P as non-zero Polynomial of L by A6,UPROOTS:17;
reconsider k2 = k-2 as Element of NAT by NAT_2:29,INT_1:5;
A12: k-'2 = k2 by XREAL_0:def 2;
A13: k-'1 = k1 by XREAL_0:def 2;
A14: P.k = 0.L by A6,A11,ALGSEQ_1:8;
A15: p = <%-r,1.L%>*'P by A10,UPROOTS:50;
then
A16: p.(k1+1) = (-r)*P.(k1+1)+1.L*P.k1 by UPROOTS:37;
A17: p.(k2+1) = (-r)*P.(k2+1)+1.L*P.k2 by A15,UPROOTS:37;
-((-r)*P.k1) = (--r)*P.k1 by VECTSP_1:9;
then
A18: -((-r)*P.k1+P.k2) = r*P.k1 - P.k2 by RLVECT_1:30;
A19: len P = k1+1 by A6,A11;
then
A20: P.k1 <> 0.L by ALGSEQ_1:10;
A21: P.k1*(/P.k1) = (/P.k1)*P.k1;
P.k1 is non zero by A19,ALGSEQ_1:10;
then
A22: r = r*P.k1/P.k1 by A21,Th4;
thus SumRoots(p) = -(-r)/1.L + SumRoots(P) by A15,Th28
.= r - P.k2/P.k1 by A5,A6,A11,A12,A13
.= (r*P.k1-P.k2) / P.k1 by A20,A22,VECTSP_2:20
.= - p.(k+1-'2) / p.(k+1-'1) by A7,A8,A14,A16,A17,A18,A20,VECTSP_2:19;
end;
for k being non trivial Nat holds P[k] from NAT_2:sch 2(A2,A4);
hence thesis by A1;
end;