let R be domRing; :: thesis: for p being non zero Polynomial of R ex n being natural number st

( n = card (Roots p) & n <= deg p )

let p be non zero Polynomial of R; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

defpred S_{1}[ Nat] means for p being non zero Polynomial of R st deg p = $1 holds

ex n being natural number st

( n = card (Roots p) & n <= deg p );

IA: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(IA, IS);

p <> 0_. R ;

then deg p is Element of NAT by T8;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by I; :: thesis: verum

( n = card (Roots p) & n <= deg p )

let p be non zero Polynomial of R; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

defpred S

ex n being natural number st

( n = card (Roots p) & n <= deg p );

IA: S

proof

let p be non zero Polynomial of R; :: thesis: ( deg p = 0 implies ex n being natural number st

( n = card (Roots p) & n <= deg p ) )

assume A1: deg p = 0 ; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

reconsider q = p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

consider a being Element of R such that

A2: q = a | R by A1, RING_4:def 4, RING_4:20;

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

end;( n = card (Roots p) & n <= deg p ) )

assume A1: deg p = 0 ; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

reconsider q = p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

consider a being Element of R such that

A2: q = a | R by A1, RING_4:def 4, RING_4:20;

now :: thesis: ( Roots p <> {} implies for u being Element of Roots p holds contradiction )

hence
ex n being natural number st assume A3:
Roots p <> {}
; :: thesis: for u being Element of Roots p holds contradiction

let u be Element of Roots p; :: thesis: contradiction

u in Roots p by A3;

then reconsider u = u as Element of R ;

u is_a_root_of p by A3, POLYNOM5:def 10;

then eval (p,u) = 0. R by POLYNOM5:def 7;

then a = 0. R by A2, evconst;

hence contradiction by A2; :: thesis: verum

end;let u be Element of Roots p; :: thesis: contradiction

u in Roots p by A3;

then reconsider u = u as Element of R ;

u is_a_root_of p by A3, POLYNOM5:def 10;

then eval (p,u) = 0. R by POLYNOM5:def 7;

then a = 0. R by A2, evconst;

hence contradiction by A2; :: thesis: verum

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

IS: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

I:
for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume IV: S

now :: thesis: for p being non zero Polynomial of R st deg p = k + 1 holds

ex n being natural number st

( n = card (Roots p) & n <= deg p )

hence
Sex n being natural number st

( n = card (Roots p) & n <= deg p )

let p be non zero Polynomial of R; :: thesis: ( deg p = k + 1 implies ex n being natural number st

( b_{2} = card (Roots n) & b_{2} <= deg n ) )

assume A1: deg p = k + 1 ; :: thesis: ex n being natural number st

( b_{2} = card (Roots n) & b_{2} <= deg n )

end;( b

assume A1: deg p = k + 1 ; :: thesis: ex n being natural number st

( b

per cases
( ex x being Element of R st x is_a_root_of p or for x being Element of R holds not x is_a_root_of p )
;

end;

suppose
ex x being Element of R st x is_a_root_of p
; :: thesis: ex n being natural number st

( b_{2} = card (Roots n) & b_{2} <= deg n )

( b

then consider x being Element of R such that

A2: x is_a_root_of p ;

consider q being Polynomial of R such that

A3: p = (rpoly (1,x)) *' q by A2, HURWITZ:33;

A4: q <> 0_. R by A3;

reconsider q = q as non zero Polynomial of R by A3;

A7: deg p = (deg q) + (deg (rpoly (1,x))) by HURWITZ:23, A3, A4

.= (deg q) + 1 by HURWITZ:27 ;

then consider m being natural number such that

A5: ( m = card (Roots q) & m <= deg q ) by A1, IV;

reconsider RQ = Roots q as finite Subset of R ;

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

end;A2: x is_a_root_of p ;

consider q being Polynomial of R such that

A3: p = (rpoly (1,x)) *' q by A2, HURWITZ:33;

A4: q <> 0_. R by A3;

reconsider q = q as non zero Polynomial of R by A3;

A7: deg p = (deg q) + (deg (rpoly (1,x))) by HURWITZ:23, A3, A4

.= (deg q) + 1 by HURWITZ:27 ;

then consider m being natural number such that

A5: ( m = card (Roots q) & m <= deg q ) by A1, IV;

reconsider RQ = Roots q as finite Subset of R ;

now :: thesis: ( ( x in Roots q & ex n being natural number st

( n = card (Roots p) & n <= deg p ) ) or ( not x in Roots q & ex n being natural number st

( n = card (Roots p) & n <= deg p ) ) )end;

hence
ex n being natural number st ( n = card (Roots p) & n <= deg p ) ) or ( not x in Roots q & ex n being natural number st

( n = card (Roots p) & n <= deg p ) ) )

per cases
( x in Roots q or not x in Roots q )
;

end;

case
x in Roots q
; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

( n = card (Roots p) & n <= deg p )

then
for o being object st o in {x} holds

o in Roots q by TARSKI:def 1;

then A6: card (RQ \/ {x}) = m by A5, XBOOLE_1:12, TARSKI:def 3;

Roots (rpoly (1,x)) = {x} by ro4;

then A8: card (Roots p) = m by A3, A6, UPROOTS:23;

deg q <= (deg q) + 1 by NAT_1:11;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by A7, A8, A5, XXREAL_0:2; :: thesis: verum

end;o in Roots q by TARSKI:def 1;

then A6: card (RQ \/ {x}) = m by A5, XBOOLE_1:12, TARSKI:def 3;

Roots (rpoly (1,x)) = {x} by ro4;

then A8: card (Roots p) = m by A3, A6, UPROOTS:23;

deg q <= (deg q) + 1 by NAT_1:11;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by A7, A8, A5, XXREAL_0:2; :: thesis: verum

case
not x in Roots q
; :: thesis: ex n being natural number st

( n = card (Roots p) & n <= deg p )

( n = card (Roots p) & n <= deg p )

then A6:
card (RQ \/ {x}) = m + 1
by A5, CARD_2:41;

Roots (rpoly (1,x)) = {x} by ro4;

then card (Roots p) = m + 1 by A3, A6, UPROOTS:23;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by A7, A5, XREAL_1:6; :: thesis: verum

end;Roots (rpoly (1,x)) = {x} by ro4;

then card (Roots p) = m + 1 by A3, A6, UPROOTS:23;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by A7, A5, XREAL_1:6; :: thesis: verum

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

suppose A2:
for x being Element of R holds not x is_a_root_of p
; :: thesis: ex n being natural number st

( b_{2} = card (Roots n) & b_{2} <= deg n )

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

end;

( b

now :: thesis: ( Roots p <> {} implies for x being Element of Roots p holds contradiction )

hence
ex n being natural number st assume A3:
Roots p <> {}
; :: thesis: for x being Element of Roots p holds contradiction

let x be Element of Roots p; :: thesis: contradiction

x in Roots p by A3;

then reconsider x = x as Element of R ;

x is_a_root_of p by A3, POLYNOM5:def 10;

hence contradiction by A2; :: thesis: verum

end;let x be Element of Roots p; :: thesis: contradiction

x in Roots p by A3;

then reconsider x = x as Element of R ;

x is_a_root_of p by A3, POLYNOM5:def 10;

hence contradiction by A2; :: thesis: verum

( n = card (Roots p) & n <= deg p ) ; :: thesis: verum

p <> 0_. R ;

then deg p is Element of NAT by T8;

hence ex n being natural number st

( n = card (Roots p) & n <= deg p ) by I; :: thesis: verum