refld

Description: The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017)

		Ref	Expression
	Assertion	refld	$⊢ ℝ_{fld} \in Field$

Step	Hyp	Ref	Expression
1		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
2	1	simpri	$⊢ ℝ_{fld} \in DivRing$
3		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
4		cncrng	$⊢ ℂ_{fld} \in CRing$
5	1	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
6		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℝ = ℂ_{fld} ↾_{𝑠} ℝ$
7	6	subrgcrng	$⊢ (ℂ_{fld} \in CRing \land ℝ \in SubRing (ℂ_{fld})) \to ℂ_{fld} ↾_{𝑠} ℝ \in CRing$
8	4 5 7	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} ℝ \in CRing$
9	3 8	eqeltri	$⊢ ℝ_{fld} \in CRing$
10		isfld	$⊢ ℝ_{fld} \in Field \leftrightarrow (ℝ_{fld} \in DivRing \land ℝ_{fld} \in CRing)$
11	2 9 10	mpbir2an	$⊢ ℝ_{fld} \in Field$

Metamath Proof Explorer