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 20312
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 20311 . 2 class fld
2 ccnfld 20106 . . 3 class fld
3 cr 10251 . . 3 class
4 cress 16223 . . 3 class s
52, 3, 4co 6905 . 2 class (ℂflds ℝ)
61, 5wceq 1656 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  20313  remulg  20314  resubdrg  20315  resubgval  20316  replusg  20317  remulr  20318  re0g  20319  re1r  20320  rele2  20321  relt  20322  reds  20323  redvr  20324  retos  20325  refld  20326  refldcj  20327  regsumsupp  20329  rzgrp  20330  tgioo3  22978  recvs  23315  retopn  23547  recms  23548  reust  23549  rrxcph  23560  rrxdsfi  23579  reefgim  24603  amgmlem  25129  nn0omnd  30375  nn0archi  30377  xrge0slmod  30378  rezh  30549  rrhcn  30575  rerrext  30587  cnrrext  30588  qqtopn  30589  amgmwlem  43437
  Copyright terms: Public domain W3C validator