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=1AΛn

Proof

Step Hyp Ref Expression
1 fveq2 x=Ax=A
2 1 oveq2d x=A1x=1A
3 2 sumeq1d x=An=1xΛn=n=1AΛn
4 df-chp ψ=xn=1xΛn
5 sumex n=1AΛnV
6 3 4 5 fvmpt AψA=n=1AΛn