Theorem ppi3

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

	Ref	Expression
Assertion	ppi3	|- ( ppi ` 3 ) = 2

Proof

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