Theorem chtfl

Description: The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		flidm	$$⊢A\in ℝ\to ⌊⌊A⌋⌋=⌊A⌋$$
2	1	oveq2d	$$⊢A\in ℝ\to \left(2\dots ⌊⌊A⌋⌋\right)=\left(2\dots ⌊A⌋\right)$$
3	2	ineq1d	$$⊢A\in ℝ\to \left(2\dots ⌊⌊A⌋⌋\right)\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
4		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
5		ppisval	$$⊢⌊A⌋\in ℝ\to \left[0,⌊A⌋\right]\cap \mathbb{P}=\left(2\dots ⌊⌊A⌋⌋\right)\cap \mathbb{P}$$
6	4 5	syl	$$⊢A\in ℝ\to \left[0,⌊A⌋\right]\cap \mathbb{P}=\left(2\dots ⌊⌊A⌋⌋\right)\cap \mathbb{P}$$
7		ppisval	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
8	3 6 7	3eqtr4d	$$⊢A\in ℝ\to \left[0,⌊A⌋\right]\cap \mathbb{P}=\left[0,A\right]\cap \mathbb{P}$$
9	8	sumeq1d	$$⊢A\in ℝ\to \sum _{p\in \left[0,⌊A⌋\right]\cap \mathbb{P}}\log p=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$
10		chtval	$$⊢⌊A⌋\in ℝ\to \theta \left(⌊A⌋\right)=\sum _{p\in \left[0,⌊A⌋\right]\cap \mathbb{P}}\log p$$
11	4 10	syl	$$⊢A\in ℝ\to \theta \left(⌊A⌋\right)=\sum _{p\in \left[0,⌊A⌋\right]\cap \mathbb{P}}\log p$$
12		chtval	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$
13	9 11 12	3eqtr4d	$$⊢A\in ℝ\to \theta \left(⌊A⌋\right)=\theta \left(A\right)$$