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 ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ ↔ P ∥ N

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 1nn0 ⊢ 1 ∈ ℕ 0
3 pcdvdsb ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ 1 ∈ ℕ 0 → 1 ≤ P pCnt N ↔ P 1 ∥ N
4 2 3 mp3an3 ⊢ P ∈ ℙ ∧ N ∈ ℤ → 1 ≤ P pCnt N ↔ P 1 ∥ N
5 1 4 sylan2 ⊢ P ∈ ℙ ∧ N ∈ ℕ → 1 ≤ P pCnt N ↔ P 1 ∥ N
6 pccl ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ 0
7 elnnnn0c ⊢ P pCnt N ∈ ℕ ↔ P pCnt N ∈ ℕ 0 ∧ 1 ≤ P pCnt N
8 7 baibr ⊢ P pCnt N ∈ ℕ 0 → 1 ≤ P pCnt N ↔ P pCnt N ∈ ℕ
9 6 8 syl ⊢ P ∈ ℙ ∧ N ∈ ℕ → 1 ≤ P pCnt N ↔ P pCnt N ∈ ℕ
10 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
11 10 nncnd ⊢ P ∈ ℙ → P ∈ ℂ
12 11 exp1d ⊢ P ∈ ℙ → P 1 = P
13 12 adantr ⊢ P ∈ ℙ ∧ N ∈ ℕ → P 1 = P
14 13 breq1d ⊢ P ∈ ℙ ∧ N ∈ ℕ → P 1 ∥ N ↔ P ∥ N
15 5 9 14 3bitr3d ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ ↔ P ∥ N