Theorem refld

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

	Ref	Expression
Assertion	refld	⊢ ℝfld ∈ Field

Proof

Step	Hyp	Ref	Expression
1		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
2	1	simpri	⊢ ℝfld ∈ DivRing
3		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
4		cncrng	⊢ ℂfld ∈ CRing
5	1	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
6		eqid	⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ )
7	6	subrgcrng	⊢ ( ( ℂfld ∈ CRing ∧ ℝ ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s ℝ ) ∈ CRing )
8	4 5 7	mp2an	⊢ ( ℂfld ↾s ℝ ) ∈ CRing
9	3 8	eqeltri	⊢ ℝfld ∈ CRing
10		isfld	⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
11	2 9 10	mpbir2an	⊢ ℝfld ∈ Field