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	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to A B \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
3		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
4	1 2 3	syl2an	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to A B \in ℝ$
5		elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$
6		elrp	$⊢ B \in ℝ^{+} \leftrightarrow (B \in ℝ \land 0 < B)$
7		mulgt0	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < A B$
8	5 6 7	syl2anb	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to 0 < A B$
9		elrp	$⊢ A B \in ℝ^{+} \leftrightarrow (A B \in ℝ \land 0 < A B)$
10	4 8 9	sylanbrc	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to A B \in ℝ^{+}$

Metamath Proof Explorer