Metamath Proof Explorer

Theorem dvdssub

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

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

Proof

Step Hyp Ref Expression
1 dvdsnegb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ -N
2 znegcl ⊢ N ∈ ℤ → − N ∈ ℤ
3 dvdsadd ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M ∥ -N ↔ M ∥ M + -N
4 2 3 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ -N ↔ M ∥ M + -N
5 zcn ⊢ M ∈ ℤ → M ∈ ℂ
6 zcn ⊢ N ∈ ℤ → N ∈ ℂ
7 negsub ⊢ 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 1 4 9 3bitrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ M − N