Metamath Proof Explorer

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 ℝ$