Metamath Proof Explorer


Theorem dvds2sub

Description: If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds2sub KMNKMKNKMN

Proof

Step Hyp Ref Expression
1 3simpa KMNKM
2 3simpb KMNKN
3 zsubcl MNMN
4 3 anim2i KMNKMN
5 4 3impb KMNKMN
6 zsubcl xyxy
7 6 adantl KMNxyxy
8 zcn xx
9 zcn yy
10 zcn KK
11 subdir xyKxyK=xKyK
12 8 9 10 11 syl3an xyKxyK=xKyK
13 12 3comr KxyxyK=xKyK
14 13 3expb KxyxyK=xKyK
15 oveq12 xK=MyK=NxKyK=MN
16 14 15 sylan9eq KxyxK=MyK=NxyK=MN
17 16 ex KxyxK=MyK=NxyK=MN
18 17 3ad2antl1 KMNxyxK=MyK=NxyK=MN
19 1 2 5 7 18 dvds2lem KMNKMKNKMN