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

Metamath Proof Explorer

Theorem ppival

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

		Ref	Expression
	Assertion	ppival	$⊢ A \in ℝ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$

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	fveq2d	$⊢ x = A \to \|[0, x] \cap ℙ\| = \|[0, A] \cap ℙ\|$
4		df-ppi	$⊢ \underline{π} = (x \in ℝ ⟼ \|[0, x] \cap ℙ\|)$
5		fvex	$⊢ \|[0, A] \cap ℙ\| \in V$
6	3 4 5	fvmpt	$⊢ A \in ℝ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$