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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ+ )