Metamath Proof Explorer

Theorem ppival2

Description: Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion ppival2 ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 ppival ⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
4 ppisval ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
5 1 4 syl ⊢ ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
6 flid ⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
7 6 oveq2d ⊢ ( 𝐴 ∈ ℤ → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( 2 ... 𝐴 ) )
8 7 ineq1d ⊢ ( 𝐴 ∈ ℤ → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
9 5 8 eqtrd ⊢ ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
10 9 fveq2d ⊢ ( 𝐴 ∈ ℤ → ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )
11 3 10 eqtrd ⊢ ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) )