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 )