Theorem ppi3

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

	Ref	Expression
Assertion	ppi3	⊢ ( π ‘ 3 ) = 2

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		df-3	⊢ 3 = ( 2 + 1 )
3		ppi2	⊢ ( π ‘ 2 ) = 1
4		3prm	⊢ 3 ∈ ℙ
5	1 2 3 4	ppi1i	⊢ ( π ‘ 3 ) = ( 1 + 1 )
6		df-2	⊢ 2 = ( 1 + 1 )
7	5 6	eqtr4i	⊢ ( π ‘ 3 ) = 2