let L be Field; :: thesis: for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n )
defpred S₁[ Nat] means for f being non-zero Polynomial of L st deg f = $1 holds
ex m being Element of NAT st
( m = card (Roots f) & m <= $1 );
A1: S₁[ 0 ]

proof

let f be non-zero Polynomial of L; :: thesis: ( deg f = 0 implies ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) )
assume A2: deg f = 0 ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= 0 )
A3: f <> 0_. L by UPROOTS:def 5;
A4: f . 0 <> 0. L

proof

assume f . 0 = 0. L ; :: thesis: contradiction
then f = <%(0. L)%> by A2, ALGSEQ_1:def 6;
hence contradiction by A3, POLYNOM5:35; :: thesis: verum

end;

reconsider x = f . 0 as Element of L ;
A5: f = <%x%> by A2, ALGSEQ_1:def 6;

A6: now

let z be Element of L; :: thesis: eval <%x%>,z <> 0. L
eval <%x%>,z = eval <%x,(0. L)%>,z by POLYNOM5:44
.= x by POLYNOM5:46 ;
hence eval <%x%>,z <> 0. L by A4; :: thesis: verum

end;

Roots f = {}

proof

assume Roots f <> {} ; :: thesis: contradiction
then consider z being set such that
A7: z in Roots f by XBOOLE_0:def 1;
reconsider z = z as Element of L by A7;
z is_a_root_of f by A7, POLYNOM5:def 9;
then eval <%x%>,z = 0. L by A5, POLYNOM5:def 6;
hence contradiction by A6; :: thesis: verum

end;

then card (Roots f) = 0 ;
hence ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) ; :: thesis: verum

end;

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now

let f be non-zero Polynomial of L; :: thesis: ( deg f = k + 1 implies ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) )
A10: f <> 0_. L by UPROOTS:def 5;
assume A11: deg f = k + 1 ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )
thus ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) :: thesis: verum

proof

per cases ( Roots f = {} or Roots f <> {} ) ;

suppose Roots f = {} ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )

then card (Roots f) = 0 ;
hence ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) ; :: thesis: verum

end;

suppose Roots f <> {} ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )

then consider z being set such that
A12: z in Roots f by XBOOLE_0:def 1;
reconsider z = z as Element of L by A12;
A13: z is_a_root_of f by A12, POLYNOM5:def 9;
then A14: rpoly 1,z divides f by HURWITZ:35;
set g = f div (rpoly 1,z);
0_. L = f mod (rpoly 1,z) by A14, HURWITZ:def 7;
then (f div (rpoly 1,z)) *' (rpoly 1,z) = (f - ((f div (rpoly 1,z)) *' (rpoly 1,z))) + ((f div (rpoly 1,z)) *' (rpoly 1,z)) by POLYNOM3:29;
then (f div (rpoly 1,z)) *' (rpoly 1,z) = f + ((- ((f div (rpoly 1,z)) *' (rpoly 1,z))) + ((f div (rpoly 1,z)) *' (rpoly 1,z))) by POLYNOM3:26;
then (f div (rpoly 1,z)) *' (rpoly 1,z) = f + (((f div (rpoly 1,z)) *' (rpoly 1,z)) - ((f div (rpoly 1,z)) *' (rpoly 1,z))) ;
then (f div (rpoly 1,z)) *' (rpoly 1,z) = f + (0_. L) by POLYNOM3:30;
then A15: f = (f div (rpoly 1,z)) *' (rpoly 1,z) by POLYNOM3:29;
f div (rpoly 1,z) <> 0_. L by A10, A15, POLYNOM3:35;
then reconsider g = f div (rpoly 1,z) as non-zero Polynomial of L by UPROOTS:def 5;
A16: deg g = (k + 1) - 1 by A10, A11, A13, HURWITZ:36
.= k ;
set RG = Roots g;
consider m1 being Element of NAT such that
A17: ( m1 = card (Roots g) & m1 <= k ) by A9, A16;
A18: Roots f c= (Roots g) \/ {z}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Roots f or y in (Roots g) \/ {z} )
assume A19: y in Roots f ; :: thesis: y in (Roots g) \/ {z}
then reconsider y1 = y as Element of L ;
y1 is_a_root_of f by A19, POLYNOM5:def 9;
then eval f,y1 = 0. L by POLYNOM5:def 6;
then (eval g,y1) * (eval (rpoly 1,z),y1) = 0. L by A15, POLYNOM4:27;
then A20: (eval g,y1) * (y1 - z) = 0. L by HURWITZ:29;

now

per cases ( y1 = z or y1 <> z ) ;

suppose y1 = z ; :: thesis: y in (Roots g) \/ {z}

then y in {z} by TARSKI:def 1;
hence y in (Roots g) \/ {z} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y1 <> z ; :: thesis: y in (Roots g) \/ {z}

then y1 - z <> 0. L by RLVECT_1:35;
then eval g,y1 = 0. L by A20, VECTSP_1:44;
then y1 is_a_root_of g by POLYNOM5:def 6;
then y1 in Roots g by POLYNOM5:def 9;
hence y in (Roots g) \/ {z} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence y in (Roots g) \/ {z} ; :: thesis: verum

end;

set RF = Roots f;
card ((Roots g) \/ {z}) <= (card (Roots g)) + (card {z}) by CARD_2:62;
then A21: card ((Roots g) \/ {z}) <= (card (Roots g)) + 1 by CARD_2:60;
card (Roots f) <= card ((Roots g) \/ {z}) by A18, NAT_1:44;
then A22: card (Roots f) <= (card (Roots g)) + 1 by A21, XXREAL_0:2;
(card (Roots g)) + 1 <= k + 1 by A17, XREAL_1:8;
hence ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) by A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A8);
hence for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n ) ; :: thesis: verum