Metamath Proof Explorer


Theorem dgrcl

Description: The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion dgrcl FPolySdegF0

Proof

Step Hyp Ref Expression
1 eqid coeffF=coeffF
2 1 dgrval FPolySdegF=supcoeffF-100<
3 nn0ssre 0
4 ltso <Or
5 soss 0<Or<Or0
6 3 4 5 mp2 <Or0
7 6 a1i FPolyS<Or0
8 0zd FPolyS0
9 cnvimass coeffF-10domcoeffF
10 1 coef FPolyScoeffF:0S0
11 9 10 fssdm FPolyScoeffF-100
12 1 dgrlem FPolyScoeffF:0S0nxcoeffF-10xn
13 12 simprd FPolySnxcoeffF-10xn
14 nn0uz 0=0
15 14 uzsupss 0coeffF-100nxcoeffF-10xnn0xcoeffF-10¬n<xx0x<nycoeffF-10x<y
16 8 11 13 15 syl3anc FPolySn0xcoeffF-10¬n<xx0x<nycoeffF-10x<y
17 7 16 supcl FPolySsupcoeffF-100<0
18 2 17 eqeltrd FPolySdegF0