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\in \mathbb{Z}\to \psi \left(N\right)=\sum _{n=1}^N\Lambda \left(n\right)$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
2		chpval	$$⊢N\in ℝ\to \psi \left(N\right)=\sum _{n=1}^{⌊N⌋}\Lambda \left(n\right)$$
3	1 2	syl	$$⊢N\in \mathbb{Z}\to \psi \left(N\right)=\sum _{n=1}^{⌊N⌋}\Lambda \left(n\right)$$
4		flid	$$⊢N\in \mathbb{Z}\to ⌊N⌋=N$$
5	4	oveq2d	$$⊢N\in \mathbb{Z}\to \left(1\dots ⌊N⌋\right)=\left(1\dots N\right)$$
6	5	sumeq1d	$$⊢N\in \mathbb{Z}\to \sum _{n=1}^{⌊N⌋}\Lambda \left(n\right)=\sum _{n=1}^N\Lambda \left(n\right)$$
7	3 6	eqtrd	$$⊢N\in \mathbb{Z}\to \psi \left(N\right)=\sum _{n=1}^N\Lambda \left(n\right)$$