Theorem 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	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge B\ne 0\right)\to \frac{A}{B}\in ℝ$$

Proof

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