Metamath Proof Explorer


Theorem dvds2add

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

Ref Expression
Assertion dvds2add KMNKMKNKM+N

Proof

Step Hyp Ref Expression
1 3simpa KMNKM
2 3simpb KMNKN
3 zaddcl MNM+N
4 3 anim2i KMNKM+N
5 4 3impb KMNKM+N
6 zaddcl xyx+y
7 6 adantl KMNxyx+y
8 zcn xx
9 zcn yy
10 zcn KK
11 adddir xyKx+yK=xK+yK
12 8 9 10 11 syl3an xyKx+yK=xK+yK
13 12 3comr Kxyx+yK=xK+yK
14 13 3expb Kxyx+yK=xK+yK
15 oveq12 xK=MyK=NxK+yK=M+N
16 14 15 sylan9eq KxyxK=MyK=Nx+yK=M+N
17 16 ex KxyxK=MyK=Nx+yK=M+N
18 17 3ad2antl1 KMNxyxK=MyK=Nx+yK=M+N
19 1 2 5 7 18 dvds2lem KMNKMKNKM+N