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

Metamath Proof Explorer

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 = deg 1 ⁡ R
deg1xrf.p ⊢ P = Poly 1 ⁡ R
deg1xrf.b ⊢ B = Base P
Assertion deg1xrcl ⊢ F ∈ B → D ⁡ F ∈ ℝ *

Proof

Step Hyp Ref Expression
1 deg1xrf.d ⊢ D = deg 1 ⁡ R
2 deg1xrf.p ⊢ P = Poly 1 ⁡ R
3 deg1xrf.b ⊢ B = Base P
4 1 2 3 deg1xrf ⊢ D : B ⟶ ℝ *
5 4 ffvelcdmi ⊢ F ∈ B → D ⁡ F ∈ ℝ *