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 PN0PpCntN

Proof

Step Hyp Ref Expression
1 0lepnf 0+∞
2 oveq2 N=0PpCntN=PpCnt0
3 pc0 PPpCnt0=+∞
4 3 adantr PNPpCnt0=+∞
5 2 4 sylan9eqr PNN=0PpCntN=+∞
6 1 5 breqtrrid PNN=00PpCntN
7 pczcl PNN0PpCntN0
8 7 nn0ge0d PNN00PpCntN
9 8 anassrs PNN00PpCntN
10 6 9 pm2.61dane PN0PpCntN