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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → 0 ≤ ( 𝑃 pCnt 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		0lepnf	⊢ 0 ≤ +∞
2		oveq2	⊢ ( 𝑁 = 0 → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt 0 ) )
3		pc0	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )
4	3	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 pCnt 0 ) = +∞ )
5	2 4	sylan9eqr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝑃 pCnt 𝑁 ) = +∞ )
6	1 5	breqtrrid	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → 0 ≤ ( 𝑃 pCnt 𝑁 ) )
7		pczcl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
8	7	nn0ge0d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 0 ≤ ( 𝑃 pCnt 𝑁 ) )
9	8	anassrs	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → 0 ≤ ( 𝑃 pCnt 𝑁 ) )
10	6 9	pm2.61dane	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → 0 ≤ ( 𝑃 pCnt 𝑁 ) )