Metamath Proof Explorer


Theorem dvds2ln

Description: If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in ApostolNT p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds2ln IJKMNKMKNK I M+ J N

Proof

Step Hyp Ref Expression
1 simpr1 IJKMNK
2 simpr2 IJKMNM
3 1 2 jca IJKMNKM
4 simpr3 IJKMNN
5 1 4 jca IJKMNKN
6 simpll IJKMNI
7 6 2 zmulcld IJKMN I M
8 simplr IJKMNJ
9 8 4 zmulcld IJKMN J N
10 7 9 zaddcld IJKMN I M+ J N
11 1 10 jca IJKMNK I M+ J N
12 zmulcl xIx I
13 zmulcl yJy J
14 12 13 anim12i xIyJx Iy J
15 14 an4s xyIJx Iy J
16 15 expcom IJxyx Iy J
17 16 adantr IJKMNxyx Iy J
18 17 imp IJKMNxyx Iy J
19 zaddcl x Iy Jx I+y J
20 18 19 syl IJKMNxyx I+y J
21 zcn x Ix I
22 zcn y Jy J
23 21 22 anim12i x Iy Jx Iy J
24 18 23 syl IJKMNxyx Iy J
25 1 zcnd IJKMNK
26 25 adantr IJKMNxyK
27 adddir x Iy JKx I+y JK=x IK+y JK
28 27 3expa x Iy JKx I+y JK=x IK+y JK
29 24 26 28 syl2anc IJKMNxyx I+y JK=x IK+y JK
30 zcn xx
31 30 adantr xyx
32 31 adantl IJKMNxyx
33 zcn II
34 33 ad3antrrr IJKMNxyI
35 32 34 26 mul32d IJKMNxyx IK=xK I
36 zcn yy
37 36 adantl xyy
38 37 adantl IJKMNxyy
39 8 zcnd IJKMNJ
40 39 adantr IJKMNxyJ
41 38 40 26 mul32d IJKMNxyy JK=yK J
42 35 41 oveq12d IJKMNxyx IK+y JK=xK I+yK J
43 32 26 mulcld IJKMNxyxK
44 43 34 mulcomd IJKMNxyxK I=IxK
45 38 26 mulcld IJKMNxyyK
46 45 40 mulcomd IJKMNxyyK J=JyK
47 44 46 oveq12d IJKMNxyxK I+yK J=IxK+JyK
48 29 42 47 3eqtrd IJKMNxyx I+y JK=IxK+JyK
49 oveq2 xK=MIxK= I M
50 oveq2 yK=NJyK= J N
51 49 50 oveqan12d xK=MyK=NIxK+JyK= I M+ J N
52 48 51 sylan9eq IJKMNxyxK=MyK=Nx I+y JK= I M+ J N
53 52 ex IJKMNxyxK=MyK=Nx I+y JK= I M+ J N
54 3 5 11 20 53 dvds2lem IJKMNKMKNK I M+ J N