Theorem rpxdivcld

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

	Ref	Expression
Hypotheses	rpxdivcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	rpxdivcld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
Assertion	rpxdivcld	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		rpxdivcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		rpxdivcld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3	1	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4	2	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5	2	rpne0d	⊢ ( 𝜑 → 𝐵 ≠ 0 )
6		rexdiv	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( 𝐴 / 𝐵 ) )
7	3 4 5 6	syl3anc	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) = ( 𝐴 / 𝐵 ) )
8	1 2	rpdivcld	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) ∈ ℝ+ )
9	7 8	eqeltrd	⊢ ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ )