Theorem ppi2

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

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

Proof

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