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	⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2		chpval	⊢ ( 𝑁 ∈ ℝ → ( ψ ‘ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( Λ ‘ 𝑛 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( Λ ‘ 𝑛 ) )
4		flid	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
5	4	oveq2d	⊢ ( 𝑁 ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑁 ) ) = ( 1 ... 𝑁 ) )
6	5	sumeq1d	⊢ ( 𝑁 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( Λ ‘ 𝑛 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑛 ) )
7	3 6	eqtrd	⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑛 ) )