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

Metamath Proof Explorer

Definition df-ppi

Description: Define the prime π function, which counts the number of primes less than or equal to x , see definition in ApostolNT p. 8. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	df-ppi	$⊢ \underline{π} = (x \in ℝ ⟼ \|[0, x] \cap ℙ\|)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cppi	$class \underline{π}$
1		vx	$setvar x$
2		cr	$class ℝ$
3		chash	$class \|.\|$
4		cc0	$class 0$
5		cicc	$class [.]$
6	1	cv	$setvar x$
7	4 6 5	co	$class [0, x]$
8		cprime	$class ℙ$
9	7 8	cin	$class ([0, x] \cap ℙ)$
10	9 3	cfv	$class \|[0, x] \cap ℙ\|$
11	1 2 10	cmpt	$class (x \in ℝ ⟼ \|[0, x] \cap ℙ\|)$
12	0 11	wceq	$wff \underline{π} = (x \in ℝ ⟼ \|[0, x] \cap ℙ\|)$