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 )