Metamath Proof Explorer


Theorem dvdssub2

Description: If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion dvdssub2 KMNKMNKMKN

Proof

Step Hyp Ref Expression
1 zsubcl MNMN
2 1 3adant1 KMNMN
3 dvds2sub KMMNKMKMNKMMN
4 2 3 syld3an3 KMNKMKMNKMMN
5 4 ancomsd KMNKMNKMKMMN
6 5 imp KMNKMNKMKMMN
7 zcn MM
8 zcn NN
9 nncan MNMMN=N
10 7 8 9 syl2an MNMMN=N
11 10 3adant1 KMNMMN=N
12 11 adantr KMNKMNKMMMN=N
13 6 12 breqtrd KMNKMNKMKN
14 13 expr KMNKMNKMKN
15 dvds2add KMNNKMNKNKM-N+N
16 2 15 syld3an2 KMNKMNKNKM-N+N
17 16 imp KMNKMNKNKM-N+N
18 npcan MNM-N+N=M
19 7 8 18 syl2an MNM-N+N=M
20 19 3adant1 KMNM-N+N=M
21 20 adantr KMNKMNKNM-N+N=M
22 17 21 breqtrd KMNKMNKNKM
23 22 expr KMNKMNKNKM
24 14 23 impbid KMNKMNKMKN