Description: Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | coe1fval.a | |
|
Assertion | coe1fval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coe1fval.a | |
|
2 | elex | |
|
3 | fveq1 | |
|
4 | 3 | mpteq2dv | |
5 | df-coe1 | |
|
6 | nn0ex | |
|
7 | 6 | mptex | |
8 | 4 5 7 | fvmpt | |
9 | 1 8 | eqtrid | |
10 | 2 9 | syl | |