Theorem deg1xrcl

Description: Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1xrf.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1xrf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1xrf.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1xrf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1xrf.b	$$⊢B={\mathrm{Base}}_P$$
4	1 2 3	deg1xrf	$$⊢D:B⟶{ℝ}^{*}$$
5	4	ffvelrni	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$