# Metamath Proof Explorer

## Theorem pceq0

Description: There are zero powers of a prime P in N iff P does not divide N . (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pceq0 ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\mathrm{pCnt}{N}=0↔¬{P}\parallel {N}\right)$

### Proof

Step Hyp Ref Expression
1 pcelnn ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\mathrm{pCnt}{N}\in ℕ↔{P}\parallel {N}\right)$
2 pccl ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to {P}\mathrm{pCnt}{N}\in {ℕ}_{0}$
3 nnne0 ${⊢}{P}\mathrm{pCnt}{N}\in ℕ\to {P}\mathrm{pCnt}{N}\ne 0$
4 elnn0 ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}↔\left({P}\mathrm{pCnt}{N}\in ℕ\vee {P}\mathrm{pCnt}{N}=0\right)$
5 4 biimpi ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}\to \left({P}\mathrm{pCnt}{N}\in ℕ\vee {P}\mathrm{pCnt}{N}=0\right)$
6 5 ord ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}\to \left(¬{P}\mathrm{pCnt}{N}\in ℕ\to {P}\mathrm{pCnt}{N}=0\right)$
7 6 necon1ad ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}\to \left({P}\mathrm{pCnt}{N}\ne 0\to {P}\mathrm{pCnt}{N}\in ℕ\right)$
8 3 7 impbid2 ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}\to \left({P}\mathrm{pCnt}{N}\in ℕ↔{P}\mathrm{pCnt}{N}\ne 0\right)$
9 2 8 syl ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\mathrm{pCnt}{N}\in ℕ↔{P}\mathrm{pCnt}{N}\ne 0\right)$
10 1 9 bitr3d ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\parallel {N}↔{P}\mathrm{pCnt}{N}\ne 0\right)$
11 10 necon2bbid ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\mathrm{pCnt}{N}=0↔¬{P}\parallel {N}\right)$