This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary prime number theory Coprimality and Euclid's lemma (cont.) prmdvdssq
Description: Condition for a prime dividing a square. (Contributed by Scott Fenton , 8-Apr-2014) (Revised by Mario Carneiro , 19-Apr-2014) (Proof shortened by SN , 21-Aug-2024)
Ref
Expression
Assertion
prmdvdssq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ 𝑀 ↔ 𝑃 ∥ ( 𝑀 ↑ 2 ) ) )
Proof
Step
Hyp
Ref
Expression
1
2nn ⊢ 2 ∈ ℕ
2
prmdvdsexp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑀 ↑ 2 ) ↔ 𝑃 ∥ 𝑀 ) )
3
1 2
mp3an3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 ↑ 2 ) ↔ 𝑃 ∥ 𝑀 ) )
4
3
bicomd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ 𝑀 ↔ 𝑃 ∥ ( 𝑀 ↑ 2 ) ) )