Metamath Proof Explorer

Theorem pcxnn0cl

Description: Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024)

Ref Expression
Assertion pcxnn0cl 
|- ( ( P e. Prime /\ N e. ZZ ) -> ( P pCnt N ) e. NN0* )

Proof

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