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 
|- ( ( P e. Prime /\ N e. QQ ) -> ( P pCnt N ) e. RR* )

Proof

Step Hyp Ref Expression
1 pc0 
 |-  ( P e. Prime -> ( P pCnt 0 ) = +oo )
2 pnfxr 
 |-  +oo e. RR*
3 1 2 eqeltrdi 
 |-  ( P e. Prime -> ( P pCnt 0 ) e. RR* )
4 3 adantr 
 |-  ( ( P e. Prime /\ N e. QQ ) -> ( P pCnt 0 ) e. RR* )
5 oveq2 
 |-  ( N = 0 -> ( P pCnt N ) = ( P pCnt 0 ) )
6 5 eleq1d 
 |-  ( N = 0 -> ( ( P pCnt N ) e. RR* <-> ( P pCnt 0 ) e. RR* ) )
7 4 6 syl5ibrcom 
 |-  ( ( P e. Prime /\ N e. QQ ) -> ( N = 0 -> ( P pCnt N ) e. RR* ) )
8 pcqcl 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. ZZ )
9 8 zred 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. RR )
10 9 rexrd 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. RR* )
11 10 expr 
 |-  ( ( P e. Prime /\ N e. QQ ) -> ( N =/= 0 -> ( P pCnt N ) e. RR* ) )
12 7 11 pm2.61dne 
 |-  ( ( P e. Prime /\ N e. QQ ) -> ( P pCnt N ) e. RR* )