Theorem coeidp

Description: The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	coeidp	$$⊢A\in {\mathbb{N}}_0\to \mathrm{coeff}\left(X^p\right)\left(A\right)=if\left(A=1,1,0\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{ℂ}=\left(z\in ℂ⟼z\right)$$
4		df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$
5		exp1	$$⊢z\in ℂ\to z^1=z$$
6	5	oveq2d	$$⊢z\in ℂ\to 1z^1=1z$$
7		mullid	$$⊢z\in ℂ\to 1z=z$$
8	6 7	eqtrd	$$⊢z\in ℂ\to 1z^1=z$$
9	8	mpteq2ia	$$⊢\left(z\in ℂ⟼1z^1\right)=\left(z\in ℂ⟼z\right)$$
10	3 4 9	3eqtr4i	$$⊢X^p=\left(z\in ℂ⟼1z^1\right)$$
11	10	coe1term	$$⊢\left(1\in ℂ\wedge 1\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(X^p\right)\left(A\right)=if\left(A=1,1,0\right)$$
12	1 2 11	mp3an12	$$⊢A\in {\mathbb{N}}_0\to \mathrm{coeff}\left(X^p\right)\left(A\right)=if\left(A=1,1,0\right)$$