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	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(A\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ppicl	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)\in {\mathbb{N}}_0$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(A\right)\in {\mathbb{N}}_0$$
3	2	nn0zd	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(A\right)\in \mathbb{Z}$$
4		ppi2	$$⊢\underset{\_}{\pi }\left(2\right)=1$$
5		2re	$$⊢2\in ℝ$$
6		ppiwordi	$$⊢\left(2\in ℝ\wedge A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(2\right)\le \underset{\_}{\pi }\left(A\right)$$
7	5 6	mp3an1	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(2\right)\le \underset{\_}{\pi }\left(A\right)$$
8	4 7	eqbrtrrid	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to 1\le \underset{\_}{\pi }\left(A\right)$$
9		elnnz1	$$⊢\underset{\_}{\pi }\left(A\right)\in \mathbb{N}\leftrightarrow \left(\underset{\_}{\pi }\left(A\right)\in \mathbb{Z}\wedge 1\le \underset{\_}{\pi }\left(A\right)\right)$$
10	3 8 9	sylanbrc	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \underset{\_}{\pi }\left(A\right)\in \mathbb{N}$$