Metamath Proof Explorer

Theorem 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 ⊢ P ∈ ℙ ∧ M ∈ ℤ → P ∥ M ↔ P ∥ M 2

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 prmdvdsexp ⊢ P ∈ ℙ ∧ M ∈ ℤ ∧ 2 ∈ ℕ → P ∥ M 2 ↔ P ∥ M
3 1 2 mp3an3 ⊢ P ∈ ℙ ∧ M ∈ ℤ → P ∥ M 2 ↔ P ∥ M
4 3 bicomd ⊢ P ∈ ℙ ∧ M ∈ ℤ → P ∥ M ↔ P ∥ M 2