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	$$⊢\underset{\_}{\pi }=\left(x\in ℝ⟼\left|\left[0,x\right]\cap \mathbb{P}\right|\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cppi	$$class\underset{\_}{\pi }$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		chash	$$class\left|.\right|$$
4		cc0	$$class0$$
5		cicc	$$class\left[.\right]$$
6	1	cv	$$setvarx$$
7	4 6 5	co	$$class\left[0,x\right]$$
8		cprime	$$class\mathbb{P}$$
9	7 8	cin	$$class\left(\left[0,x\right]\cap \mathbb{P}\right)$$
10	9 3	cfv	$$class\left|\left[0,x\right]\cap \mathbb{P}\right|$$
11	1 2 10	cmpt	$$class\left(x\in ℝ⟼\left|\left[0,x\right]\cap \mathbb{P}\right|\right)$$
12	0 11	wceq	$$wff\underset{\_}{\pi }=\left(x\in ℝ⟼\left|\left[0,x\right]\cap \mathbb{P}\right|\right)$$