Metamath Proof Explorer

Theorem dvdsadd

Description: An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 13-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∈ ℤ
2 zaddcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + N ∈ ℤ
3 simpr ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ
4 iddvds ⊢ M ∈ ℤ → M ∥ M
5 4 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M
6 zcn ⊢ M ∈ ℤ → M ∈ ℂ
7 zcn ⊢ N ∈ ℤ → N ∈ ℂ
8 pncan ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + N - N = M
9 6 7 8 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + N - N = M
10 5 9 breqtrrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M + N - N
11 dvdssub2 ⊢ M ∈ ℤ ∧ M + N ∈ ℤ ∧ N ∈ ℤ ∧ M ∥ M + N - N → M ∥ M + N ↔ M ∥ N
12 1 2 3 10 11 syl31anc ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M + N ↔ M ∥ N
13 12 bicomd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ M + N