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 ⊢ P ∈ ℙ ∧ N ∈ ℤ → P pCnt N ∈ ℕ 0 *

Proof

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