Theorem ppi1

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

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

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		ppival2	$$⊢1\in \mathbb{Z}\to \underset{\_}{\pi }\left(1\right)=\left|\left(2\dots 1\right)\cap \mathbb{P}\right|$$
3	1 2	ax-mp	$$⊢\underset{\_}{\pi }\left(1\right)=\left|\left(2\dots 1\right)\cap \mathbb{P}\right|$$
4		1lt2	$$⊢1<2$$
5		2z	$$⊢2\in \mathbb{Z}$$
6		fzn	$$⊢\left(2\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(1<2\leftrightarrow \left(2\dots 1\right)=\varnothing \right)$$
7	5 1 6	mp2an	$$⊢1<2\leftrightarrow \left(2\dots 1\right)=\varnothing$$
8	4 7	mpbi	$$⊢\left(2\dots 1\right)=\varnothing$$
9	8	ineq1i	$$⊢\left(2\dots 1\right)\cap \mathbb{P}=\varnothing \cap \mathbb{P}$$
10		0in	$$⊢\varnothing \cap \mathbb{P}=\varnothing$$
11	9 10	eqtri	$$⊢\left(2\dots 1\right)\cap \mathbb{P}=\varnothing$$
12	11	fveq2i	$$⊢\left|\left(2\dots 1\right)\cap \mathbb{P}\right|=\left|\varnothing \right|$$
13		hash0	$$⊢\left|\varnothing \right|=0$$
14	12 13	eqtri	$$⊢\left|\left(2\dots 1\right)\cap \mathbb{P}\right|=0$$
15	3 14	eqtri	$$⊢\underset{\_}{\pi }\left(1\right)=0$$