Theorem coeeq2

Description: Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	dgrle.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	dgrle.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	dgrle.3	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to A\in ℂ$$
	dgrle.4	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A{z}^k\right)$$
Assertion	coeeq2	$$⊢\phi \to \mathrm{coeff}\left(F\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dgrle.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
2		dgrle.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		dgrle.3	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to A\in ℂ$$
4		dgrle.4	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A{z}^k\right)$$
5		simpll	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to \phi$$
6		simpr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to k\le N$$
7		simplr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to k\in {\mathbb{N}}_0$$
8		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
9	7 8	eleqtrdi	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to k\in {\mathbb{Z}}_{\ge 0}$$
10	2	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
11	10	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to N\in \mathbb{Z}$$
12		elfz5	$$⊢\left(k\in {\mathbb{Z}}_{\ge 0}\wedge N\in \mathbb{Z}\right)\to \left(k\in \left(0\dots N\right)\leftrightarrow k\le N\right)$$
13	9 11 12	syl2anc	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to \left(k\in \left(0\dots N\right)\leftrightarrow k\le N\right)$$
14	6 13	mpbird	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to k\in \left(0\dots N\right)$$
15	5 14 3	syl2anc	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\le N\right)\to A\in ℂ$$
16		0cnd	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \neg k\le N\right)\to 0\in ℂ$$
17	15 16	ifclda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k\le N,A,0\right)\in ℂ$$
18	17	fmpttd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right):{\mathbb{N}}_0⟶ℂ$$
19		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
20		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$
21	20	fvmpt2	$$⊢\left(k\in {\mathbb{N}}_0\wedge if\left(k\le N,A,0\right)\in ℂ\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=if\left(k\le N,A,0\right)$$
22	19 17 21	syl2anc	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=if\left(k\le N,A,0\right)$$
23	22	neeq1d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\leftrightarrow if\left(k\le N,A,0\right)\ne 0\right)$$
24		iffalse	$$⊢\neg k\le N\to if\left(k\le N,A,0\right)=0$$
25	24	necon1ai	$$⊢if\left(k\le N,A,0\right)\ne 0\to k\le N$$
26	23 25	biimtrdi	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)$$
27	26	ralrimiva	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)$$
28		nfv	$$⊢Ⅎm\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)$$
29		nffvmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}k0$$
31	29 30	nfne	$$⊢Ⅎk\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0$$
32		nfv	$$⊢Ⅎkm\le N$$
33	31 32	nfim	$$⊢Ⅎk\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)$$
34		fveq2	$$⊢k=m\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)$$
35	34	neeq1d	$$⊢k=m\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\leftrightarrow \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\right)$$
36		breq1	$$⊢k=m\to \left(k\le N\leftrightarrow m\le N\right)$$
37	35 36	imbi12d	$$⊢k=m\to \left(\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)\leftrightarrow \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)\right)$$
38	28 33 37	cbvralw	$$⊢\forall k\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)\ne 0\to k\le N\right)\leftrightarrow \forall m\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)$$
39	27 38	sylib	$$⊢\phi \to \forall m\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)$$
40		plyco0	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right):{\mathbb{N}}_0⟶ℂ\right)\to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall m\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)\right)$$
41	2 18 40	syl2anc	$$⊢\phi \to \left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\leftrightarrow \forall m\in {\mathbb{N}}_0\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)\ne 0\to m\le N\right)\right)$$
42	39 41	mpbird	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
43		oveq2	$$⊢k=m\to z^k=z^m$$
44	34 43	oveq12d	$$⊢k=m\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)z^k=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m$$
45		nfcv	$$⊢\underset{\_}{Ⅎ}m\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)z^k$$
46		nfcv	$$⊢\underset{\_}{Ⅎ}k\times$$
47		nfcv	$$⊢\underset{\_}{Ⅎ}k{z}^m$$
48	29 46 47	nfov	$$⊢\underset{\_}{Ⅎ}k\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m$$
49	44 45 48	cbvsum	$$⊢\sum _{k=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)z^k=\sum _{m=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m$$
50		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_0$$
51	50	adantl	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to k\in {\mathbb{N}}_0$$
52		elfzle2	$$⊢k\in \left(0\dots N\right)\to k\le N$$
53	52	adantl	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to k\le N$$
54	53	iftrued	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to if\left(k\le N,A,0\right)=A$$
55	3	adantlr	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to A\in ℂ$$
56	54 55	eqeltrd	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to if\left(k\le N,A,0\right)\in ℂ$$
57	51 56 21	syl2anc	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=if\left(k\le N,A,0\right)$$
58	57 54	eqtrd	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)=A$$
59	58	oveq1d	$$⊢\left(\left(\phi \wedge z\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)z^k=A{z}^k$$
60	59	sumeq2dv	$$⊢\left(\phi \wedge z\in ℂ\right)\to \sum _{k=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(k\right)z^k=\sum _{k=0}^{N}A{z}^k$$
61	49 60	eqtr3id	$$⊢\left(\phi \wedge z\in ℂ\right)\to \sum _{m=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m=\sum _{k=0}^{N}A{z}^k$$
62	61	mpteq2dva	$$⊢\phi \to \left(z\in ℂ⟼\sum _{m=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m\right)=\left(z\in ℂ⟼\sum _{k=0}^{N}A{z}^k\right)$$
63	4 62	eqtr4d	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{m=0}^N\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)\left(m\right)z^m\right)$$
64	1 2 18 42 63	coeeq	$$⊢\phi \to \mathrm{coeff}\left(F\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\le N,A,0\right)\right)$$