Metamath Proof Explorer

Theorem rerrext

Description: The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018)

Ref Expression
Assertion rerrext ⊢ ℝ fld ∈ ℝExt

Proof

Step Hyp Ref Expression
1 cnnrg ⊢ ℂ fld ∈ NrmRing
2 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
3 2 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
4 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
5 4 subrgnrg ⊢ ℂ fld ∈ NrmRing ∧ ℝ ∈ SubRing ⁡ ℂ fld → ℝ fld ∈ NrmRing
6 1 3 5 mp2an ⊢ ℝ fld ∈ NrmRing
7 2 simpri ⊢ ℝ fld ∈ DivRing
8 6 7 pm3.2i ⊢ ℝ fld ∈ NrmRing ∧ ℝ fld ∈ DivRing
9 rezh ⊢ ℤMod ⁡ ℝ fld ∈ NrmMod
10 reofld ⊢ ℝ fld ∈ oField
11 ofldchr ⊢ ℝ fld ∈ oField → chr ⁡ ℝ fld = 0
12 10 11 ax-mp ⊢ chr ⁡ ℝ fld = 0
13 9 12 pm3.2i ⊢ ℤMod ⁡ ℝ fld ∈ NrmMod ∧ chr ⁡ ℝ fld = 0
14 recusp ⊢ ℝ fld ∈ CUnifSp
15 reust ⊢ UnifSt ⁡ ℝ fld = metUnif ⁡ dist ⁡ ℝ fld ↾ ℝ 2
16 14 15 pm3.2i ⊢ ℝ fld ∈ CUnifSp ∧ UnifSt ⁡ ℝ fld = metUnif ⁡ dist ⁡ ℝ fld ↾ ℝ 2
17 rebase ⊢ ℝ = Base ℝ fld
18 eqid ⊢ dist ⁡ ℝ fld ↾ ℝ 2 = dist ⁡ ℝ fld ↾ ℝ 2
19 eqid ⊢ ℤMod ⁡ ℝ fld = ℤMod ⁡ ℝ fld
20 17 18 19 isrrext ⊢ ℝ fld ∈ ℝExt ↔ ℝ fld ∈ NrmRing ∧ ℝ fld ∈ DivRing ∧ ℤMod ⁡ ℝ fld ∈ NrmMod ∧ chr ⁡ ℝ fld = 0 ∧ ℝ fld ∈ CUnifSp ∧ UnifSt ⁡ ℝ fld = metUnif ⁡ dist ⁡ ℝ fld ↾ ℝ 2
21 8 13 16 20 mpbir3an ⊢ ℝ fld ∈ ℝExt