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

Metamath Proof Explorer

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