This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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