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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ 𝑀 ↔ 𝑃 ∥ ( 𝑀 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
2	1	sqvald	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
3	2	breq2d	⊢ ( 𝑀 ∈ ℤ → ( 𝑃 ∥ ( 𝑀 ↑ 2 ) ↔ 𝑃 ∥ ( 𝑀 · 𝑀 ) ) )
4	3	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 ↑ 2 ) ↔ 𝑃 ∥ ( 𝑀 · 𝑀 ) ) )
5		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑀 ) ↔ ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑀 ) ) )
6	5	3anidm23	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑀 ) ↔ ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑀 ) ) )
7		oridm	⊢ ( ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑀 ) ↔ 𝑃 ∥ 𝑀 )
8	6 7	bitrdi	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑀 ) ↔ 𝑃 ∥ 𝑀 ) )
9	4 8	bitr2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ 𝑀 ↔ 𝑃 ∥ ( 𝑀 ↑ 2 ) ) )