Metamath Proof Explorer

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 ↾ 𝑠 ℝ
4 cncrng ⊢ ℂ fld ∈ CRing
5 1 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
6 eqid ⊢ ℂ fld ↾ 𝑠 ℝ = ℂ fld ↾ 𝑠 ℝ
7 6 subrgcrng ⊢ ℂ fld ∈ CRing ∧ ℝ ∈ SubRing ⁡ ℂ fld → ℂ fld ↾ 𝑠 ℝ ∈ CRing
8 4 5 7 mp2an ⊢ ℂ fld ↾ 𝑠 ℝ ∈ CRing
9 3 8 eqeltri ⊢ ℝ fld ∈ CRing
10 isfld ⊢ ℝ fld ∈ Field ↔ ℝ fld ∈ DivRing ∧ ℝ fld ∈ CRing
11 2 9 10 mpbir2an ⊢ ℝ fld ∈ Field