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 MNMNMN+M

Proof

Step Hyp Ref Expression
1 dvdsadd MNMNMM+N
2 zcn MM
3 zcn NN
4 addcom MNM+N=N+M
5 2 3 4 syl2an MNM+N=N+M
6 5 breq2d MNMM+NMN+M
7 1 6 bitrd MNMNMN+M