Theorem ppifl

Description: The prime-counting function ppi does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014)

	Ref	Expression
Assertion	ppifl	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(⌊A⌋\right)=\underset{\_}{\pi }\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ppisval	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
2	1	fveq2d	$$⊢A\in ℝ\to \left|\left[0,A\right]\cap \mathbb{P}\right|=\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|$$
3		ppival	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
4		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
5		ppival2	$$⊢⌊A⌋\in \mathbb{Z}\to \underset{\_}{\pi }\left(⌊A⌋\right)=\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|$$
6	4 5	syl	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(⌊A⌋\right)=\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|$$
7	2 3 6	3eqtr4rd	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(⌊A⌋\right)=\underset{\_}{\pi }\left(A\right)$$