# Metamath Proof Explorer

## Theorem pcelnn

Description: There are a positive number of powers of a prime P in N iff P divides N . (Contributed by Mario Carneiro, 23-Feb-2014)

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

### Proof

Step Hyp Ref Expression
1 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
2 1nn0 ${⊢}1\in {ℕ}_{0}$
3 pcdvdsb ${⊢}\left({P}\in ℙ\wedge {N}\in ℤ\wedge 1\in {ℕ}_{0}\right)\to \left(1\le {P}\mathrm{pCnt}{N}↔{{P}}^{1}\parallel {N}\right)$
4 2 3 mp3an3 ${⊢}\left({P}\in ℙ\wedge {N}\in ℤ\right)\to \left(1\le {P}\mathrm{pCnt}{N}↔{{P}}^{1}\parallel {N}\right)$
5 1 4 sylan2 ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left(1\le {P}\mathrm{pCnt}{N}↔{{P}}^{1}\parallel {N}\right)$
6 pccl ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to {P}\mathrm{pCnt}{N}\in {ℕ}_{0}$
7 elnnnn0c ${⊢}{P}\mathrm{pCnt}{N}\in ℕ↔\left({P}\mathrm{pCnt}{N}\in {ℕ}_{0}\wedge 1\le {P}\mathrm{pCnt}{N}\right)$
8 7 baibr ${⊢}{P}\mathrm{pCnt}{N}\in {ℕ}_{0}\to \left(1\le {P}\mathrm{pCnt}{N}↔{P}\mathrm{pCnt}{N}\in ℕ\right)$
9 6 8 syl ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left(1\le {P}\mathrm{pCnt}{N}↔{P}\mathrm{pCnt}{N}\in ℕ\right)$
10 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
11 10 nncnd ${⊢}{P}\in ℙ\to {P}\in ℂ$
12 11 exp1d ${⊢}{P}\in ℙ\to {{P}}^{1}={P}$
13 12 adantr ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to {{P}}^{1}={P}$
14 13 breq1d ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({{P}}^{1}\parallel {N}↔{P}\parallel {N}\right)$
15 5 9 14 3bitr3d ${⊢}\left({P}\in ℙ\wedge {N}\in ℕ\right)\to \left({P}\mathrm{pCnt}{N}\in ℕ↔{P}\parallel {N}\right)$