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

Proof

Step	Hyp	Ref	Expression
1		prmz	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
2		prmdvdsexp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) ↔ 𝑃 ∥ 𝑄 ) )
3	1 2	syl3an2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) ↔ 𝑃 ∥ 𝑄 ) )
4		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
5		dvdsprm	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℙ ) → ( 𝑃 ∥ 𝑄 ↔ 𝑃 = 𝑄 ) )
6	4 5	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 ∥ 𝑄 ↔ 𝑃 = 𝑄 ) )
7	6	3adant3	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ 𝑄 ↔ 𝑃 = 𝑄 ) )
8	3 7	bitrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) ↔ 𝑃 = 𝑄 ) )