Metamath Proof Explorer

Theorem pcxnn0cl

Description: Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024)

Ref Expression
Assertion pcxnn0cl ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* )

Proof

Step Hyp Ref Expression
1 pc0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )
2 pnf0xnn0 ⊢ +∞ ∈ ℕ0*
3 1 2 eqeltrdi ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) ∈ ℕ0* )
4 3 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 pCnt 0 ) ∈ ℕ0* )
5 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt 0 ) )
6 5 eleq1d ⊢ ( 𝑁 = 0 → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* ↔ ( 𝑃 pCnt 0 ) ∈ ℕ0* ) )
7 4 6 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 = 0 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* ) )
8 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
9 8 nn0xnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* )
10 9 expr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≠ 0 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* ) )
11 7 10 pm2.61dne ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0* )