Theorem coef

Description: The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion	coef	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2	1	dgrlem	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) )
3	2	simpld	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )