Metamath Proof Explorer


Theorem ppi2

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

Ref Expression
Assertion ppi2
|- ( ppi ` 2 ) = 1

Proof

Step Hyp Ref Expression
1 1nn0
 |-  1 e. NN0
2 df-2
 |-  2 = ( 1 + 1 )
3 ppi1
 |-  ( ppi ` 1 ) = 0
4 2prm
 |-  2 e. Prime
5 1 2 3 4 ppi1i
 |-  ( ppi ` 2 ) = ( 0 + 1 )
6 1e0p1
 |-  1 = ( 0 + 1 )
7 5 6 eqtr4i
 |-  ( ppi ` 2 ) = 1