Metamath Proof Explorer


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