This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rerpdivcl

Description: Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008)

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

Step	Hyp	Ref	Expression
1		rprene0	$⊢ B \in ℝ^{+} \to (B \in ℝ \land B \neq 0)$
2		redivcl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} \in ℝ$
3	2	3expb	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0)) \to \frac{A}{B} \in ℝ$
4	1 3	sylan2	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$