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 \in ℙ \land N \in ℕ) \to (P pCnt N = 0 \leftrightarrow \neg P ∥ N)$

Step	Hyp	Ref	Expression
1		pcelnn	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
2		pccl	$⊢ (P \in ℙ \land N \in ℕ) \to P pCnt N \in ℕ_{0}$
3		nnne0	$⊢ P pCnt N \in ℕ \to P pCnt N \neq 0$
4		elnn0	$⊢ P pCnt N \in ℕ_{0} \leftrightarrow (P pCnt N \in ℕ \lor P pCnt N = 0)$
5	4	biimpi	$⊢ P pCnt N \in ℕ_{0} \to (P pCnt N \in ℕ \lor P pCnt N = 0)$
6	5	ord	$⊢ P pCnt N \in ℕ_{0} \to (\neg P pCnt N \in ℕ \to P pCnt N = 0)$
7	6	necon1ad	$⊢ P pCnt N \in ℕ_{0} \to (P pCnt N \neq 0 \to P pCnt N \in ℕ)$
8	3 7	impbid2	$⊢ P pCnt N \in ℕ_{0} \to (P pCnt N \in ℕ \leftrightarrow P pCnt N \neq 0)$
9	2 8	syl	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P pCnt N \neq 0)$
10	1 9	bitr3d	$⊢ (P \in ℙ \land N \in ℕ) \to (P ∥ N \leftrightarrow P pCnt N \neq 0)$
11	10	necon2bbid	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N = 0 \leftrightarrow \neg P ∥ N)$

Metamath Proof Explorer