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