Theorem chpf

Description: Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	chpf	$$⊢\psi :ℝ⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		df-chp	$$⊢\psi =\left(x\in ℝ⟼\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\right)$$
2		fzfid	$$⊢x\in ℝ\to \left(1\dots ⌊x⌋\right)\in \mathrm{Fin}$$
3		elfznn	$$⊢n\in \left(1\dots ⌊x⌋\right)\to n\in \mathbb{N}$$
4	3	adantl	$$⊢\left(x\in ℝ\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to n\in \mathbb{N}$$
5		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
6	4 5	syl	$$⊢\left(x\in ℝ\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\in ℝ$$
7	2 6	fsumrecl	$$⊢x\in ℝ\to \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\in ℝ$$
8	1 7	fmpti	$$⊢\psi :ℝ⟶ℝ$$