Description: A cancellation law for division. ( divid analog.) (Contributed by Mario Carneiro, 18-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | unitdvcl.o | |
|
unitdvcl.d | |
||
dvrid.o | |
||
Assertion | dvrid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unitdvcl.o | |
|
2 | unitdvcl.d | |
|
3 | dvrid.o | |
|
4 | eqid | |
|
5 | 4 1 | unitcl | |
6 | 5 | adantl | |
7 | eqid | |
|
8 | eqid | |
|
9 | 4 7 1 8 2 | dvrval | |
10 | 6 9 | sylancom | |
11 | 1 8 7 3 | unitrinv | |
12 | 10 11 | eqtrd | |