Theorem pntrf

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

	Ref	Expression
Hypothesis	pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion	pntrf	|- R : RR+ --> RR

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		rpre	|- ( a e. RR+ -> a e. RR )
3		chpcl	|- ( a e. RR -> ( psi ` a ) e. RR )
4	2 3	syl	|- ( a e. RR+ -> ( psi ` a ) e. RR )
5	4 2	resubcld	|- ( a e. RR+ -> ( ( psi ` a ) - a ) e. RR )
6	1 5	fmpti	|- R : RR+ --> RR