Theorem plyrecld

Description: Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018)

	Ref	Expression
Hypotheses	plyrecld.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℝ ) )
	plyrecld.2	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion	plyrecld	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		plyrecld.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℝ ) )
2		plyrecld.2	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3		fvres	⊢ ( 𝑋 ∈ ℝ → ( ( 𝐹 ↾ ℝ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
4	2 3	syl	⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
5		plyreres	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )
6	1 5	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )
7	6 2	ffvelrnd	⊢ ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ‘ 𝑋 ) ∈ ℝ )
8	4 7	eqeltrrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )