pcxcl

Description: Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014)

		Ref	Expression
	Assertion	pcxcl	$⊢ (P \in ℙ \land N \in ℚ) \to P pCnt N \in ℝ^{*}$

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

Metamath Proof Explorer