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