coeid3

Description: Reconstruct a polynomial as an explicit sum of the coefficient function up to at least the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	$⊢ A = coeff (F)$
	dgrub.2	$⊢ N = \deg (F)$
Assertion	coeid3	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to F (X) = \sum_{k = 0}^{M} A (k) X^{k}$

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$⊢ A = coeff (F)$
2		dgrub.2	$⊢ N = \deg (F)$
3	1 2	coeid2	$⊢ (F \in Poly (S) \land X \in ℂ) \to F (X) = \sum_{k = 0}^{N} A (k) X^{k}$
4	3	3adant2	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to F (X) = \sum_{k = 0}^{N} A (k) X^{k}$
5		fzss2	$⊢ M \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots M)$
6	5	3ad2ant2	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to (0 \dots N) \subseteq (0 \dots M)$
7		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
8	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
9	8	3ad2ant1	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
10	9	ffvelcdmda	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
11		expcl	$⊢ (X \in ℂ \land k \in ℕ_{0}) \to X^{k} \in ℂ$
12	11	3ad2antl3	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ℕ_{0}) \to X^{k} \in ℂ$
13	10 12	mulcld	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ℕ_{0}) \to A (k) X^{k} \in ℂ$
14	7 13	sylan2	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in (0 \dots N)) \to A (k) X^{k} \in ℂ$
15		eldifn	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to \neg k \in (0 \dots N)$
16	15	adantl	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to \neg k \in (0 \dots N)$
17		simpl1	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to F \in Poly (S)$
18		eldifi	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in (0 \dots M)$
19		elfzuz	$⊢ k \in (0 \dots M) \to k \in ℤ_{\geq 0}$
20	18 19	syl	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in ℤ_{\geq 0}$
21	20	adantl	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to k \in ℤ_{\geq 0}$
22		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
23	21 22	eleqtrrdi	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to k \in ℕ_{0}$
24	1 2	dgrub	$⊢ (F \in Poly (S) \land k \in ℕ_{0} \land A (k) \neq 0) \to k \leq N$
25	24	3expia	$⊢ (F \in Poly (S) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq N)$
26	17 23 25	syl2anc	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (A (k) \neq 0 \to k \leq N)$
27		simpl2	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to M \in ℤ_{\geq N}$
28		eluzel2	$⊢ M \in ℤ_{\geq N} \to N \in ℤ$
29	27 28	syl	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to N \in ℤ$
30		elfz5	$⊢ (k \in ℤ_{\geq 0} \land N \in ℤ) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
31	21 29 30	syl2anc	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (k \in (0 \dots N) \leftrightarrow k \leq N)$
32	26 31	sylibrd	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (A (k) \neq 0 \to k \in (0 \dots N))$
33	32	necon1bd	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to (\neg k \in (0 \dots N) \to A (k) = 0)$
34	16 33	mpd	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) = 0$
35	34	oveq1d	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) X^{k} = 0 \cdot X^{k}$
36		elfznn0	$⊢ k \in (0 \dots M) \to k \in ℕ_{0}$
37	18 36	syl	$⊢ k \in ((0 \dots M) ∖ (0 \dots N)) \to k \in ℕ_{0}$
38	37 12	sylan2	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to X^{k} \in ℂ$
39	38	mul02d	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to 0 \cdot X^{k} = 0$
40	35 39	eqtrd	$⊢ ((F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \land k \in ((0 \dots M) ∖ (0 \dots N))) \to A (k) X^{k} = 0$
41		fzfid	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to (0 \dots M) \in Fin$
42	6 14 40 41	fsumss	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to \sum_{k = 0}^{N} A (k) X^{k} = \sum_{k = 0}^{M} A (k) X^{k}$
43	4 42	eqtrd	$⊢ (F \in Poly (S) \land M \in ℤ_{\geq N} \land X \in ℂ) \to F (X) = \sum_{k = 0}^{M} A (k) X^{k}$

Metamath Proof Explorer

Theorem coeid3

Proof