rpdivcl

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

		Ref	Expression
	Assertion	rpdivcl	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ^{+}$

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

Metamath Proof Explorer