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=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
Assertion	pntrval	$$⊢A\in {ℝ}^{+}\to R\left(A\right)=\psi \left(A\right)-A$$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
2		fveq2	$$⊢a=A\to \psi \left(a\right)=\psi \left(A\right)$$
3		id	$$⊢a=A\to a=A$$
4	2 3	oveq12d	$$⊢a=A\to \psi \left(a\right)-a=\psi \left(A\right)-A$$
5		ovex	$$⊢\psi \left(A\right)-A\in \mathrm{V}$$
6	4 1 5	fvmpt	$$⊢A\in {ℝ}^{+}\to R\left(A\right)=\psi \left(A\right)-A$$