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 ) ) |
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 ) ) |