Theorem ppif

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

	Ref	Expression
Assertion	ppif	$$⊢\underset{\_}{\pi }:ℝ⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		df-ppi	$$⊢\underset{\_}{\pi }=\left(x\in ℝ⟼\left|\left[0,x\right]\cap \mathbb{P}\right|\right)$$
2		ppifi	$$⊢x\in ℝ\to \left[0,x\right]\cap \mathbb{P}\in \mathrm{Fin}$$
3		hashcl	$$⊢\left[0,x\right]\cap \mathbb{P}\in \mathrm{Fin}\to \left|\left[0,x\right]\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
4	2 3	syl	$$⊢x\in ℝ\to \left|\left[0,x\right]\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
5	1 4	fmpti	$$⊢\underset{\_}{\pi }:ℝ⟶{\mathbb{N}}_0$$