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 ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 1 ) = 0 )

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 ax-1ne0 ⊢ 1 ≠ 0
3 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < )
4 3 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 1 ∈ ℤ ∧ 1 ≠ 0 ) ) → ( 𝑃 pCnt 1 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) )
5 1 2 4 mpanr12 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 1 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) )
6 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
7 eqid ⊢ 1 = 1
8 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 }
9 8 3 pcpre1 ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 = 1 ) → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = 0 )
10 6 7 9 sylancl ⊢ ( 𝑃 ∈ ℙ → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 1 } , ℝ , < ) = 0 )
11 5 10 eqtrd ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 1 ) = 0 )