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 \underset{\_}{\pi }\left(A\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		ppif	$$⊢\underset{\_}{\pi }:ℝ⟶{\mathbb{N}}_0$$
2	1	ffvelrni	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)\in {\mathbb{N}}_0$$