Metamath Proof Explorer

Theorem resubdrg

Description: The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014) (Revised by Thierry Arnoux, 30-Jun-2019)

		Ref	Expression
	Assertion	resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ x \in ℝ \to x \in ℂ$
2		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
3		renegcl	$⊢ x \in ℝ \to - x \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
6		rereccl	$⊢ (x \in ℝ \land x \neq 0) \to \frac{1}{x} \in ℝ$
7	1 2 3 4 5 6	cnsubdrglem	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℝ \in DivRing)$
8		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
9	8	eleq1i	$⊢ ℝ_{fld} \in DivRing \leftrightarrow ℂ_{fld} ↾_{𝑠} ℝ \in DivRing$
10	9	anbi2i	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing) \leftrightarrow (ℝ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℝ \in DivRing)$
11	7 10	mpbir	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$