This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chpval

Description: Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion chpval ⊢ A ∈ ℝ → ψ ⁡ A = ∑ n = 1 A Λ ⁡ n

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ x = A → x = A
2 1 oveq2d ⊢ x = A → 1 … x = 1 … A
3 2 sumeq1d ⊢ x = A → ∑ n = 1 x Λ ⁡ n = ∑ n = 1 A Λ ⁡ n
4 df-chp ⊢ ψ = x ∈ ℝ ⟼ ∑ n = 1 x Λ ⁡ n
5 sumex ⊢ ∑ n = 1 A Λ ⁡ n ∈ V
6 3 4 5 fvmpt ⊢ A ∈ ℝ → ψ ⁡ A = ∑ n = 1 A Λ ⁡ n