Theorem dgrub2

Description: All the coefficients above the degree of F are zero. (Contributed by Mario Carneiro, 23-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
	dgrub.2	$$⊢N=\mathrm{deg}\left(F\right)$$
Assertion	dgrub2	$$⊢F\in \mathrm{Poly}\left(S\right)\to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		dgrub.2	$$⊢N=\mathrm{deg}\left(F\right)$$
3	1 2	dgrub	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge k\in {\mathbb{N}}_0\wedge A\left(k\right)\ne 0\right)\to k\le N$$
4	3	3expia	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(A\left(k\right)\ne 0\to k\le N\right)$$
5	4	ralrimiva	$$⊢F\in \mathrm{Poly}\left(S\right)\to \forall k\in {\mathbb{N}}_0\left(A\left(k\right)\ne 0\to k\le N\right)$$
6		dgrcl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)\in {\mathbb{N}}_0$$
7	2 6	eqeltrid	$$⊢F\in \mathrm{Poly}\left(S\right)\to N\in {\mathbb{N}}_0$$
8	1	coef3	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶ℂ$$
9		plyco0	$$⊢\left(N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶ℂ\right)\to \left(A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall k\in {\mathbb{N}}_0\left(A\left(k\right)\ne 0\to k\le N\right)\right)$$
10	7 8 9	syl2anc	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall k\in {\mathbb{N}}_0\left(A\left(k\right)\ne 0\to k\le N\right)\right)$$
11	5 10	mpbird	$$⊢F\in \mathrm{Poly}\left(S\right)\to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$