Theorem chpvalz

Description: Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021)

	Ref	Expression
Assertion	chpvalz	|- ( N e. ZZ -> ( psi ` N ) = sum_ n e. ( 1 ... N ) ( Lam ` n ) )

Proof

Step	Hyp	Ref	Expression
1		zre	|- ( N e. ZZ -> N e. RR )
2		chpval	|- ( N e. RR -> ( psi ` N ) = sum_ n e. ( 1 ... ( |_ ` N ) ) ( Lam ` n ) )
3	1 2	syl	|- ( N e. ZZ -> ( psi ` N ) = sum_ n e. ( 1 ... ( |_ ` N ) ) ( Lam ` n ) )
4		flid	|- ( N e. ZZ -> ( |_ ` N ) = N )
5	4	oveq2d	|- ( N e. ZZ -> ( 1 ... ( |_ ` N ) ) = ( 1 ... N ) )
6	5	sumeq1d	|- ( N e. ZZ -> sum_ n e. ( 1 ... ( |_ ` N ) ) ( Lam ` n ) = sum_ n e. ( 1 ... N ) ( Lam ` n ) )
7	3 6	eqtrd	|- ( N e. ZZ -> ( psi ` N ) = sum_ n e. ( 1 ... N ) ( Lam ` n ) )