Metamath Proof Explorer
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 } ) ) |