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 ) ) )