Theorem chtval

Description: Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	chtval	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \left[0,x\right]=\left[0,A\right]$$
2	1	ineq1d	$$⊢x=A\to \left[0,x\right]\cap \mathbb{P}=\left[0,A\right]\cap \mathbb{P}$$
3	2	sumeq1d	$$⊢x=A\to \sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$
4		df-cht	$$⊢\theta =\left(x\in ℝ⟼\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\right)$$
5		sumex	$$⊢\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$