Theorem absdvdsabsb

Description: Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024)

	Ref	Expression
Assertion	absdvdsabsb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		absdvdsb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) )
2		zabscl	⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) ∈ ℤ )
3		dvdsabsb	⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )
4	2 3	sylan	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )
5	1 4	bitrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )