Theorem ppival

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

	Ref	Expression
Assertion	ppival	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \left[0,x\right]=\left[0,A\right]$$
2	1	ineq1d	$$⊢x=A\to \left[0,x\right]\cap \mathbb{P}=\left[0,A\right]\cap \mathbb{P}$$
3	2	fveq2d	$$⊢x=A\to \left|\left[0,x\right]\cap \mathbb{P}\right|=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
4		df-ppi	$$⊢\underset{\_}{\pi }=\left(x\in ℝ⟼\left|\left[0,x\right]\cap \mathbb{P}\right|\right)$$
5		fvex	$$⊢\left|\left[0,A\right]\cap \mathbb{P}\right|\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$