Theorem coeeu

Description: Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	coeeu	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
2	1	sseli	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
3		elply2	$$⊢F\in \mathrm{Poly}\left(ℂ\right)\leftrightarrow \left(ℂ\subseteq ℂ\wedge \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)$$
4	3	simprbi	$$⊢F\in \mathrm{Poly}\left(ℂ\right)\to \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
5		rexcom	$$⊢\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
6	4 5	sylib	$$⊢F\in \mathrm{Poly}\left(ℂ\right)\to \exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
7	2 6	syl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
8		0cn	$$⊢0\in ℂ$$
9		snssi	$$⊢0\in ℂ\to \left\{0\right\}\subseteq ℂ$$
10	8 9	ax-mp	$$⊢\left\{0\right\}\subseteq ℂ$$
11		ssequn2	$$⊢\left\{0\right\}\subseteq ℂ\leftrightarrow ℂ\cup \left\{0\right\}=ℂ$$
12	10 11	mpbi	$$⊢ℂ\cup \left\{0\right\}=ℂ$$
13	12	oveq1i	$$⊢{\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}={ℂ}^{{\mathbb{N}}_0}$$
14	13	rexeqi	$$⊢\exists a\in \left({\left(ℂ\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
15	7 14	sylib	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
16		reeanv	$$⊢\exists n\in {\mathbb{N}}_0\exists m\in {\mathbb{N}}_0\left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)$$
17		simp1l	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to F\in \mathrm{Poly}\left(S\right)$$
18		simp1rl	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to a\in \left({ℂ}^{{\mathbb{N}}_0}\right)$$
19		simp1rr	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to b\in \left({ℂ}^{{\mathbb{N}}_0}\right)$$
20		simp2l	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to n\in {\mathbb{N}}_0$$
21		simp2r	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to m\in {\mathbb{N}}_0$$
22		simp3ll	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}$$
23		simp3rl	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}$$
24		simp3lr	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
25		oveq1	$$⊢z=w\to z^k=w^k$$
26	25	oveq2d	$$⊢z=w\to a\left(k\right)z^k=a\left(k\right)w^k$$
27	26	sumeq2sdv	$$⊢z=w\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{k=0}^{n}a\left(k\right)w^k$$
28		fveq2	$$⊢k=j\to a\left(k\right)=a\left(j\right)$$
29		oveq2	$$⊢k=j\to w^k=w^j$$
30	28 29	oveq12d	$$⊢k=j\to a\left(k\right)w^k=a\left(j\right)w^j$$
31	30	cbvsumv	$$⊢\sum _{k=0}^{n}a\left(k\right)w^k=\sum _{j=0}^{n}a\left(j\right)w^j$$
32	27 31	eqtrdi	$$⊢z=w\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{j=0}^{n}a\left(j\right)w^j$$
33	32	cbvmptv	$$⊢\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)=\left(w\in ℂ⟼\sum _{j=0}^{n}a\left(j\right)w^j\right)$$
34	24 33	eqtrdi	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to F=\left(w\in ℂ⟼\sum _{j=0}^{n}a\left(j\right)w^j\right)$$
35		simp3rr	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)$$
36	25	oveq2d	$$⊢z=w\to b\left(k\right)z^k=b\left(k\right)w^k$$
37	36	sumeq2sdv	$$⊢z=w\to \sum _{k=0}^{m}b\left(k\right)z^k=\sum _{k=0}^{m}b\left(k\right)w^k$$
38		fveq2	$$⊢k=j\to b\left(k\right)=b\left(j\right)$$
39	38 29	oveq12d	$$⊢k=j\to b\left(k\right)w^k=b\left(j\right)w^j$$
40	39	cbvsumv	$$⊢\sum _{k=0}^{m}b\left(k\right)w^k=\sum _{j=0}^{m}b\left(j\right)w^j$$
41	37 40	eqtrdi	$$⊢z=w\to \sum _{k=0}^{m}b\left(k\right)z^k=\sum _{j=0}^{m}b\left(j\right)w^j$$
42	41	cbvmptv	$$⊢\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)=\left(w\in ℂ⟼\sum _{j=0}^{m}b\left(j\right)w^j\right)$$
43	35 42	eqtrdi	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to F=\left(w\in ℂ⟼\sum _{j=0}^{m}b\left(j\right)w^j\right)$$
44	17 18 19 20 21 22 23 34 43	coeeulem	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\wedge \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\right)\to a=b$$
45	44	3expia	$$⊢\left(\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\wedge \left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\to a=b\right)$$
46	45	rexlimdvva	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\to \left(\exists n\in {\mathbb{N}}_0\exists m\in {\mathbb{N}}_0\left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\to a=b\right)$$
47	16 46	biimtrrid	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge \left(a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\right)\right)\to \left(\left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\to a=b\right)$$
48	47	ralrimivva	$$⊢F\in \mathrm{Poly}\left(S\right)\to \forall a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\forall b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\left(\left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\to a=b\right)$$
49		imaeq1	$$⊢a=b\to a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]$$
50	49	eqeq1d	$$⊢a=b\to \left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\leftrightarrow b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\right)$$
51		fveq1	$$⊢a=b\to a\left(k\right)=b\left(k\right)$$
52	51	oveq1d	$$⊢a=b\to a\left(k\right)z^k=b\left(k\right)z^k$$
53	52	sumeq2sdv	$$⊢a=b\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{k=0}^{n}b\left(k\right)z^k$$
54	53	mpteq2dv	$$⊢a=b\to \left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)$$
55	54	eqeq2d	$$⊢a=b\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\right)$$
56	50 55	anbi12d	$$⊢a=b\to \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \left(b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\right)\right)$$
57	56	rexbidv	$$⊢a=b\to \left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\right)\right)$$
58		fvoveq1	$$⊢n=m\to {\mathbb{Z}}_{\ge \left(n+1\right)}={\mathbb{Z}}_{\ge \left(m+1\right)}$$
59	58	imaeq2d	$$⊢n=m\to b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]$$
60	59	eqeq1d	$$⊢n=m\to \left(b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\leftrightarrow b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\right)$$
61		oveq2	$$⊢n=m\to \left(0\dots n\right)=\left(0\dots m\right)$$
62	61	sumeq1d	$$⊢n=m\to \sum _{k=0}^{n}b\left(k\right)z^k=\sum _{k=0}^{m}b\left(k\right)z^k$$
63	62	mpteq2dv	$$⊢n=m\to \left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)$$
64	63	eqeq2d	$$⊢n=m\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\leftrightarrow F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)$$
65	60 64	anbi12d	$$⊢n=m\to \left(\left(b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\right)\leftrightarrow \left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)$$
66	65	cbvrexvw	$$⊢\exists n\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}b\left(k\right)z^k\right)\right)\leftrightarrow \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)$$
67	57 66	bitrdi	$$⊢a=b\to \left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)$$
68	67	reu4	$$⊢\exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \left(\exists a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \forall a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\forall b\in \left({ℂ}^{{\mathbb{N}}_0}\right)\left(\left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\wedge \exists m\in {\mathbb{N}}_0\left(b\left[{\mathbb{Z}}_{\ge \left(m+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{m}b\left(k\right)z^k\right)\right)\right)\to a=b\right)\right)$$
69	15 48 68	sylanbrc	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$