This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem re1r

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

Ref Expression
Assertion re1r ⊢ 1 = 1 ℝ fld

Proof

Step Hyp Ref Expression
1 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
2 1 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
3 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
4 cnfld1 ⊢ 1 = 1 ℂ fld
5 3 4 subrg1 ⊢ ℝ ∈ SubRing ⁡ ℂ fld → 1 = 1 ℝ fld
6 2 5 ax-mp ⊢ 1 = 1 ℝ fld