Metamath Proof Explorer

Theorem dvdsabsmod0

Description: Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014) (Proof shortened by OpenAI, 3-Jul-2020)

Ref Expression
Assertion dvdsabsmod0 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≠ 0 → M ∥ N ↔ N mod M = 0

Proof

Step Hyp Ref Expression
1 absdvdsb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N
2 1 adantlr ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N
3 nnabscl ⊢ M ∈ ℤ ∧ M ≠ 0 → M ∈ ℕ
4 dvdsval3 ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∥ N ↔ N mod M = 0
5 3 4 sylan ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ → M ∥ N ↔ N mod M = 0
6 2 5 bitrd ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ → M ∥ N ↔ N mod M = 0
7 6 an32s ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≠ 0 → M ∥ N ↔ N mod M = 0
8 7 3impa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≠ 0 → M ∥ N ↔ N mod M = 0