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 MNMNMMN

Proof

Step Hyp Ref Expression
1 dvdsnegb MNMNM- N
2 znegcl NN
3 dvdsadd MNM- NMM+- N
4 2 3 sylan2 MNM- NMM+- N
5 zcn MM
6 zcn NN
7 negsub MNM+- N=MN
8 5 6 7 syl2an MNM+- N=MN
9 8 breq2d MNMM+- NMMN
10 1 4 9 3bitrd MNMNMMN