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	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion	pntrval	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑅 ‘ 𝐴 ) = ( ( ψ ‘ 𝐴 ) − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		fveq2	⊢ ( 𝑎 = 𝐴 → ( ψ ‘ 𝑎 ) = ( ψ ‘ 𝐴 ) )
3		id	⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
4	2 3	oveq12d	⊢ ( 𝑎 = 𝐴 → ( ( ψ ‘ 𝑎 ) − 𝑎 ) = ( ( ψ ‘ 𝐴 ) − 𝐴 ) )
5		ovex	⊢ ( ( ψ ‘ 𝐴 ) − 𝐴 ) ∈ V
6	4 1 5	fvmpt	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑅 ‘ 𝐴 ) = ( ( ψ ‘ 𝐴 ) − 𝐴 ) )