Metamath Proof Explorer

Theorem prmdvdsexpb

Description: A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012) (Revised by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion prmdvdsexpb ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ N ∈ ℕ → P ∥ Q N ↔ P = Q

Proof

Step Hyp Ref Expression
1 prmz ⊢ Q ∈ ℙ → Q ∈ ℤ
2 prmdvdsexp ⊢ P ∈ ℙ ∧ Q ∈ ℤ ∧ N ∈ ℕ → P ∥ Q N ↔ P ∥ Q
3 1 2 syl3an2 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ N ∈ ℕ → P ∥ Q N ↔ P ∥ Q
4 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
5 dvdsprm ⊢ P ∈ ℤ ≥ 2 ∧ Q ∈ ℙ → P ∥ Q ↔ P = Q
6 4 5 sylan ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P ∥ Q ↔ P = Q
7 6 3adant3 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ N ∈ ℕ → P ∥ Q ↔ P = Q
8 3 7 bitrd ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ N ∈ ℕ → P ∥ Q N ↔ P = Q