Theorem dgr1term

Description: The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypothesis	coe1term.1	$$⊢F=\left(z\in ℂ⟼A{z}^N\right)$$
Assertion	dgr1term	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{deg}\left(F\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		coe1term.1	$$⊢F=\left(z\in ℂ⟼A{z}^N\right)$$
2	1	coe1termlem	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(\mathrm{coeff}\left(F\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\wedge \left(A\ne 0\to \mathrm{deg}\left(F\right)=N\right)\right)$$
3	2	simprd	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(A\ne 0\to \mathrm{deg}\left(F\right)=N\right)$$
4	3	3impia	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge A\ne 0\right)\to \mathrm{deg}\left(F\right)=N$$
5	4	3com23	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{deg}\left(F\right)=N$$