This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppinncl

Description: Closure of the prime-counting function ppi in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppinncl 
|- ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) e. NN )

Proof

Step Hyp Ref Expression
1 ppicl 
 |-  ( A e. RR -> ( ppi ` A ) e. NN0 )
2 1 adantr 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) e. NN0 )
3 2 nn0zd 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) e. ZZ )
4 ppi2 
 |-  ( ppi ` 2 ) = 1
5 2re 
 |-  2 e. RR
6 ppiwordi 
 |-  ( ( 2 e. RR /\ A e. RR /\ 2 <_ A ) -> ( ppi ` 2 ) <_ ( ppi ` A ) )
7 5 6 mp3an1 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` 2 ) <_ ( ppi ` A ) )
8 4 7 eqbrtrrid 
 |-  ( ( A e. RR /\ 2 <_ A ) -> 1 <_ ( ppi ` A ) )
9 elnnz1 
 |-  ( ( ppi ` A ) e. NN <-> ( ( ppi ` A ) e. ZZ /\ 1 <_ ( ppi ` A ) ) )
10 3 8 9 sylanbrc 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) e. NN )