Theorem pntrf

Description: Functionality of the residual. Lemma for pnt . (Contributed by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Hypothesis	pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		rpre	⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ )
3		chpcl	⊢ ( 𝑎 ∈ ℝ → ( ψ ‘ 𝑎 ) ∈ ℝ )
4	2 3	syl	⊢ ( 𝑎 ∈ ℝ+ → ( ψ ‘ 𝑎 ) ∈ ℝ )
5	4 2	resubcld	⊢ ( 𝑎 ∈ ℝ+ → ( ( ψ ‘ 𝑎 ) − 𝑎 ) ∈ ℝ )
6	1 5	fmpti	⊢ 𝑅 : ℝ+ ⟶ ℝ