Metamath Proof Explorer

Theorem absdvdsb

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

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

Proof

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