Description: Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | chtval | ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | ⊢ ( 𝑥 = 𝐴 → ( 0 [,] 𝑥 ) = ( 0 [,] 𝐴 ) ) | |
2 | 1 | ineq1d | ⊢ ( 𝑥 = 𝐴 → ( ( 0 [,] 𝑥 ) ∩ ℙ ) = ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
3 | 2 | sumeq1d | ⊢ ( 𝑥 = 𝐴 → Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
4 | df-cht | ⊢ θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) | |
5 | sumex | ⊢ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ∈ V | |
6 | 3 4 5 | fvmpt | ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |