This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pc1

Description: Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pc1 ⊢ P ∈ ℙ → P pCnt 1 = 0

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 ax-1ne0 ⊢ 1 ≠ 0
3 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ 1 ℝ < = sup n ∈ ℕ 0 | P n ∥ 1 ℝ <
4 3 pczpre ⊢ P ∈ ℙ ∧ 1 ∈ ℤ ∧ 1 ≠ 0 → P pCnt 1 = sup n ∈ ℕ 0 | P n ∥ 1 ℝ <
5 1 2 4 mpanr12 ⊢ P ∈ ℙ → P pCnt 1 = sup n ∈ ℕ 0 | P n ∥ 1 ℝ <
6 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
7 eqid ⊢ 1 = 1
8 eqid ⊢ n ∈ ℕ 0 | P n ∥ 1 = n ∈ ℕ 0 | P n ∥ 1
9 8 3 pcpre1 ⊢ P ∈ ℤ ≥ 2 ∧ 1 = 1 → sup n ∈ ℕ 0 | P n ∥ 1 ℝ < = 0
10 6 7 9 sylancl ⊢ P ∈ ℙ → sup n ∈ ℕ 0 | P n ∥ 1 ℝ < = 0
11 5 10 eqtrd ⊢ P ∈ ℙ → P pCnt 1 = 0