Metamath Proof Explorer


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 ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ )