Theorem pcxcl

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

	Ref	Expression
Assertion	pcxcl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℝ* )

Proof

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