Metamath Proof Explorer

Theorem ppicl

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

Ref Expression
Assertion ppicl 
|- ( A e. RR -> ( ppi ` A ) e. NN0 )

Proof

Step Hyp Ref Expression
1 ppif 
 |-  ppi : RR --> NN0
2 1 ffvelrni 
 |-  ( A e. RR -> ( ppi ` A ) e. NN0 )