Theorem dgrcl

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

	Ref	Expression
Assertion	dgrcl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{coeff}\left(F\right)=\mathrm{coeff}\left(F\right)$$
2	1	dgrval	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)=sup\left({\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$
3		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
4		ltso	$$⊢<\mathrm{Or}ℝ$$
5		soss	$$⊢{\mathbb{N}}_0\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}{\mathbb{N}}_0\right)$$
6	3 4 5	mp2	$$⊢<\mathrm{Or}{\mathbb{N}}_0$$
7	6	a1i	$$⊢F\in \mathrm{Poly}\left(S\right)\to <\mathrm{Or}{\mathbb{N}}_0$$
8		0zd	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0\in \mathbb{Z}$$
9		cnvimass	$$⊢{\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq \mathrm{dom}\mathrm{coeff}\left(F\right)$$
10	1	coef	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{coeff}\left(F\right):{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
11	9 10	fssdm	$$⊢F\in \mathrm{Poly}\left(S\right)\to {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq {\mathbb{N}}_0$$
12	1	dgrlem	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(\mathrm{coeff}\left(F\right):{\mathbb{N}}_0⟶S\cup \left\{0\right\}\wedge \exists n\in \mathbb{Z}\forall x\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]x\le n\right)$$
13	12	simprd	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists n\in \mathbb{Z}\forall x\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]x\le n$$
14		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
15	14	uzsupss	$$⊢\left(0\in \mathbb{Z}\wedge {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq {\mathbb{N}}_0\wedge \exists n\in \mathbb{Z}\forall x\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]x\le n\right)\to \exists n\in {\mathbb{N}}_0\left(\forall x\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\neg n<x\wedge \forall x\in {\mathbb{N}}_0\left(x<n\to \exists y\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]x<y\right)\right)$$
16	8 11 13 15	syl3anc	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists n\in {\mathbb{N}}_0\left(\forall x\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\neg n<x\wedge \forall x\in {\mathbb{N}}_0\left(x<n\to \exists y\in {\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]x<y\right)\right)$$
17	7 16	supcl	$$⊢F\in \mathrm{Poly}\left(S\right)\to sup\left({\mathrm{coeff}\left(F\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\in {\mathbb{N}}_0$$
18	2 17	eqeltrd	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)\in {\mathbb{N}}_0$$