Theorem ppif

Description: Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	ppif	|- ppi : RR --> NN0

Proof

Step	Hyp	Ref	Expression
1		df-ppi	|- ppi = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )
2		ppifi	|- ( x e. RR -> ( ( 0 [,] x ) i^i Prime ) e. Fin )
3		hashcl	|- ( ( ( 0 [,] x ) i^i Prime ) e. Fin -> ( # ` ( ( 0 [,] x ) i^i Prime ) ) e. NN0 )
4	2 3	syl	|- ( x e. RR -> ( # ` ( ( 0 [,] x ) i^i Prime ) ) e. NN0 )
5	1 4	fmpti	|- ppi : RR --> NN0