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 S_{1}[ Nat] means for p being non-zero Polynomial of L st len p = $1 holds

card (Roots p) < len p;

A1: S_{1}[1]
by UPROOTS:46, CARD_1:27;

A2: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]

then A12: len p >= 1 by NAT_1:14, POLYNOM4:5;

for n being Nat st n >= 1 holds

S_{1}[n]
from NAT_1:sch 8(A1, A2);

hence card (Roots p) < len p by A12; :: thesis: verum

let p be non-zero Polynomial of L; :: thesis: card (Roots p) < len p

defpred S

card (Roots p) < len p;

A1: S

A2: for n being Nat st n >= 1 & S

S

proof

p <> 0_. L
by UPROOTS:def 5;
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

n >= 1 and

A3: S_{1}[n]
; :: thesis: S_{1}[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

end;assume that

n >= 1 and

A3: S

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

end;

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

suppose A10:
not p is with_roots
; :: thesis: card (Roots p) < len p

end;

now :: thesis: not Roots p <> {}

hence
card (Roots p) < len p
by A4; :: thesis: verumassume
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;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

then A12: len p >= 1 by NAT_1:14, POLYNOM4:5;

for n being Nat st n >= 1 holds

S

hence card (Roots p) < len p by A12; :: thesis: verum