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

Proof

Step Hyp Ref Expression
1 pcelnn ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ ↔ P ∥ N
2 pccl ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ 0
3 nnne0 ⊢ P pCnt N ∈ ℕ → P pCnt N ≠ 0
4 elnn0 ⊢ P pCnt N ∈ ℕ 0 ↔ P pCnt N ∈ ℕ ∨ P pCnt N = 0
5 4 biimpi ⊢ P pCnt N ∈ ℕ 0 → P pCnt N ∈ ℕ ∨ P pCnt N = 0
6 5 ord ⊢ P pCnt N ∈ ℕ 0 → ¬ P pCnt N ∈ ℕ → P pCnt N = 0
7 6 necon1ad ⊢ P pCnt N ∈ ℕ 0 → P pCnt N ≠ 0 → P pCnt N ∈ ℕ
8 3 7 impbid2 ⊢ P pCnt N ∈ ℕ 0 → P pCnt N ∈ ℕ ↔ P pCnt N ≠ 0
9 2 8 syl ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N ∈ ℕ ↔ P pCnt N ≠ 0
10 1 9 bitr3d ⊢ P ∈ ℙ ∧ N ∈ ℕ → P ∥ N ↔ P pCnt N ≠ 0
11 10 necon2bbid ⊢ P ∈ ℙ ∧ N ∈ ℕ → P pCnt N = 0 ↔ ¬ P ∥ N