Metamath Proof Explorer

Theorem dvdsabsb

Description: An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdsabsb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N

Proof

Step Hyp Ref Expression
1 breq2 ⊢ N = N → M ∥ N ↔ M ∥ N
2 1 bicomd ⊢ N = N → M ∥ N ↔ M ∥ N
3 2 a1i ⊢ M ∈ ℤ ∧ N ∈ ℤ → N = N → M ∥ N ↔ M ∥ N
4 dvdsnegb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ -N
5 breq2 ⊢ N = − N → M ∥ N ↔ M ∥ -N
6 5 bicomd ⊢ N = − N → M ∥ -N ↔ M ∥ N
7 4 6 sylan9bb ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N = − N → M ∥ N ↔ M ∥ N
8 7 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → N = − N → M ∥ N ↔ M ∥ N
9 zre ⊢ N ∈ ℤ → N ∈ ℝ
10 9 absord ⊢ N ∈ ℤ → N = N ∨ N = − N
11 10 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ → N = N ∨ N = − N
12 3 8 11 mpjaod ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N