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 MNMNMM+N

Proof

Step Hyp Ref Expression
1 simpl MNM
2 zaddcl MNM+N
3 simpr MNN
4 iddvds MMM
5 4 adantr MNMM
6 zcn MM
7 zcn NN
8 pncan MNM+N-N=M
9 6 7 8 syl2an MNM+N-N=M
10 5 9 breqtrrd MNMM+N-N
11 dvdssub2 MM+NNMM+N-NMM+NMN
12 1 2 3 10 11 syl31anc MNMM+NMN
13 12 bicomd MNMNMM+N