This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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