Theorem coe1termlem

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

	Ref	Expression
Hypothesis	coe1term.1	$$⊢F=\left(z\in ℂ⟼A{z}^N\right)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		coe1term.1	$$⊢F=\left(z\in ℂ⟼A{z}^N\right)$$
2		ssid	$$⊢ℂ\subseteq ℂ$$
3	1	ply1term	$$⊢\left(ℂ\subseteq ℂ\wedge A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
4	2 3	mp3an1	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
5		simpr	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
6		simpl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A\in ℂ$$
7		0cn	$$⊢0\in ℂ$$
8		ifcl	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to if\left(n=N,A,0\right)\in ℂ$$
9	6 7 8	sylancl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to if\left(n=N,A,0\right)\in ℂ$$
10	9	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to if\left(n=N,A,0\right)\in ℂ$$
11	10	fmpttd	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right):{\mathbb{N}}_0⟶ℂ$$
12		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)$$
13		eqeq1	$$⊢n=k\to \left(n=N\leftrightarrow k=N\right)$$
14	13	ifbid	$$⊢n=k\to if\left(n=N,A,0\right)=if\left(k=N,A,0\right)$$
15		simpr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
16		ifcl	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to if\left(k=N,A,0\right)\in ℂ$$
17	6 7 16	sylancl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to if\left(k=N,A,0\right)\in ℂ$$
18	17	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to if\left(k=N,A,0\right)\in ℂ$$
19	12 14 15 18	fvmptd3	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)=if\left(k=N,A,0\right)$$
20	19	neeq1d	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)\ne 0\leftrightarrow if\left(k=N,A,0\right)\ne 0\right)$$
21		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
22	21	leidd	$$⊢N\in {\mathbb{N}}_0\to N\le N$$
23	22	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to N\le N$$
24		iffalse	$$⊢\neg k=N\to if\left(k=N,A,0\right)=0$$
25	24	necon1ai	$$⊢if\left(k=N,A,0\right)\ne 0\to k=N$$
26	25	breq1d	$$⊢if\left(k=N,A,0\right)\ne 0\to \left(k\le N\leftrightarrow N\le N\right)$$
27	23 26	syl5ibrcom	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(if\left(k=N,A,0\right)\ne 0\to k\le N\right)$$
28	20 27	sylbid	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)$$
29	28	ralrimiva	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \forall k\in {\mathbb{N}}_0\left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)$$
30		plyco0	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right):{\mathbb{N}}_0⟶ℂ\right)\to \left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall k\in {\mathbb{N}}_0\left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)\right)$$
31	5 11 30	syl2anc	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall k\in {\mathbb{N}}_0\left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)\right)$$
32	29 31	mpbird	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
33	1	ply1termlem	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^{N}if\left(k=N,A,0\right)z^k\right)$$
34		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_0$$
35	19	oveq1d	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k=if\left(k=N,A,0\right)z^k$$
36	34 35	sylan2	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots N\right)\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k=if\left(k=N,A,0\right)z^k$$
37	36	sumeq2dv	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \sum _{k=0}^N\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k=\sum _{k=0}^{N}if\left(k=N,A,0\right)z^k$$
38	37	mpteq2dv	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(z\in ℂ⟼\sum _{k=0}^N\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{N}if\left(k=N,A,0\right)z^k\right)$$
39	33 38	eqtr4d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^N\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k\right)$$
40	4 5 11 32 39	coeeq	$$⊢\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)$$
41	4	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
42	5	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to N\in {\mathbb{N}}_0$$
43	11	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right):{\mathbb{N}}_0⟶ℂ$$
44	32	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
45	39	adantr	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^N\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(k\right)z^k\right)$$
46		iftrue	$$⊢n=N\to if\left(n=N,A,0\right)=A$$
47	46 12	fvmptg	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℂ\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(N\right)=A$$
48	47	ancoms	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(N\right)=A$$
49	48	neeq1d	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(N\right)\ne 0\leftrightarrow A\ne 0\right)$$
50	49	biimpar	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to \left(n\in {\mathbb{N}}_0⟼if\left(n=N,A,0\right)\right)\left(N\right)\ne 0$$
51	41 42 43 44 45 50	dgreq	$$⊢\left(\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\wedge A\ne 0\right)\to \mathrm{deg}\left(F\right)=N$$
52	51	ex	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \left(A\ne 0\to \mathrm{deg}\left(F\right)=N\right)$$
53	40 52	jca	$$⊢\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)$$