Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | divcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divval | |
|
2 | receu | |
|
3 | riotacl | |
|
4 | 2 3 | syl | |
5 | 1 4 | eqeltrd | |