Theorem xdivcld

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

	Ref	Expression
Hypotheses	xdivcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xdivcld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	xdivcld.3	⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion	xdivcld	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		xdivcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xdivcld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		xdivcld.3	⊢ ( 𝜑 → 𝐵 ≠ 0 )
4		xdivval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
6		xreceu	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
7	1 2 3 6	syl3anc	⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
8		riotacl	⊢ ( ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 → ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) ∈ ℝ* )
9	7 8	syl	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) ∈ ℝ* )
10	5 9	eqeltrd	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ* )