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↔NmodM=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↔NmodM=0
5 3 4 sylan ⊢M∈ℤ∧M≠0∧N∈ℤ→M∥N↔NmodM=0
6 2 5 bitrd ⊢M∈ℤ∧M≠0∧N∈ℤ→M∥N↔NmodM=0
7 6 an32s ⊢M∈ℤ∧N∈ℤ∧M≠0→M∥N↔NmodM=0
8 7 3impa ⊢M∈ℤ∧N∈ℤ∧M≠0→M∥N↔NmodM=0