Theorem ppi3

Description: The prime-counting function ppi at 3 . (Contributed by Mario Carneiro, 21-Sep-2014)

	Ref	Expression
Assertion	ppi3	$$⊢\underset{\_}{\pi }\left(3\right)=2$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		df-3	$$⊢3=2+1$$
3		ppi2	$$⊢\underset{\_}{\pi }\left(2\right)=1$$
4		3prm	$$⊢3\in \mathbb{P}$$
5	1 2 3 4	ppi1i	$$⊢\underset{\_}{\pi }\left(3\right)=1+1$$
6		df-2	$$⊢2=1+1$$
7	5 6	eqtr4i	$$⊢\underset{\_}{\pi }\left(3\right)=2$$