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 ↔ ¬ 𝑃 ∥ 𝑁 ) )