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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 | |
|
2 | simpr2 | |
|
3 | 1 2 | jca | |
4 | simpr3 | |
|
5 | 1 4 | jca | |
6 | simpll | |
|
7 | 6 2 | zmulcld | |
8 | simplr | |
|
9 | 8 4 | zmulcld | |
10 | 7 9 | zaddcld | |
11 | 1 10 | jca | |
12 | zmulcl | |
|
13 | zmulcl | |
|
14 | 12 13 | anim12i | |
15 | 14 | an4s | |
16 | 15 | expcom | |
17 | 16 | adantr | |
18 | 17 | imp | |
19 | zaddcl | |
|
20 | 18 19 | syl | |
21 | zcn | |
|
22 | zcn | |
|
23 | 21 22 | anim12i | |
24 | 18 23 | syl | |
25 | 1 | zcnd | |
26 | 25 | adantr | |
27 | adddir | |
|
28 | 27 | 3expa | |
29 | 24 26 28 | syl2anc | |
30 | zcn | |
|
31 | 30 | adantr | |
32 | 31 | adantl | |
33 | zcn | |
|
34 | 33 | ad3antrrr | |
35 | 32 34 26 | mul32d | |
36 | zcn | |
|
37 | 36 | adantl | |
38 | 37 | adantl | |
39 | 8 | zcnd | |
40 | 39 | adantr | |
41 | 38 40 26 | mul32d | |
42 | 35 41 | oveq12d | |
43 | 32 26 | mulcld | |
44 | 43 34 | mulcomd | |
45 | 38 26 | mulcld | |
46 | 45 40 | mulcomd | |
47 | 44 46 | oveq12d | |
48 | 29 42 47 | 3eqtrd | |
49 | oveq2 | |
|
50 | oveq2 | |
|
51 | 49 50 | oveqan12d | |
52 | 48 51 | sylan9eq | |
53 | 52 | ex | |
54 | 3 5 11 20 53 | dvds2lem | |