redvr

Description: The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

		Ref	Expression
	Assertion	redvr	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A /_{r} (ℝ_{fld}) B = \frac{A}{B}$

Step	Hyp	Ref	Expression
1		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
2	1	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
3		simp1	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \in ℝ$
4		3simpc	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to (B \in ℝ \land B \neq 0)$
5	1	simpri	$⊢ ℝ_{fld} \in DivRing$
6		rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$
7		eqid	$⊢ Unit (ℝ_{fld}) = Unit (ℝ_{fld})$
8		re0g	$⊢ 0 = 0_{ℝ_{fld}}$
9	6 7 8	drngunit	$⊢ ℝ_{fld} \in DivRing \to (B \in Unit (ℝ_{fld}) \leftrightarrow (B \in ℝ \land B \neq 0))$
10	5 9	ax-mp	$⊢ B \in Unit (ℝ_{fld}) \leftrightarrow (B \in ℝ \land B \neq 0)$
11	4 10	sylibr	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to B \in Unit (ℝ_{fld})$
12		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
13		cnflddiv	$⊢ \div = /_{r} (ℂ_{fld})$
14		eqid	$⊢ /_{r} (ℝ_{fld}) = /_{r} (ℝ_{fld})$
15	12 13 7 14	subrgdv	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land A \in ℝ \land B \in Unit (ℝ_{fld})) \to \frac{A}{B} = A /_{r} (ℝ_{fld}) B$
16	2 3 11 15	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} = A /_{r} (ℝ_{fld}) B$
17	16	eqcomd	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A /_{r} (ℝ_{fld}) B = \frac{A}{B}$

Metamath Proof Explorer