Theorem ppival2g

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

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

Proof

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