Theorem chpfl

Description: The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016)

	Ref	Expression
Assertion	chpfl	$$⊢A\in ℝ\to \psi \left(⌊A⌋\right)=\psi \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		flidm	$$⊢A\in ℝ\to ⌊⌊A⌋⌋=⌊A⌋$$
2	1	oveq2d	$$⊢A\in ℝ\to \left(1\dots ⌊⌊A⌋⌋\right)=\left(1\dots ⌊A⌋\right)$$
3	2	sumeq1d	$$⊢A\in ℝ\to \sum _{x=1}^{⌊⌊A⌋⌋}\Lambda \left(x\right)=\sum _{x=1}^{⌊A⌋}\Lambda \left(x\right)$$
4		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
5		chpval	$$⊢⌊A⌋\in ℝ\to \psi \left(⌊A⌋\right)=\sum _{x=1}^{⌊⌊A⌋⌋}\Lambda \left(x\right)$$
6	4 5	syl	$$⊢A\in ℝ\to \psi \left(⌊A⌋\right)=\sum _{x=1}^{⌊⌊A⌋⌋}\Lambda \left(x\right)$$
7		chpval	$$⊢A\in ℝ\to \psi \left(A\right)=\sum _{x=1}^{⌊A⌋}\Lambda \left(x\right)$$
8	3 6 7	3eqtr4d	$$⊢A\in ℝ\to \psi \left(⌊A⌋\right)=\psi \left(A\right)$$