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 K M N K M K N K M + N

Proof

Step Hyp Ref Expression
1 3simpa K M N K M
2 3simpb K M N K N
3 zaddcl M N M + N
4 3 anim2i K M N K M + N
5 4 3impb K M N K M + N
6 zaddcl x y x + y
7 6 adantl K M N x y x + y
8 zcn x x
9 zcn y y
10 zcn K K
11 adddir x y K x + y K = x K + y K
12 8 9 10 11 syl3an x y K x + y K = x K + y K
13 12 3comr K x y x + y K = x K + y K
14 13 3expb K x y x + y K = x K + y K
15 oveq12 x K = M y K = N x K + y K = M + N
16 14 15 sylan9eq K x y x K = M y K = N x + y K = M + N
17 16 ex K x y x K = M y K = N x + y K = M + N
18 17 3ad2antl1 K M N x y x K = M y K = N x + y K = M + N
19 1 2 5 7 18 dvds2lem K M N K M K N K M + N