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