let L be algebraic-closed Field; :: thesis: for p being non-zero Polynomial of L st len p >= 2 holds
SumRoots p = - ((p . ((len p) -' 2)) / (p . ((len p) -' 1)))
let p be non-zero Polynomial of L; :: thesis: ( len p >= 2 implies SumRoots p = - ((p . ((len p) -' 2)) / (p . ((len p) -' 1))) )
assume len p >= 2 ; :: thesis: SumRoots p = - ((p . ((len p) -' 2)) / (p . ((len p) -' 1)))
then ( len p <> 0 & len p <> 1 ) ;
then A1: not len p is trivial by NAT_2:28;
defpred S₁[ Nat] means for p being non-zero Polynomial of L st $1 = len p holds
SumRoots p = - ((p . ($1 -' 2)) / (p . ($1 -' 1)));
A2: S₁[2]

proof

let p be non-zero Polynomial of L; :: thesis: ( 2 = len p implies SumRoots p = - ((p . (2 -' 2)) / (p . (2 -' 1))) )
assume len p = 2 ; :: thesis: SumRoots p = - ((p . (2 -' 2)) / (p . (2 -' 1)))
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 SumRoots p = - ((p . (2 -' 2)) / (p . (2 -' 1))) by A3, Lm1, Lm2, Th27; :: thesis: verum

end;

A4: for k being non trivial Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non trivial Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let p be non-zero Polynomial of L; :: thesis: ( k + 1 = len p implies SumRoots p = - ((p . ((k + 1) -' 2)) / (p . ((k + 1) -' 1))) )
assume A6: k + 1 = len p ; :: thesis: SumRoots p = - ((p . ((k + 1) -' 2)) / (p . ((k + 1) -' 1)))
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 (poly_quotient (p,r))) + 1 = len p by A6, A10, UPROOTS:def 7;
then reconsider P = poly_quotient (p,r) 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) ;
not P . k1 is 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 ; :: thesis: verum

end;

for k being non trivial Nat holds S₁[k] from NAT_2:sch 2(A2, A4);
hence SumRoots p = - ((p . ((len p) -' 2)) / (p . ((len p) -' 1))) by A1; :: thesis: verum