Metamath Proof Explorer

Theorem pcge0

Description: The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pcge0 
|- ( ( P e. Prime /\ N e. ZZ ) -> 0 <_ ( P pCnt N ) )

Proof

Step Hyp Ref Expression
1 0lepnf 
 |-  0 <_ +oo
2 oveq2 
 |-  ( N = 0 -> ( P pCnt N ) = ( P pCnt 0 ) )
3 pc0 
 |-  ( P e. Prime -> ( P pCnt 0 ) = +oo )
4 3 adantr 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P pCnt 0 ) = +oo )
5 2 4 sylan9eqr 
 |-  ( ( ( P e. Prime /\ N e. ZZ ) /\ N = 0 ) -> ( P pCnt N ) = +oo )
6 1 5 breqtrrid 
 |-  ( ( ( P e. Prime /\ N e. ZZ ) /\ N = 0 ) -> 0 <_ ( P pCnt N ) )
7 pczcl 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )
8 7 nn0ge0d 
 |-  ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> 0 <_ ( P pCnt N ) )
9 8 anassrs 
 |-  ( ( ( P e. Prime /\ N e. ZZ ) /\ N =/= 0 ) -> 0 <_ ( P pCnt N ) )
10 6 9 pm2.61dane 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> 0 <_ ( P pCnt N ) )