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