Theorem pc1

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

	Ref	Expression
Assertion	pc1	$$⊢P\in \mathbb{P}\to P\mathrm{pCnt}1=0$$

Proof

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