# 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}\in ℙ\to {P}\mathrm{pCnt}1=0$

### Proof

Step Hyp Ref Expression
1 1z ${⊢}1\in ℤ$
2 ax-1ne0 ${⊢}1\ne 0$
3 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)$
4 3 pczpre ${⊢}\left({P}\in ℙ\wedge \left(1\in ℤ\wedge 1\ne 0\right)\right)\to {P}\mathrm{pCnt}1=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)$
5 1 2 4 mpanr12 ${⊢}{P}\in ℙ\to {P}\mathrm{pCnt}1=sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)$
6 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
7 eqid ${⊢}1=1$
8 eqid ${⊢}\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\}=\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\}$
9 8 3 pcpre1 ${⊢}\left({P}\in {ℤ}_{\ge 2}\wedge 1=1\right)\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)=0$
10 6 7 9 sylancl ${⊢}{P}\in ℙ\to sup\left(\left\{{n}\in {ℕ}_{0}|{{P}}^{{n}}\parallel 1\right\},ℝ,<\right)=0$
11 5 10 eqtrd ${⊢}{P}\in ℙ\to {P}\mathrm{pCnt}1=0$