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 e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` 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 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
4 df-chp
 |-  psi = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
5 sumex
 |-  sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) e. _V
6 3 4 5 fvmpt
 |-  ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )