Theorem dvdssqnn

Description: Two positive integers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by AV, 16-Sep-2026)

	Ref	Expression
Assertion	dvdssqnn	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		dvdsexpnn	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
3	1 2	mp3an3	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )