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 ∈ ℝ ∧ 2 ≤ A → π _ ⁡ A ∈ ℕ

Proof

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