Theorem ppicl

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

	Ref	Expression
Assertion	ppicl	⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		ppif	⊢ π : ℝ ⟶ ℕ0
2	1	ffvelrni	⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 )