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 \in ℙ \land N \in ℤ) \to 0 \leq P pCnt N$

Step	Hyp	Ref	Expression
1		0lepnf	$⊢ 0 \leq +∞$
2		oveq2	$⊢ N = 0 \to P pCnt N = P pCnt 0$
3		pc0	$⊢ P \in ℙ \to P pCnt 0 = +∞$
4	3	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to P pCnt 0 = +∞$
5	2 4	sylan9eqr	$⊢ ((P \in ℙ \land N \in ℤ) \land N = 0) \to P pCnt N = +∞$
6	1 5	breqtrrid	$⊢ ((P \in ℙ \land N \in ℤ) \land N = 0) \to 0 \leq P pCnt N$
7		pczcl	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N \in ℕ_{0}$
8	7	nn0ge0d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to 0 \leq P pCnt N$
9	8	anassrs	$⊢ ((P \in ℙ \land N \in ℤ) \land N \neq 0) \to 0 \leq P pCnt N$
10	6 9	pm2.61dane	$⊢ (P \in ℙ \land N \in ℤ) \to 0 \leq P pCnt N$

Metamath Proof Explorer