This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppi3

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

		Ref	Expression
	Assertion	ppi3	$⊢ \underline{π} (3) = 2$

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		df-3	$⊢ 3 = 2 + 1$
3		ppi2	$⊢ \underline{π} (2) = 1$
4		3prm	$⊢ 3 \in ℙ$
5	1 2 3 4	ppi1i	$⊢ \underline{π} (3) = 1 + 1$
6		df-2	$⊢ 2 = 1 + 1$
7	5 6	eqtr4i	$⊢ \underline{π} (3) = 2$