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

Metamath Proof Explorer

Theorem ppif

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

		Ref	Expression
	Assertion	ppif	$⊢ \underline{π} : ℝ ⟶ ℕ_{0}$

Step	Hyp	Ref	Expression
1		df-ppi	$⊢ \underline{π} = (x \in ℝ ⟼ \|[0, x] \cap ℙ\|)$
2		ppifi	$⊢ x \in ℝ \to [0, x] \cap ℙ \in Fin$
3		hashcl	$⊢ [0, x] \cap ℙ \in Fin \to \|[0, x] \cap ℙ\| \in ℕ_{0}$
4	2 3	syl	$⊢ x \in ℝ \to \|[0, x] \cap ℙ\| \in ℕ_{0}$
5	1 4	fmpti	$⊢ \underline{π} : ℝ ⟶ ℕ_{0}$