Theorem dgreq

Description: If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	dgreq.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	dgreq.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	dgreq.3	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
	dgreq.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
	dgreq.5	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
	dgreq.6	$$⊢\phi \to A\left(N\right)\ne 0$$
Assertion	dgreq	$$⊢\phi \to \mathrm{deg}\left(F\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		dgreq.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
2		dgreq.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		dgreq.3	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
4		dgreq.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
5		dgreq.5	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
6		dgreq.6	$$⊢\phi \to A\left(N\right)\ne 0$$
7		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_0$$
8		ffvelrn	$$⊢\left(A:{\mathbb{N}}_0⟶ℂ\wedge k\in {\mathbb{N}}_0\right)\to A\left(k\right)\in ℂ$$
9	3 7 8	syl2an	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to A\left(k\right)\in ℂ$$
10	1 2 9 5	dgrle	$$⊢\phi \to \mathrm{deg}\left(F\right)\le N$$
11	1 2 3 4 5	coeeq	$$⊢\phi \to \mathrm{coeff}\left(F\right)=A$$
12	11	fveq1d	$$⊢\phi \to \mathrm{coeff}\left(F\right)\left(N\right)=A\left(N\right)$$
13	12 6	eqnetrd	$$⊢\phi \to \mathrm{coeff}\left(F\right)\left(N\right)\ne 0$$
14		eqid	$$⊢\mathrm{coeff}\left(F\right)=\mathrm{coeff}\left(F\right)$$
15		eqid	$$⊢\mathrm{deg}\left(F\right)=\mathrm{deg}\left(F\right)$$
16	14 15	dgrub	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(F\right)\left(N\right)\ne 0\right)\to N\le \mathrm{deg}\left(F\right)$$
17	1 2 13 16	syl3anc	$$⊢\phi \to N\le \mathrm{deg}\left(F\right)$$
18		dgrcl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)\in {\mathbb{N}}_0$$
19	1 18	syl	$$⊢\phi \to \mathrm{deg}\left(F\right)\in {\mathbb{N}}_0$$
20	19	nn0red	$$⊢\phi \to \mathrm{deg}\left(F\right)\in ℝ$$
21	2	nn0red	$$⊢\phi \to N\in ℝ$$
22	20 21	letri3d	$$⊢\phi \to \left(\mathrm{deg}\left(F\right)=N\leftrightarrow \left(\mathrm{deg}\left(F\right)\le N\wedge N\le \mathrm{deg}\left(F\right)\right)\right)$$
23	10 17 22	mpbir2and	$$⊢\phi \to \mathrm{deg}\left(F\right)=N$$