Theorem ppival2

Description: Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014)

	Ref	Expression
Assertion	ppival2	$$⊢A\in \mathbb{Z}\to \underset{\_}{\pi }\left(A\right)=\left|\left(2\dots A\right)\cap \mathbb{P}\right|$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
2		ppival	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
3	1 2	syl	$$⊢A\in \mathbb{Z}\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
4		ppisval	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
5	1 4	syl	$$⊢A\in \mathbb{Z}\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
6		flid	$$⊢A\in \mathbb{Z}\to ⌊A⌋=A$$
7	6	oveq2d	$$⊢A\in \mathbb{Z}\to \left(2\dots ⌊A⌋\right)=\left(2\dots A\right)$$
8	7	ineq1d	$$⊢A\in \mathbb{Z}\to \left(2\dots ⌊A⌋\right)\cap \mathbb{P}=\left(2\dots A\right)\cap \mathbb{P}$$
9	5 8	eqtrd	$$⊢A\in \mathbb{Z}\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots A\right)\cap \mathbb{P}$$
10	9	fveq2d	$$⊢A\in \mathbb{Z}\to \left|\left[0,A\right]\cap \mathbb{P}\right|=\left|\left(2\dots A\right)\cap \mathbb{P}\right|$$
11	3 10	eqtrd	$$⊢A\in \mathbb{Z}\to \underset{\_}{\pi }\left(A\right)=\left|\left(2\dots A\right)\cap \mathbb{P}\right|$$