Theorem coe1term

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

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

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	simpld	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)$$
4	3	fveq1d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)\left(M\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(M\right)$$
5	4	3adant3	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)\left(M\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(M\right)$$
6		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)$$
7		eqeq1	$$⊢n=M\to \left(n=N\leftrightarrow M=N\right)$$
8	7	ifbid	$$⊢n=M\to if\left(n=N,A,0\right)=if\left(M=N,A,0\right)$$
9		simp3	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to M\in {\mathbb{N}}_0$$
10		simp1	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to A\in ℂ$$
11		0cn	$$⊢0\in ℂ$$
12		ifcl	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to if\left(M=N,A,0\right)\in ℂ$$
13	10 11 12	sylancl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to if\left(M=N,A,0\right)\in ℂ$$
14	6 8 9 13	fvmptd3	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(M\right)=if\left(M=N,A,0\right)$$
15	5 14	eqtrd	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)\left(M\right)=if\left(M=N,A,0\right)$$