Description: Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsmulcr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zmulcl | |
|
2 | 1 | 3adant2 | |
3 | zmulcl | |
|
4 | 3 | 3adant1 | |
5 | 2 4 | jca | |
6 | 5 | 3adant3r | |
7 | 3simpa | |
|
8 | simpr | |
|
9 | zcn | |
|
10 | zcn | |
|
11 | 9 10 | anim12i | |
12 | zcn | |
|
13 | zcn | |
|
14 | 13 | anim1i | |
15 | mulass | |
|
16 | 15 | 3expa | |
17 | 16 | adantrr | |
18 | 17 | 3adant2 | |
19 | 18 | eqeq1d | |
20 | mulcl | |
|
21 | mulcan2 | |
|
22 | 20 21 | syl3an1 | |
23 | 19 22 | bitr3d | |
24 | 11 12 14 23 | syl3an | |
25 | 24 | 3expb | |
26 | 25 | 3impa | |
27 | 26 | 3coml | |
28 | 27 | 3expia | |
29 | 28 | 3impb | |
30 | 29 | imp | |
31 | 30 | biimpd | |
32 | 6 7 8 31 | dvds1lem | |
33 | dvdsmulc | |
|
34 | 33 | 3adant3r | |
35 | 32 34 | impbid | |