# 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 ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({F}\right)\in {ℕ}_{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],{ℕ}_{0},<\right)$
3 nn0ssre ${⊢}{ℕ}_{0}\subseteq ℝ$
4 ltso ${⊢}<\mathrm{Or}ℝ$
5 soss ${⊢}{ℕ}_{0}\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}{ℕ}_{0}\right)$
6 3 4 5 mp2 ${⊢}<\mathrm{Or}{ℕ}_{0}$
7 6 a1i ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to <\mathrm{Or}{ℕ}_{0}$
8 0zd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to 0\in ℤ$
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):{ℕ}_{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 {ℕ}_{0}$
12 1 dgrlem ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left(\mathrm{coeff}\left({F}\right):{ℕ}_{0}⟶{S}\cup \left\{0\right\}\wedge \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{x}\le {n}\right)$
13 12 simprd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{x}\le {n}$
14 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
15 14 uzsupss ${⊢}\left(0\in ℤ\wedge {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq {ℕ}_{0}\wedge \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{x}\le {n}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}¬{n}<{x}\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({x}<{n}\to \exists {y}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)$
16 8 11 13 15 syl3anc ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}¬{n}<{x}\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({x}<{n}\to \exists {y}\in {\mathrm{coeff}\left({F}\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{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],{ℕ}_{0},<\right)\in {ℕ}_{0}$
18 2 17 eqeltrd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({F}\right)\in {ℕ}_{0}$