This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtval

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

		Ref	Expression
	Assertion	chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = A \to [0, x] = [0, A]$
2	1	ineq1d	$⊢ x = A \to [0, x] \cap ℙ = [0, A] \cap ℙ$
3	2	sumeq1d	$⊢ x = A \to \sum_{p \in [0, x] \cap ℙ} \log p = \sum_{p \in [0, A] \cap ℙ} \log p$
4		df-cht	$⊢ θ = (x \in ℝ ⟼ \sum_{p \in [0, x] \cap ℙ} \log p)$
5		sumex	$⊢ \sum_{p \in [0, A] \cap ℙ} \log p \in V$
6	3 4 5	fvmpt	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$