pcxnn0cl

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

		Ref	Expression
	Assertion	pcxnn0cl	$⊢ (P \in ℙ \land N \in ℤ) \to P pCnt N \in ℕ_{0}^{*}$

Step	Hyp	Ref	Expression
1		pc0	$⊢ P \in ℙ \to P pCnt 0 = +∞$
2		pnf0xnn0	$⊢ +∞ \in ℕ_{0}^{*}$
3	1 2	eqeltrdi	$⊢ P \in ℙ \to P pCnt 0 \in ℕ_{0}^{*}$
4	3	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to P pCnt 0 \in ℕ_{0}^{*}$
5		oveq2	$⊢ N = 0 \to P pCnt N = P pCnt 0$
6	5	eleq1d	$⊢ N = 0 \to (P pCnt N \in ℕ_{0}^{} \leftrightarrow P pCnt 0 \in ℕ_{0}^{})$
7	4 6	syl5ibrcom	$⊢ (P \in ℙ \land N \in ℤ) \to (N = 0 \to P pCnt N \in ℕ_{0}^{*})$
8		pczcl	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N \in ℕ_{0}$
9	8	nn0xnn0d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N \in ℕ_{0}^{*}$
10	9	expr	$⊢ (P \in ℙ \land N \in ℤ) \to (N \neq 0 \to P pCnt N \in ℕ_{0}^{*})$
11	7 10	pm2.61dne	$⊢ (P \in ℙ \land N \in ℤ) \to P pCnt N \in ℕ_{0}^{*}$

Metamath Proof Explorer