let L be domRing; :: thesis: for p being non-zero Polynomial of L holds card (Roots p) < len p
let p be non-zero Polynomial of L; :: thesis: card (Roots p) < len p
defpred S1[ Nat] means for p being non-zero Polynomial of L st len p = $1 holds
card (Roots p) < len p;
A1: S1[1] by UPROOTS:46, CARD_1:27;
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1 and
A3: S1[n] ; :: thesis: S1[n + 1]
let p be non-zero Polynomial of L; :: thesis: ( len p = n + 1 implies card (Roots p) < len p )
assume A4: len p = n + 1 ; :: thesis: card (Roots p) < len p
per cases ( p is with_roots or not p is with_roots ) ;
suppose p is with_roots ; :: thesis: card (Roots p) < len p
then consider x being Element of L such that
A5: x is_a_root_of p by POLYNOM5:def 8;
set r = <%(- x),(1. L)%>;
set pq = poly_quotient (p,x);
len (poly_quotient (p,x)) > 0 by A5, UPROOTS:47;
then poly_quotient (p,x) <> 0_. L by POLYNOM4:3;
then reconsider pq = poly_quotient (p,x) as non-zero Polynomial of L by UPROOTS:def 5;
set Rr = Roots <%(- x),(1. L)%>;
set Rpq = Roots pq;
p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, UPROOTS:50;
then A6: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots pq) by UPROOTS:23;
A7: Roots <%(- x),(1. L)%> = {x} by UPROOTS:48;
A8: (len pq) + 1 = len p by A4, A5, UPROOTS:def 7;
card (Roots <%(- x),(1. L)%>) = 1 by A7, CARD_1:30;
then A9: card ((Roots <%(- x),(1. L)%>) \/ (Roots pq)) <= (card (Roots pq)) + 1 by CARD_2:43;
(card (Roots pq)) + 1 < n + 1 by A8, A3, A4, XREAL_1:8;
hence card (Roots p) < len p by A4, A6, A9, XXREAL_0:2; :: thesis: verum
end;
suppose A10: not p is with_roots ; :: thesis: card (Roots p) < len p
now :: thesis: not Roots p <> {}
assume Roots p <> {} ; :: thesis: contradiction
then consider x being object such that
A11: x in Roots p by XBOOLE_0:def 1;
reconsider x = x as Element of L by A11;
x is_a_root_of p by A11, POLYNOM5:def 10;
hence contradiction by A10, POLYNOM5:def 8; :: thesis: verum
end;
hence card (Roots p) < len p by A4; :: thesis: verum
end;
end;
end;
p <> 0_. L by UPROOTS:def 5;
then A12: len p >= 1 by NAT_1:14, POLYNOM4:5;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A1, A2);
 hence card (Roots p) < len p by A12; :: thesis: verum