# Metamath Proof Explorer

## Theorem divcl

Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion divcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}\in ℂ$

### Proof

Step Hyp Ref Expression
1 divval ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}=\left(\iota {x}\in ℂ|{B}{x}={A}\right)$
2 receu ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}{B}{x}={A}$
3 riotacl ${⊢}\exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}{B}{x}={A}\to \left(\iota {x}\in ℂ|{B}{x}={A}\right)\in ℂ$
4 2 3 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(\iota {x}\in ℂ|{B}{x}={A}\right)\in ℂ$
5 1 4 eqeltrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}\in ℂ$
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 6, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}