Description: If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dvds2sub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa | |
|
2 | 3simpb | |
|
3 | zsubcl | |
|
4 | 3 | anim2i | |
5 | 4 | 3impb | |
6 | zsubcl | |
|
7 | 6 | adantl | |
8 | zcn | |
|
9 | zcn | |
|
10 | zcn | |
|
11 | subdir | |
|
12 | 8 9 10 11 | syl3an | |
13 | 12 | 3comr | |
14 | 13 | 3expb | |
15 | oveq12 | |
|
16 | 14 15 | sylan9eq | |
17 | 16 | ex | |
18 | 17 | 3ad2antl1 | |
19 | 1 2 5 7 18 | dvds2lem | |