Metamath Proof Explorer

Theorem rpdivcl

Description: Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007)

Ref Expression
Assertion rpdivcl ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2 rprene0 ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) )
3 redivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
4 3 3expb ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
5 1 2 4 syl2an ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
6 elrp ⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
7 elrp ⊢ ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
8 divgt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 / 𝐵 ) )
9 6 7 8 syl2anb ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → 0 < ( 𝐴 / 𝐵 ) )
10 elrp ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ+ ↔ ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 / 𝐵 ) ) )
11 5 9 10 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ+ )