# Metamath Proof Explorer

## Theorem 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}=\mathrm{coeff}\left({F}\right)$
dgrub.2 ${⊢}{N}=\mathrm{deg}\left({F}\right)$
Assertion coeid3 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {M}\in {ℤ}_{\ge {N}}\wedge {X}\in ℂ\right)\to {F}\left({X}\right)=\sum _{{k}=0}^{{M}}{A}\left({k}\right){{X}}^{{k}}$

### Proof

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