Metamath Proof Explorer


Theorem dvdssubr

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

Ref Expression
Assertion dvdssubr MNMNMNM

Proof

Step Hyp Ref Expression
1 zsubcl NMNM
2 1 ancoms MNNM
3 dvdsadd MNMMNMMM+N-M
4 2 3 syldan MNMNMMM+N-M
5 zcn MM
6 zcn NN
7 pncan3 MNM+N-M=N
8 5 6 7 syl2an MNM+N-M=N
9 8 breq2d MNMM+N-MMN
10 4 9 bitr2d MNMNMNM