Theorem ppif

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

	Ref	Expression
Assertion	ppif	⊢ π : ℝ ⟶ ℕ0

Proof

Step	Hyp	Ref	Expression
1		df-ppi	⊢ π = ( 𝑥 ∈ ℝ ↦ ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) )
2		ppifi	⊢ ( 𝑥 ∈ ℝ → ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∈ Fin )
3		hashcl	⊢ ( ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∈ Fin → ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) ∈ ℕ0 )
4	2 3	syl	⊢ ( 𝑥 ∈ ℝ → ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) ∈ ℕ0 )
5	1 4	fmpti	⊢ π : ℝ ⟶ ℕ0