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	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		ppicl	⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ∈ ℕ0 )
3	2	nn0zd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ∈ ℤ )
4		ppi2	⊢ ( π ‘ 2 ) = 1
5		2re	⊢ 2 ∈ ℝ
6		ppiwordi	⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 2 ) ≤ ( π ‘ 𝐴 ) )
7	5 6	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 2 ) ≤ ( π ‘ 𝐴 ) )
8	4 7	eqbrtrrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 1 ≤ ( π ‘ 𝐴 ) )
9		elnnz1	⊢ ( ( π ‘ 𝐴 ) ∈ ℕ ↔ ( ( π ‘ 𝐴 ) ∈ ℤ ∧ 1 ≤ ( π ‘ 𝐴 ) ) )
10	3 8 9	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ∈ ℕ )