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 ℂ|Bx=A\right)$$
2		receu	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \exists !x\in ℂBx=A$$
3		riotacl	$$⊢\exists !x\in ℂBx=A\to \left(\iota x\in ℂ|Bx=A\right)\in ℂ$$
4	2 3	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\iota x\in ℂ|Bx=A\right)\in ℂ$$
5	1 4	eqeltrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}\in ℂ$$