Metamath Proof Explorer

Theorem ppival2g

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

Ref Expression
Assertion ppival2g ( ( 𝐴 ∈ ℤ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 𝑀 ... 𝐴 ) ∩ ℙ ) ) )

Proof

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