This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coelem ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m ℕ0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 coeval ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
2 coeeu ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
3 riotacl2 ⊢ ( ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } )
4 2 3 syl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } )
5 1 4 eqeltrd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } )
6 imaeq1 ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
7 6 eqeq1d ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
8 fveq1 ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎 ‘ 𝑘 ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) )
9 8 oveq1d ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
10 9 sumeq2sdv ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
11 10 mpteq2dv ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
12 11 eqeq2d ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
13 7 12 anbi12d ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
14 13 rexbidv ⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
15 14 elrab ⊢ ( ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ↔ ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m ℕ0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
16 5 15 sylib ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m ℕ0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )