ppi1

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

		Ref	Expression
	Assertion	ppi1	$⊢ \underline{π} (1) = 0$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		ppival2	$⊢ 1 \in ℤ \to \underline{π} (1) = \|(2 \dots 1) \cap ℙ\|$
3	1 2	ax-mp	$⊢ \underline{π} (1) = \|(2 \dots 1) \cap ℙ\|$
4		1lt2	$⊢ 1 < 2$
5		2z	$⊢ 2 \in ℤ$
6		fzn	$⊢ (2 \in ℤ \land 1 \in ℤ) \to (1 < 2 \leftrightarrow (2 \dots 1) = \emptyset)$
7	5 1 6	mp2an	$⊢ 1 < 2 \leftrightarrow (2 \dots 1) = \emptyset$
8	4 7	mpbi	$⊢ (2 \dots 1) = \emptyset$
9	8	ineq1i	$⊢ (2 \dots 1) \cap ℙ = \emptyset \cap ℙ$
10		0in	$⊢ \emptyset \cap ℙ = \emptyset$
11	9 10	eqtri	$⊢ (2 \dots 1) \cap ℙ = \emptyset$
12	11	fveq2i	$⊢ \|(2 \dots 1) \cap ℙ\| = \|\emptyset\|$
13		hash0	$⊢ \|\emptyset\| = 0$
14	12 13	eqtri	$⊢ \|(2 \dots 1) \cap ℙ\| = 0$
15	3 14	eqtri	$⊢ \underline{π} (1) = 0$

Metamath Proof Explorer