Theorem prmdvdssqOLD

Description: Obsolete version of prmdvdssq as of 21-Aug-2024. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	prmdvdssqOLD	$$⊢\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		zcn	$$⊢M\in \mathbb{Z}\to M\in ℂ$$
2	1	sqvald	$$⊢M\in \mathbb{Z}\to M^2=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
3	2	breq2d	$$⊢M\in \mathbb{Z}\to \left(P\parallel M^2\leftrightarrow P\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
4	3	adantl	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel M^2\leftrightarrow P\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
5		euclemma	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\leftrightarrow \left(P\parallel M\vee P\parallel M\right)\right)$$
6	5	3anidm23	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\leftrightarrow \left(P\parallel M\vee P\parallel M\right)\right)$$
7		oridm	$$⊢\left(P\parallel M\vee P\parallel M\right)\leftrightarrow P\parallel M$$
8	6 7	bitrdi	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\leftrightarrow P\parallel M\right)$$
9	4 8	bitr2d	$$⊢\left(P\in \mathbb{P}\wedge M\in \mathbb{Z}\right)\to \left(P\parallel M\leftrightarrow P\parallel M^2\right)$$