coeidlem

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

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$⊢ A = coeff (F)$
2		dgrub.2	$⊢ N = \deg (F)$
3		coeid.3	$⊢ φ \to F \in Poly (S)$
4		coeid.4	$⊢ φ \to M \in ℕ_{0}$
5		coeid.5	$⊢ φ \to B \in ({(S \cup \{0\})}^{ℕ_{0}})$
6		coeid.6	$⊢ φ \to B [ℤ_{\geq (M + 1)}] = \{0\}$
7		coeid.7	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{M} B (k) z^{k})$
8		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
9	3 8	syl	$⊢ φ \to S \subseteq ℂ$
10		0cnd	$⊢ φ \to 0 \in ℂ$
11	10	snssd	$⊢ φ \to \{0\} \subseteq ℂ$
12	9 11	unssd	$⊢ φ \to S \cup \{0\} \subseteq ℂ$
13		cnex	$⊢ ℂ \in V$
14		ssexg	$⊢ (S \cup \{0\} \subseteq ℂ \land ℂ \in V) \to S \cup \{0\} \in V$
15	12 13 14	sylancl	$⊢ φ \to S \cup \{0\} \in V$
16		nn0ex	$⊢ ℕ_{0} \in V$
17		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (B \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow B : ℕ_{0} ⟶ S \cup \{0\})$
18	15 16 17	sylancl	$⊢ φ \to (B \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow B : ℕ_{0} ⟶ S \cup \{0\})$
19	5 18	mpbid	$⊢ φ \to B : ℕ_{0} ⟶ S \cup \{0\}$
20	19 12	fssd	$⊢ φ \to B : ℕ_{0} ⟶ ℂ$
21	3 4 20 6 7	coeeq	$⊢ φ \to coeff (F) = B$
22	1 21	syl5req	$⊢ φ \to B = A$
23	22	adantr	$⊢ (φ \land z \in ℂ) \to B = A$
24		fveq1	$⊢ B = A \to B (k) = A (k)$
25	24	oveq1d	$⊢ B = A \to B (k) z^{k} = A (k) z^{k}$
26	25	sumeq2sdv	$⊢ B = A \to \sum_{k = 0}^{M} B (k) z^{k} = \sum_{k = 0}^{M} A (k) z^{k}$
27	23 26	syl	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} B (k) z^{k} = \sum_{k = 0}^{M} A (k) z^{k}$
28	3	adantr	$⊢ (φ \land z \in ℂ) \to F \in Poly (S)$
29		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
30	2 29	eqeltrid	$⊢ F \in Poly (S) \to N \in ℕ_{0}$
31	28 30	syl	$⊢ (φ \land z \in ℂ) \to N \in ℕ_{0}$
32	31	nn0zd	$⊢ (φ \land z \in ℂ) \to N \in ℤ$
33	4	adantr	$⊢ (φ \land z \in ℂ) \to M \in ℕ_{0}$
34	33	nn0zd	$⊢ (φ \land z \in ℂ) \to M \in ℤ$
35	23	imaeq1d	$⊢ (φ \land z \in ℂ) \to B [ℤ_{\geq (M + 1)}] = A [ℤ_{\geq (M + 1)}]$
36	6	adantr	$⊢ (φ \land z \in ℂ) \to B [ℤ_{\geq (M + 1)}] = \{0\}$
37	35 36	eqtr3d	$⊢ (φ \land z \in ℂ) \to A [ℤ_{\geq (M + 1)}] = \{0\}$
38	1 2	dgrlb	$⊢ (F \in Poly (S) \land M \in ℕ_{0} \land A [ℤ_{\geq (M + 1)}] = \{0\}) \to N \leq M$
39	28 33 37 38	syl3anc	$⊢ (φ \land z \in ℂ) \to N \leq M$
40		eluz2	$⊢ M \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land M \in ℤ \land N \leq M)$
41	32 34 39 40	syl3anbrc	$⊢ (φ \land z \in ℂ) \to M \in ℤ_{\geq N}$
42		fzss2	$⊢ M \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots M)$
43	41 42	syl	$⊢ (φ \land z \in ℂ) \to (0 \dots N) \subseteq (0 \dots M)$
44		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
45		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
46	45 3	sseldi	$⊢ φ \to F \in Poly (ℂ)$
47	1	coef3	$⊢ F \in Poly (ℂ) \to A : ℕ_{0} ⟶ ℂ$
48	46 47	syl	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
49	48	adantr	$⊢ (φ \land z \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
50	49	ffvelrnda	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
51		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
52	51	adantll	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to z^{k} \in ℂ$
53	50 52	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in ℕ_{0}) \to A (k) z^{k} \in ℂ$
54	44 53	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N)) \to A (k) z^{k} \in ℂ$
55		eldifn	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to \neg k \in (0 \dots N)$
56	55	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to \neg k \in (0 \dots N)$
57		eldifi	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in (0 \dots M)$
58		elfznn0	$⊢ k \in (0 \dots M) \to k \in ℕ_{0}$
59	57 58	syl	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in ℕ_{0}$
60	1 2	dgrub	$⊢ (F \in Poly (S) \land k \in ℕ_{0} \land A (k) \neq 0) \to k \leq N$
61	60	3expia	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq N)$
62	28 59 61	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (A (k) \neq 0 \to k \leq N)$
63		elfzuz	$⊢ k \in (0 \dots M) \to k \in ℤ_{\geq 0}$
64	57 63	syl	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in ℤ_{\geq 0}$
65		elfz5	$⊢ (k \in ℤ_{\geq 0} \land N \in ℤ) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
66	64 32 65	syl2anr	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
67	62 66	sylibrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (A (k) \neq 0 \to k \in (0 \dots N))$
68	67	necon1bd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (\neg k \in (0 \dots N) \to A (k) = 0)$
69	56 68	mpd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) = 0$
70	69	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) z^{k} = 0 \cdot z^{k}$
71		simpr	$⊢ (φ \land z \in ℂ) \to z \in ℂ$
72	71 59 51	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to z^{k} \in ℂ$
73	72	mul02d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to 0 \cdot z^{k} = 0$
74	70 73	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) z^{k} = 0$
75		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots M) \in Fin$
76	43 54 74 75	fsumss	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{N} A (k) z^{k} = \sum_{k = 0}^{M} A (k) z^{k}$
77	27 76	eqtr4d	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{M} B (k) z^{k} = \sum_{k = 0}^{N} A (k) z^{k}$
78	77	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{M} B (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
79	7 78	eqtrd	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$

Metamath Proof Explorer

Theorem coeidlem

Proof