This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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