MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-refld Structured version   Visualization version   GIF version

Definition df-refld 21012
Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
Assertion
Ref Expression
df-refld fld = (ℂflds ℝ)

Detailed syntax breakdown of Definition df-refld
StepHypRef Expression
1 crefld 21011 . 2 class fld
2 ccnfld 20799 . . 3 class fld
3 cr 11051 . . 3 class
4 cress 17113 . . 3 class s
52, 3, 4co 7358 . 2 class (ℂflds ℝ)
61, 5wceq 1542 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  21013  remulg  21014  resubdrg  21015  resubgval  21016  replusg  21017  remulr  21018  re0g  21019  re1r  21020  rele2  21021  relt  21022  reds  21023  redvr  21024  retos  21025  refld  21026  refldcj  21027  regsumsupp  21029  rzgrp  21030  tgioo3  24171  recvs  24512  recvsOLD  24513  retopn  24746  recms  24747  reust  24748  rrxcph  24759  rrxdsfi  24778  reefgim  25812  amgmlem  26342  nn0omnd  32140  nn0archi  32142  xrge0slmod  32143  ccfldextrr  32340  ccfldsrarelvec  32358  ccfldextdgrr  32359  rezh  32555  rrhcn  32581  rerrext  32593  cnrrext  32594  qqtopn  32595  bj-rveccmod  35776  amgmwlem  47256
  Copyright terms: Public domain W3C validator