Metamath Proof Explorer


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