Theorem xdivcld

Description: Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017)

	Ref	Expression
Hypotheses	xdivcld.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xdivcld.2	$$⊢\phi \to B\in ℝ$$
	xdivcld.3	$$⊢\phi \to B\ne 0$$
Assertion	xdivcld	$$⊢\phi \to A{÷}_{𝑒}B\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		xdivcld.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xdivcld.2	$$⊢\phi \to B\in ℝ$$
3		xdivcld.3	$$⊢\phi \to B\ne 0$$
4		xdivval	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\wedge B\ne 0\right)\to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$
5	1 2 3 4	syl3anc	$$⊢\phi \to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$
6		xreceu	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\wedge B\ne 0\right)\to \exists !x\in {ℝ}^{*}B{\cdot }_{𝑒}x=A$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \exists !x\in {ℝ}^{*}B{\cdot }_{𝑒}x=A$$
8		riotacl	$$⊢\exists !x\in {ℝ}^{*}B{\cdot }_{𝑒}x=A\to \left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)\in {ℝ}^{*}$$
9	7 8	syl	$$⊢\phi \to \left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)\in {ℝ}^{*}$$
10	5 9	eqeltrd	$$⊢\phi \to A{÷}_{𝑒}B\in {ℝ}^{*}$$