Metamath Proof Explorer

Theorem coeeq2

Description: Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
dgrle.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
dgrle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
dgrle.4 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion coeeq2 ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgrle.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 dgrle.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 dgrle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
4 dgrle.4 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
5 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝜑 )
6 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝑘 ≤ 𝑁 )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝑘 ∈ ℕ0 )
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 7 8 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
10 2 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
12 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
13 9 11 12 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
14 6 13 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
15 5 14 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ 𝑁 ) → 𝐴 ∈ ℂ )
16 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ 𝑁 ) → 0 ∈ ℂ )
17 15 16 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ∈ ℂ )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
20 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) )
21 20 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ∈ ℂ ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) )
22 19 17 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) )
23 22 neeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 ↔ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ≠ 0 ) )
24 iffalse ⊢ ( ¬ 𝑘 ≤ 𝑁 → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) = 0 )
25 24 necon1ai ⊢ ( if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ≠ 0 → 𝑘 ≤ 𝑁 )
26 23 25 syl6bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
27 26 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
28 nfv ⊢ Ⅎ 𝑚 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 )
29 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 )
30 nfcv ⊢ Ⅎ 𝑘 0
31 29 30 nfne ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0
32 nfv ⊢ Ⅎ 𝑘 𝑚 ≤ 𝑁
33 31 32 nfim ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 )
34 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) )
35 34 neeq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 ) )
36 breq1 ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁 ) )
37 35 36 imbi12d ⊢ ( 𝑘 = 𝑚 → ( ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ↔ ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) )
38 28 33 37 cbvralw ⊢ ( ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) )
39 27 38 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) )
40 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) )
41 2 18 40 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) )
42 39 41 mpbird ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
43 nfcv ⊢ Ⅎ 𝑚 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
44 nfcv ⊢ Ⅎ 𝑘 ·
45 nfcv ⊢ Ⅎ 𝑘 ( 𝑧 ↑ 𝑚 )
46 29 44 45 nfov ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) )
47 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑧 ↑ 𝑘 ) = ( 𝑧 ↑ 𝑚 ) )
48 34 47 oveq12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) )
49 43 46 48 cbvsumi ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) )
50 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
51 50 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
52 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ≤ 𝑁 )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ≤ 𝑁 )
54 53 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) = 𝐴 )
55 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
56 54 55 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ∈ ℂ )
57 51 56 21 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) )
58 57 54 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 𝐴 )
59 58 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
60 59 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
61 49 60 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
62 61 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
63 4 62 eqtr4d ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
64 1 2 18 42 63 coeeq ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) )