Theorem rpxdivcld

Description: Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Hypotheses	rpxdivcld.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	rpxdivcld.2	$$⊢\phi \to B\in {ℝ}^{+}$$
Assertion	rpxdivcld	$$⊢\phi \to A{÷}_{𝑒}B\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rpxdivcld.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rpxdivcld.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3	1	rpred	$$⊢\phi \to A\in ℝ$$
4	2	rpred	$$⊢\phi \to B\in ℝ$$
5	2	rpne0d	$$⊢\phi \to B\ne 0$$
6		rexdiv	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge B\ne 0\right)\to A{÷}_{𝑒}B=\frac{A}{B}$$
7	3 4 5 6	syl3anc	$$⊢\phi \to A{÷}_{𝑒}B=\frac{A}{B}$$
8	1 2	rpdivcld	$$⊢\phi \to \frac{A}{B}\in {ℝ}^{+}$$
9	7 8	eqeltrd	$$⊢\phi \to A{÷}_{𝑒}B\in {ℝ}^{+}$$