Metamath Proof Explorer

Theorem dvdsaddr

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

Ref Expression
Assertion dvdsaddr ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N + M

Proof

Step Hyp Ref Expression
1 dvdsadd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ M + N
2 zcn ⊢ M ∈ ℤ → M ∈ ℂ
3 zcn ⊢ N ∈ ℤ → N ∈ ℂ
4 addcom ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + N = N + M
5 2 3 4 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + N = N + M
6 5 breq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M + N ↔ M ∥ N + M
7 1 6 bitrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N + M