Theorem pntrval

Description: Define the residual of the second Chebyshev function. The goal is to have R ( x ) e. o ( x ) , or R ( x ) / x ~>r 0 . (Contributed by Mario Carneiro, 8-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		fveq2	|- ( a = A -> ( psi ` a ) = ( psi ` A ) )
3		id	|- ( a = A -> a = A )
4	2 3	oveq12d	|- ( a = A -> ( ( psi ` a ) - a ) = ( ( psi ` A ) - A ) )
5		ovex	|- ( ( psi ` A ) - A ) e. _V
6	4 1 5	fvmpt	|- ( A e. RR+ -> ( R ` A ) = ( ( psi ` A ) - A ) )