Metamath Proof Explorer

Theorem dvdssubr

Description: An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 zsubcl ⊢ N ∈ ℤ ∧ M ∈ ℤ → N − M ∈ ℤ
2 1 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → N − M ∈ ℤ
3 dvdsadd ⊢ M ∈ ℤ ∧ N − M ∈ ℤ → M ∥ N − M ↔ M ∥ M + N - M
4 2 3 syldan ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N − M ↔ M ∥ M + N - M
5 zcn ⊢ M ∈ ℤ → M ∈ ℂ
6 zcn ⊢ N ∈ ℤ → N ∈ ℂ
7 pncan3 ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + N - M = N
8 5 6 7 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + N - M = N
9 8 breq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M + N - M ↔ M ∥ N
10 4 9 bitr2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N − M