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	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel M\leftrightarrow P\parallel M^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		prmdvdsexp	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\wedge 2\in \mathbb{N}\right)\to \left(P\parallel M^2\leftrightarrow P\parallel M\right)$$
3	1 2	mp3an3	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel M^2\leftrightarrow P\parallel M\right)$$
4	3	bicomd	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel M\leftrightarrow P\parallel M^2\right)$$