Theorem dgrle

Description: Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	dgrle.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	dgrle.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	dgrle.3	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to A\in ℂ$$
	dgrle.4	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A{z}^k\right)$$
Assertion	dgrle	$$⊢\phi \to \mathrm{deg}\left(F\right)\le N$$

Proof

Step	Hyp	Ref	Expression
1		dgrle.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
2		dgrle.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		dgrle.3	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to A\in ℂ$$
4		dgrle.4	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A{z}^k\right)$$
5	1 2 3 4	coeeq2	$$⊢\phi \to \mathrm{coeff}\left(F\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$
6	5	ad2antrr	$$⊢\left(\left(\phi \wedge m\in {\mathbb{N}}_0\right)\wedge \neg m\le N\right)\to \mathrm{coeff}\left(F\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$
7	6	fveq1d	$$⊢\left(\left(\phi \wedge m\in {\mathbb{N}}_0\right)\wedge \neg m\le N\right)\to \mathrm{coeff}\left(F\right)\left(m\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}km$$
9		nfv	$$⊢Ⅎk\neg m\le N$$
10		nffvmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)$$
11	10	nfeq1	$$⊢Ⅎk\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0$$
12	9 11	nfim	$$⊢Ⅎk\left(\neg m\le N\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0\right)$$
13		breq1	$$⊢k=m\to \left(k\le N\leftrightarrow m\le N\right)$$
14	13	notbid	$$⊢k=m\to \left(\neg k\le N\leftrightarrow \neg m\le N\right)$$
15		fveqeq2	$$⊢k=m\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=0\leftrightarrow \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0\right)$$
16	14 15	imbi12d	$$⊢k=m\to \left(\left(\neg k\le N\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=0\right)\leftrightarrow \left(\neg m\le N\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0\right)\right)$$
17		iffalse	$$⊢\neg k\le N\to if\left(k\le N,A,0\right)=0$$
18	17	fveq2d	$$⊢\neg k\le N\to \mathrm{I}\left(if\left(k\le N,A,0\right)\right)=\mathrm{I}\left(0\right)$$
19		0cn	$$⊢0\in ℂ$$
20		fvi	$$⊢0\in ℂ\to \mathrm{I}\left(0\right)=0$$
21	19 20	ax-mp	$$⊢\mathrm{I}\left(0\right)=0$$
22	18 21	eqtrdi	$$⊢\neg k\le N\to \mathrm{I}\left(if\left(k\le N,A,0\right)\right)=0$$
23		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$
24	23	fvmpt2i	$$⊢k\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=\mathrm{I}\left(if\left(k\le N,A,0\right)\right)$$
25	24	eqeq1d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=0\leftrightarrow \mathrm{I}\left(if\left(k\le N,A,0\right)\right)=0\right)$$
26	22 25	imbitrrid	$$⊢k\in {\mathbb{N}}_0\to \left(\neg k\le N\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=0\right)$$
27	8 12 16 26	vtoclgaf	$$⊢m\in {\mathbb{N}}_0\to \left(\neg m\le N\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0\right)$$
28	27	imp	$$⊢\left(m\in {\mathbb{N}}_0\wedge \neg m\le N\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0$$
29	28	adantll	$$⊢\left(\left(\phi \wedge m\in {\mathbb{N}}_0\right)\wedge \neg m\le N\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)=0$$
30	7 29	eqtrd	$$⊢\left(\left(\phi \wedge m\in {\mathbb{N}}_0\right)\wedge \neg m\le N\right)\to \mathrm{coeff}\left(F\right)\left(m\right)=0$$
31	30	ex	$$⊢\left(\phi \wedge m\in {\mathbb{N}}_0\right)\to \left(\neg m\le N\to \mathrm{coeff}\left(F\right)\left(m\right)=0\right)$$
32	31	necon1ad	$$⊢\left(\phi \wedge m\in {\mathbb{N}}_0\right)\to \left(\mathrm{coeff}\left(F\right)\left(m\right)\ne 0\to m\le N\right)$$
33	32	ralrimiva	$$⊢\phi \to \forall m\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left(m\right)\ne 0\to m\le N\right)$$
34		eqid	$$⊢\mathrm{coeff}\left(F\right)=\mathrm{coeff}\left(F\right)$$
35	34	coef3	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{coeff}\left(F\right):{\mathbb{N}}_0⟶ℂ$$
36	1 35	syl	$$⊢\phi \to \mathrm{coeff}\left(F\right):{\mathbb{N}}_0⟶ℂ$$
37		plyco0	$$⊢\left(N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(F\right):{\mathbb{N}}_0⟶ℂ\right)\to \left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall m\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left(m\right)\ne 0\to m\le N\right)\right)$$
38	2 36 37	syl2anc	$$⊢\phi \to \left(\mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall m\in {\mathbb{N}}_0\left(\mathrm{coeff}\left(F\right)\left(m\right)\ne 0\to m\le N\right)\right)$$
39	33 38	mpbird	$$⊢\phi \to \mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
40		eqid	$$⊢\mathrm{deg}\left(F\right)=\mathrm{deg}\left(F\right)$$
41	34 40	dgrlb	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(F\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\right)\to \mathrm{deg}\left(F\right)\le N$$
42	1 2 39 41	syl3anc	$$⊢\phi \to \mathrm{deg}\left(F\right)\le N$$