Metamath Proof Explorer


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 𝑁 ) ∈ ℝ* )