let R be domRing; :: thesis: for p being non zero Polynomial of R holds card (BRoots p) <= deg p

let p be non zero Polynomial of R; :: thesis: card (BRoots p) <= deg p

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

card (BRoots p) <= 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 card (BRoots p) <= deg p by I; :: thesis: verum

let p be non zero Polynomial of R; :: thesis: card (BRoots p) <= deg p

defpred S

card (BRoots p) <= deg p;

IA: S

proof

let p be non zero Polynomial of R; :: thesis: ( deg p = 0 implies card (BRoots p) <= deg p )

assume A1: deg p = 0 ; :: thesis: card (BRoots p) <= 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;

a <> 0. R by A2;

then reconsider a = a as non zero Element of R by STRUCT_0:def 12;

q = a | R by A2;

hence card (BRoots p) <= deg p by bag1; :: thesis: verum

end;assume A1: deg p = 0 ; :: thesis: card (BRoots p) <= 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;

a <> 0. R by A2;

then reconsider a = a as non zero Element of R by STRUCT_0:def 12;

q = a | R by A2;

hence card (BRoots p) <= deg p by bag1; :: 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

card (BRoots p) <= deg p

hence
Scard (BRoots p) <= deg p

let p be non zero Polynomial of R; :: thesis: ( deg p = k + 1 implies card (BRoots b_{1}) <= deg b_{1} )

assume A1: deg p = k + 1 ; :: thesis: card (BRoots b_{1}) <= deg b_{1}

end;assume A1: deg p = k + 1 ; :: thesis: card (BRoots 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: card (BRoots b_{1}) <= deg b_{1}

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;

BRoots p = (BRoots (rpoly (1,x))) + (BRoots q) by A3, UPROOTS:56;

then A6: card (BRoots p) = (card (BRoots (rpoly (1,x)))) + (card (BRoots q)) by UPROOTS:15

.= 1 + (card (BRoots q)) by bag2 ;

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

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

hence card (BRoots p) <= deg p by IV, A1, A6, XREAL_1:6; :: 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;

BRoots p = (BRoots (rpoly (1,x))) + (BRoots q) by A3, UPROOTS:56;

then A6: card (BRoots p) = (card (BRoots (rpoly (1,x)))) + (card (BRoots q)) by UPROOTS:15

.= 1 + (card (BRoots q)) by bag2 ;

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

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

hence card (BRoots p) <= deg p by IV, A1, A6, XREAL_1:6; :: thesis: verum

suppose A2:
for x being Element of R holds not x is_a_root_of p
; :: thesis: card (BRoots b_{1}) <= deg b_{1}

hence card (BRoots p) <= deg p by bag1a; :: thesis: verum

end;

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

then
support (BRoots p) = {}
by UPROOTS:def 9;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

hence card (BRoots p) <= deg p by bag1a; :: thesis: verum

p <> 0_. R ;

then deg p is Element of NAT by T8;

hence card (BRoots p) <= deg p by I; :: thesis: verum