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 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion coeid3 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 1 2 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
4 3 3adant2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
5 fzss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
6 5 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
7 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
8 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
9 8 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
10 9 ffvelrnda ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
11 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑘 ) ∈ ℂ )
12 11 3ad2antl3 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑘 ) ∈ ℂ )
13 10 12 mulcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ ℂ )
14 7 13 sylan2 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ∈ ℂ )
15 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
16 15 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
17 simpl1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
18 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
19 elfzuz ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
20 18 19 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
21 20 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
22 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
23 21 22 eleqtrrdi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
24 1 2 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑁 )
25 24 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
26 17 23 25 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
27 simpl2 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
28 eluzel2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
29 27 28 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℤ )
30 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
31 21 29 30 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
32 26 31 sylibrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑁 ) ) )
33 32 necon1bd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
34 16 33 mpd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
35 34 oveq1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( 0 · ( 𝑋 ↑ 𝑘 ) ) )
36 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
37 18 36 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
38 37 12 sylan2 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑋 ↑ 𝑘 ) ∈ ℂ )
39 38 mul02d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑋 ↑ 𝑘 ) ) = 0 )
40 35 39 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = 0 )
41 fzfid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → ( 0 ... 𝑀 ) ∈ Fin )
42 6 14 40 41 fsumss ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
43 4 42 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )