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

Step	Hyp	Ref	Expression
1		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		pcdvdsb	$⊢ (P \in ℙ \land N \in ℤ \land 1 \in ℕ_{0}) \to (1 \leq P pCnt N \leftrightarrow P^{1} ∥ N)$
4	2 3	mp3an3	$⊢ (P \in ℙ \land N \in ℤ) \to (1 \leq P pCnt N \leftrightarrow P^{1} ∥ N)$
5	1 4	sylan2	$⊢ (P \in ℙ \land N \in ℕ) \to (1 \leq P pCnt N \leftrightarrow P^{1} ∥ N)$
6		pccl	$⊢ (P \in ℙ \land N \in ℕ) \to P pCnt N \in ℕ_{0}$
7		elnnnn0c	$⊢ P pCnt N \in ℕ \leftrightarrow (P pCnt N \in ℕ_{0} \land 1 \leq P pCnt N)$
8	7	baibr	$⊢ P pCnt N \in ℕ_{0} \to (1 \leq P pCnt N \leftrightarrow P pCnt N \in ℕ)$
9	6 8	syl	$⊢ (P \in ℙ \land N \in ℕ) \to (1 \leq P pCnt N \leftrightarrow P pCnt N \in ℕ)$
10		prmnn	$⊢ P \in ℙ \to P \in ℕ$
11	10	nncnd	$⊢ P \in ℙ \to P \in ℂ$
12	11	exp1d	$⊢ P \in ℙ \to P^{1} = P$
13	12	adantr	$⊢ (P \in ℙ \land N \in ℕ) \to P^{1} = P$
14	13	breq1d	$⊢ (P \in ℙ \land N \in ℕ) \to (P^{1} ∥ N \leftrightarrow P ∥ N)$
15	5 9 14	3bitr3d	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$

Metamath Proof Explorer