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

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 ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) = 0 ↔ ¬ 𝑃 ∥ 𝑁 ) )

Proof

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