Theorem ppi2

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

	Ref	Expression
Assertion	ppi2	⊢ ( π ‘ 2 ) = 1

Proof

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