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

Metamath Proof Explorer

Theorem ppicl

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

		Ref	Expression
	Assertion	ppicl	$⊢ A \in ℝ \to \underline{π} (A) \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		ppif	$⊢ \underline{π} : ℝ ⟶ ℕ_{0}$
2	1	ffvelcdmi	$⊢ A \in ℝ \to \underline{π} (A) \in ℕ_{0}$