Metamath Proof Explorer


Theorem rpmulcl

Description: Closure law for multiplication of positive reals. Part of Axiom 7 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

Ref Expression
Assertion rpmulcl ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
2 rpre ( 𝐵 ∈ ℝ+𝐵 ∈ ℝ )
3 remulcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
5 elrp ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
6 elrp ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
7 mulgt0 ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 · 𝐵 ) )
8 5 6 7 syl2anb ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → 0 < ( 𝐴 · 𝐵 ) )
9 elrp ( ( 𝐴 · 𝐵 ) ∈ ℝ+ ↔ ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 · 𝐵 ) ) )
10 4 8 9 sylanbrc ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ+ )