Description: Cancellation law for the divides relation. Theorem 1.1(e) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdscmulr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zmulcl | |
|
2 | 1 | 3adant3 | |
3 | zmulcl | |
|
4 | 3 | 3adant2 | |
5 | 2 4 | jca | |
6 | 5 | 3coml | |
7 | 6 | 3adant3r | |
8 | 3simpa | |
|
9 | simpr | |
|
10 | zcn | |
|
11 | zcn | |
|
12 | 10 11 | anim12i | |
13 | zcn | |
|
14 | zcn | |
|
15 | 14 | anim1i | |
16 | mul12 | |
|
17 | 16 | 3adant1r | |
18 | 17 | 3expb | |
19 | 18 | ancoms | |
20 | 19 | 3adant2 | |
21 | 20 | eqeq1d | |
22 | mulcl | |
|
23 | mulcan | |
|
24 | 22 23 | syl3an1 | |
25 | 21 24 | bitr3d | |
26 | 12 13 15 25 | syl3an | |
27 | 26 | 3expb | |
28 | 27 | 3impa | |
29 | 28 | 3coml | |
30 | 29 | 3expia | |
31 | 30 | 3impb | |
32 | 31 | imp | |
33 | 32 | biimpd | |
34 | 7 8 9 33 | dvds1lem | |
35 | dvdscmul | |
|
36 | 35 | 3adant3r | |
37 | 34 36 | impbid | |