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

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		1nn0	⊢ 1 ∈ ℕ0
3		pcdvdsb	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( 1 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 1 ) ∥ 𝑁 ) )
4	2 3	mp3an3	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 1 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 1 ) ∥ 𝑁 ) )
5	1 4	sylan2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 1 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 ↑ 1 ) ∥ 𝑁 ) )
6		pccl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
7		elnnnn0c	⊢ ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 ∧ 1 ≤ ( 𝑃 pCnt 𝑁 ) ) )
8	7	baibr	⊢ ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 → ( 1 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) )
9	6 8	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 1 ≤ ( 𝑃 pCnt 𝑁 ) ↔ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) )
10		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
11	10	nncnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
12	11	exp1d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
13	12	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ↑ 1 ) = 𝑃 )
14	13	breq1d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 ↑ 1 ) ∥ 𝑁 ↔ 𝑃 ∥ 𝑁 ) )
15	5 9 14	3bitr3d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )