Theorem plyrecld

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

	Ref	Expression
Hypotheses	plyrecld.1	$$⊢\phi \to F\in \mathrm{Poly}\left(ℝ\right)$$
	plyrecld.2	$$⊢\phi \to X\in ℝ$$
Assertion	plyrecld	$$⊢\phi \to F\left(X\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		plyrecld.1	$$⊢\phi \to F\in \mathrm{Poly}\left(ℝ\right)$$
2		plyrecld.2	$$⊢\phi \to X\in ℝ$$
3		fvres	$$⊢X\in ℝ\to \left({F\upharpoonright }_{ℝ}\right)\left(X\right)=F\left(X\right)$$
4	2 3	syl	$$⊢\phi \to \left({F\upharpoonright }_{ℝ}\right)\left(X\right)=F\left(X\right)$$
5		plyreres	$$⊢F\in \mathrm{Poly}\left(ℝ\right)\to \left({F\upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
6	1 5	syl	$$⊢\phi \to \left({F\upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
7	6 2	ffvelcdmd	$$⊢\phi \to \left({F\upharpoonright }_{ℝ}\right)\left(X\right)\in ℝ$$
8	4 7	eqeltrrd	$$⊢\phi \to F\left(X\right)\in ℝ$$