coeeulem

	Ref	Expression
Hypotheses	coeeu.1	$⊢ φ \to F \in Poly (S)$
	coeeu.2	$⊢ φ \to A \in (ℂ^{ℕ_{0}})$
	coeeu.3	$⊢ φ \to B \in (ℂ^{ℕ_{0}})$
	coeeu.4	$⊢ φ \to M \in ℕ_{0}$
	coeeu.5	$⊢ φ \to N \in ℕ_{0}$
	coeeu.6	$⊢ φ \to A [ℤ_{\geq (M + 1)}] = \{0\}$
	coeeu.7	$⊢ φ \to B [ℤ_{\geq (N + 1)}] = \{0\}$
	coeeu.8	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
	coeeu.9	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
Assertion	coeeulem	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		coeeu.1	$⊢ φ \to F \in Poly (S)$
2		coeeu.2	$⊢ φ \to A \in (ℂ^{ℕ_{0}})$
3		coeeu.3	$⊢ φ \to B \in (ℂ^{ℕ_{0}})$
4		coeeu.4	$⊢ φ \to M \in ℕ_{0}$
5		coeeu.5	$⊢ φ \to N \in ℕ_{0}$
6		coeeu.6	$⊢ φ \to A [ℤ_{\geq (M + 1)}] = \{0\}$
7		coeeu.7	$⊢ φ \to B [ℤ_{\geq (N + 1)}] = \{0\}$
8		coeeu.8	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
9		coeeu.9	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
10		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
11	4 5	nn0addcld	$⊢ φ \to M + N \in ℕ_{0}$
12		subcl	$⊢ (x \in ℂ \land y \in ℂ) \to x - y \in ℂ$
13	12	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x - y \in ℂ$
14		cnex	$⊢ ℂ \in V$
15		nn0ex	$⊢ ℕ_{0} \in V$
16	14 15	elmap	$⊢ A \in (ℂ^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ ℂ$
17	2 16	sylib	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
18	14 15	elmap	$⊢ B \in (ℂ^{ℕ_{0}}) \leftrightarrow B : ℕ_{0} ⟶ ℂ$
19	3 18	sylib	$⊢ φ \to B : ℕ_{0} ⟶ ℂ$
20	15	a1i	$⊢ φ \to ℕ_{0} \in V$
21		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
22	13 17 19 20 20 21	off	$⊢ φ \to (A -_{f} B) : ℕ_{0} ⟶ ℂ$
23	14 15	elmap	$⊢ A -_{f} B \in (ℂ^{ℕ_{0}}) \leftrightarrow (A -_{f} B) : ℕ_{0} ⟶ ℂ$
24	22 23	sylibr	$⊢ φ \to A -_{f} B \in (ℂ^{ℕ_{0}})$
25		0cn	$⊢ 0 \in ℂ$
26		snssi	$⊢ 0 \in ℂ \to \{0\} \subseteq ℂ$
27	25 26	ax-mp	$⊢ \{0\} \subseteq ℂ$
28		ssequn2	$⊢ \{0\} \subseteq ℂ \leftrightarrow ℂ \cup \{0\} = ℂ$
29	27 28	mpbi	$⊢ ℂ \cup \{0\} = ℂ$
30	29	oveq1i	$⊢ {(ℂ \cup \{0\})}^{ℕ_{0}} = ℂ^{ℕ_{0}}$
31	24 30	eleqtrrdi	$⊢ φ \to A -_{f} B \in ({(ℂ \cup \{0\})}^{ℕ_{0}})$
32	11	nn0red	$⊢ φ \to M + N \in ℝ$
33		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
34		ltnle	$⊢ (M + N \in ℝ \land k \in ℝ) \to (M + N < k \leftrightarrow \neg k \leq M + N)$
35	32 33 34	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to (M + N < k \leftrightarrow \neg k \leq M + N)$
36	17	ffnd	$⊢ φ \to A Fn ℕ_{0}$
37	19	ffnd	$⊢ φ \to B Fn ℕ_{0}$
38		eqidd	$⊢ (φ \land k \in ℕ_{0}) \to A (k) = A (k)$
39		eqidd	$⊢ (φ \land k \in ℕ_{0}) \to B (k) = B (k)$
40	36 37 20 20 21 38 39	ofval	$⊢ (φ \land k \in ℕ_{0}) \to (A -_{f} B) (k) = A (k) - B (k)$
41	40	adantrr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (A -_{f} B) (k) = A (k) - B (k)$
42	4	nn0red	$⊢ φ \to M \in ℝ$
43	42	adantr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to M \in ℝ$
44	32	adantr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to M + N \in ℝ$
45	33	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℝ$
46	45	adantrr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to k \in ℝ$
47	4	nn0cnd	$⊢ φ \to M \in ℂ$
48	5	nn0cnd	$⊢ φ \to N \in ℂ$
49	47 48	addcomd	$⊢ φ \to M + N = N + M$
50		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
51	5 50	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
52	4	nn0zd	$⊢ φ \to M \in ℤ$
53		eluzadd	$⊢ (N \in ℤ_{\geq 0} \land M \in ℤ) \to N + M \in ℤ_{\geq (0 + M)}$
54	51 52 53	syl2anc	$⊢ φ \to N + M \in ℤ_{\geq (0 + M)}$
55	49 54	eqeltrd	$⊢ φ \to M + N \in ℤ_{\geq (0 + M)}$
56	47	addid2d	$⊢ φ \to 0 + M = M$
57	56	fveq2d	$⊢ φ \to ℤ_{\geq (0 + M)} = ℤ_{\geq M}$
58	55 57	eleqtrd	$⊢ φ \to M + N \in ℤ_{\geq M}$
59		eluzle	$⊢ M + N \in ℤ_{\geq M} \to M \leq M + N$
60	58 59	syl	$⊢ φ \to M \leq M + N$
61	60	adantr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to M \leq M + N$
62		simprr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to M + N < k$
63	43 44 46 61 62	lelttrd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to M < k$
64	43 46	ltnled	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (M < k \leftrightarrow \neg k \leq M)$
65	63 64	mpbid	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to \neg k \leq M$
66		plyco0	$⊢ (M \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M))$
67	4 17 66	syl2anc	$⊢ φ \to (A [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M))$
68	6 67	mpbid	$⊢ φ \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq M)$
69	68	r19.21bi	$⊢ (φ \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq M)$
70	69	adantrr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (A (k) \neq 0 \to k \leq M)$
71	70	necon1bd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (\neg k \leq M \to A (k) = 0)$
72	65 71	mpd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to A (k) = 0$
73	5	nn0red	$⊢ φ \to N \in ℝ$
74	73	adantr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to N \in ℝ$
75	4 50	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
76	5	nn0zd	$⊢ φ \to N \in ℤ$
77		eluzadd	$⊢ (M \in ℤ_{\geq 0} \land N \in ℤ) \to M + N \in ℤ_{\geq (0 + N)}$
78	75 76 77	syl2anc	$⊢ φ \to M + N \in ℤ_{\geq (0 + N)}$
79	48	addid2d	$⊢ φ \to 0 + N = N$
80	79	fveq2d	$⊢ φ \to ℤ_{\geq (0 + N)} = ℤ_{\geq N}$
81	78 80	eleqtrd	$⊢ φ \to M + N \in ℤ_{\geq N}$
82		eluzle	$⊢ M + N \in ℤ_{\geq N} \to N \leq M + N$
83	81 82	syl	$⊢ φ \to N \leq M + N$
84	83	adantr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to N \leq M + N$
85	74 44 46 84 62	lelttrd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to N < k$
86	74 46	ltnled	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (N < k \leftrightarrow \neg k \leq N)$
87	85 86	mpbid	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to \neg k \leq N$
88		plyco0	$⊢ (N \in ℕ_{0} \land B : ℕ_{0} ⟶ ℂ) \to (B [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N))$
89	5 19 88	syl2anc	$⊢ φ \to (B [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N))$
90	7 89	mpbid	$⊢ φ \to \forall k \in ℕ_{0} (B (k) \neq 0 \to k \leq N)$
91	90	r19.21bi	$⊢ (φ \land k \in ℕ_{0}) \to (B (k) \neq 0 \to k \leq N)$
92	91	adantrr	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (B (k) \neq 0 \to k \leq N)$
93	92	necon1bd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (\neg k \leq N \to B (k) = 0)$
94	87 93	mpd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to B (k) = 0$
95	72 94	oveq12d	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to A (k) - B (k) = 0 - 0$
96		0m0e0	$⊢ 0 - 0 = 0$
97	95 96	eqtrdi	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to A (k) - B (k) = 0$
98	41 97	eqtrd	$⊢ (φ \land (k \in ℕ_{0} \land M + N < k)) \to (A -_{f} B) (k) = 0$
99	98	expr	$⊢ (φ \land k \in ℕ_{0}) \to (M + N < k \to (A -_{f} B) (k) = 0)$
100	35 99	sylbird	$⊢ (φ \land k \in ℕ_{0}) \to (\neg k \leq M + N \to (A -_{f} B) (k) = 0)$
101	100	necon1ad	$⊢ (φ \land k \in ℕ_{0}) \to ((A -_{f} B) (k) \neq 0 \to k \leq M + N)$
102	101	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} ((A -_{f} B) (k) \neq 0 \to k \leq M + N)$
103		plyco0	$⊢ (M + N \in ℕ_{0} \land (A -_{f} B) : ℕ_{0} ⟶ ℂ) \to ((A -_{f} B) [ℤ_{\geq (M + N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((A -_{f} B) (k) \neq 0 \to k \leq M + N))$
104	11 22 103	syl2anc	$⊢ φ \to ((A -_{f} B) [ℤ_{\geq (M + N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} ((A -_{f} B) (k) \neq 0 \to k \leq M + N))$
105	102 104	mpbird	$⊢ φ \to (A -_{f} B) [ℤ_{\geq (M + N + 1)}] = \{0\}$
106		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
107		fconstmpt	$⊢ ℂ \times \{0\} = (z \in ℂ ⟼ 0)$
108	106 107	eqtri	$⊢ 0_{𝑝} = (z \in ℂ ⟼ 0)$
109		elfznn0	$⊢ k \in (0 \dots M + N) \to k \in ℕ_{0}$
110	40	adantlr	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (A -_{f} B) (k) = A (k) - B (k)$
111	110	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (A -_{f} B) (k) z^{k} = (A (k) - B (k)) z^{k}$
112	17	adantr	$⊢ (φ \land z \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
113	112	ffvelrnda	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
114	19	adantr	$⊢ (φ \land z \in ℂ) \to B : ℕ_{0} ⟶ ℂ$
115	114	ffvelrnda	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to B (k) \in ℂ$
116		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
117	116	adantll	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to z^{k} \in ℂ$
118	113 115 117	subdird	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (A (k) - B (k)) z^{k} = A (k) z^{k} - B (k) z^{k}$
119	111 118	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (A -_{f} B) (k) z^{k} = A (k) z^{k} - B (k) z^{k}$
120	109 119	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M + N)) \to (A -_{f} B) (k) z^{k} = A (k) z^{k} - B (k) z^{k}$
121	120	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} (A -_{f} B) (k) z^{k} = \sum_{k = 0}^{M + N} (A (k) z^{k} - B (k) z^{k})$
122		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots M + N) \in Fin$
123	113 117	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) z^{k} \in ℂ$
124	109 123	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M + N)) \to A (k) z^{k} \in ℂ$
125	115 117	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to B (k) z^{k} \in ℂ$
126	109 125	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M + N)) \to B (k) z^{k} \in ℂ$
127	122 124 126	fsumsub	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} (A (k) z^{k} - B (k) z^{k}) = \sum_{k = 0}^{M + N} A (k) z^{k} - \sum_{k = 0}^{M + N} B (k) z^{k}$
128	122 124	fsumcl	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} A (k) z^{k} \in ℂ$
129	8 9	eqtr3d	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
130	129	fveq1d	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) (z) = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) (z)$
131	130	adantr	$⊢ (φ \land z \in ℂ) \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) (z) = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) (z)$
132		simpr	$⊢ (φ \land z \in ℂ) \to z \in ℂ$
133		sumex	$⊢ \sum_{k = 0}^{M} A (k) z^{k} \in V$
134		eqid	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k})$
135	134	fvmpt2	$⊢ (z \in ℂ \land \sum_{k = 0}^{M} A (k) z^{k} \in V) \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) (z) = \sum_{k = 0}^{M} A (k) z^{k}$
136	132 133 135	sylancl	$⊢ (φ \land z \in ℂ) \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) (z) = \sum_{k = 0}^{M} A (k) z^{k}$
137		fzss2	$⊢ M + N \in ℤ_{\geq M} \to (0 \dots M) \subseteq (0 \dots M + N)$
138	58 137	syl	$⊢ φ \to (0 \dots M) \subseteq (0 \dots M + N)$
139	138	adantr	$⊢ (φ \land z \in ℂ) \to (0 \dots M) \subseteq (0 \dots M + N)$
140	139	sselda	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to k \in (0 \dots M + N)$
141	140 124	syldan	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots M)) \to A (k) z^{k} \in ℂ$
142		eldifn	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to \neg k \in (0 \dots M)$
143	142	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to \neg k \in (0 \dots M)$
144		eldifi	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to k \in (0 \dots M + N)$
145	144 109	syl	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots M)) \to k \in ℕ_{0}$
146		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
147	146 50	eleqtrdi	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
148	52	adantr	$⊢ (φ \land k \in ℕ_{0}) \to M \in ℤ$
149		elfz5	$⊢ (k \in ℤ_{\geq 0} \land M \in ℤ) \to (k \in (0 \dots M) \leftrightarrow k \leq M)$
150	147 148 149	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (k \in (0 \dots M) \leftrightarrow k \leq M)$
151	69 150	sylibrd	$⊢ (φ \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \in (0 \dots M))$
152	151	adantlr	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \in (0 \dots M))$
153	152	necon1bd	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (\neg k \in (0 \dots M) \to A (k) = 0)$
154	145 153	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to (\neg k \in (0 \dots M) \to A (k) = 0)$
155	143 154	mpd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) = 0$
156	155	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) z^{k} = 0 \cdot z^{k}$
157	132 145 116	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to z^{k} \in ℂ$
158	157	mul02d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to 0 \cdot z^{k} = 0$
159	156 158	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots M))) \to A (k) z^{k} = 0$
160	139 141 159 122	fsumss	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} A (k) z^{k} = \sum_{k = 0}^{M + N} A (k) z^{k}$
161	136 160	eqtrd	$⊢ (φ \land z \in ℂ) \to (z \in ℂ ⟼ \sum_{k = 0}^{M} A (k) z^{k}) (z) = \sum_{k = 0}^{M + N} A (k) z^{k}$
162		sumex	$⊢ \sum_{k = 0}^{N} B (k) z^{k} \in V$
163		eqid	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k})$
164	163	fvmpt2	$⊢ (z \in ℂ \land \sum_{k = 0}^{N} B (k) z^{k} \in V) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) (z) = \sum_{k = 0}^{N} B (k) z^{k}$
165	132 162 164	sylancl	$⊢ (φ \land z \in ℂ) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) (z) = \sum_{k = 0}^{N} B (k) z^{k}$
166		fzss2	$⊢ M + N \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots M + N)$
167	81 166	syl	$⊢ φ \to (0 \dots N) \subseteq (0 \dots M + N)$
168	167	adantr	$⊢ (φ \land z \in ℂ) \to (0 \dots N) \subseteq (0 \dots M + N)$
169	168	sselda	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N)) \to k \in (0 \dots M + N)$
170	169 126	syldan	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N)) \to B (k) z^{k} \in ℂ$
171		eldifn	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots N)) \to \neg k \in (0 \dots N)$
172	171	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to \neg k \in (0 \dots N)$
173		eldifi	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots N)) \to k \in (0 \dots M + N)$
174	173 109	syl	$⊢ k \in ((0 \dots M + N) ∖ (0 \dots N)) \to k \in ℕ_{0}$
175	76	adantr	$⊢ (φ \land k \in ℕ_{0}) \to N \in ℤ$
176		elfz5	$⊢ (k \in ℤ_{\geq 0} \land N \in ℤ) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
177	147 175 176	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
178	91 177	sylibrd	$⊢ (φ \land k \in ℕ_{0}) \to (B (k) \neq 0 \to k \in (0 \dots N))$
179	178	adantlr	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (B (k) \neq 0 \to k \in (0 \dots N))$
180	179	necon1bd	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to (\neg k \in (0 \dots N) \to B (k) = 0)$
181	174 180	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to (\neg k \in (0 \dots N) \to B (k) = 0)$
182	172 181	mpd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to B (k) = 0$
183	182	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to B (k) z^{k} = 0 \cdot z^{k}$
184	132 174 116	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to z^{k} \in ℂ$
185	184	mul02d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to 0 \cdot z^{k} = 0$
186	183 185	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M + N) ∖ (0 \dots N))) \to B (k) z^{k} = 0$
187	168 170 186 122	fsumss	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{N} B (k) z^{k} = \sum_{k = 0}^{M + N} B (k) z^{k}$
188	165 187	eqtrd	$⊢ (φ \land z \in ℂ) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} B (k) z^{k}) (z) = \sum_{k = 0}^{M + N} B (k) z^{k}$
189	131 161 188	3eqtr3d	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} A (k) z^{k} = \sum_{k = 0}^{M + N} B (k) z^{k}$
190	128 189	subeq0bd	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M + N} A (k) z^{k} - \sum_{k = 0}^{M + N} B (k) z^{k} = 0$
191	121 127 190	3eqtrrd	$⊢ (φ \land z \in ℂ) \to 0 = \sum_{k = 0}^{M + N} (A -_{f} B) (k) z^{k}$
192	191	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ 0) = (z \in ℂ ⟼ \sum_{k = 0}^{M + N} (A -_{f} B) (k) z^{k})$
193	108 192	syl5eq	$⊢ φ \to 0_{𝑝} = (z \in ℂ ⟼ \sum_{k = 0}^{M + N} (A -_{f} B) (k) z^{k})$
194	10 11 31 105 193	plyeq0	$⊢ φ \to A -_{f} B = ℕ_{0} \times \{0\}$
195		ofsubeq0	$⊢ (ℕ_{0} \in V \land A : ℕ_{0} ⟶ ℂ \land B : ℕ_{0} ⟶ ℂ) \to (A -_{f} B = ℕ_{0} \times \{0\} \leftrightarrow A = B)$
196	15 17 19 195	mp3an2i	$⊢ φ \to (A -_{f} B = ℕ_{0} \times \{0\} \leftrightarrow A = B)$
197	194 196	mpbid	$⊢ φ \to A = B$

Metamath Proof Explorer

Theorem coeeulem

Proof