redivcl

Description: Closure law for division of reals. (Contributed by NM, 27-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	redivcl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} \in ℝ$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \in ℝ$
2	1	recnd	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \in ℂ$
3		simp2	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to B \in ℝ$
4	3	recnd	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to B \in ℂ$
5		simp3	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to B \neq 0$
6		divrec	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
7	2 4 5 6	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
8		rereccl	$⊢ (B \in ℝ \land B \neq 0) \to \frac{1}{B} \in ℝ$
9	8	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{1}{B} \in ℝ$
10	1 9	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A (\frac{1}{B}) \in ℝ$
11	7 10	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} \in ℝ$

Metamath Proof Explorer