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