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 19711
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 19710 . 2 class fld
2 ccnfld 19509 . . 3 class fld
3 cr 9787 . . 3 class
4 cress 15638 . . 3 class s
52, 3, 4co 6523 . 2 class (ℂflds ℝ)
61, 5wceq 1474 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  19712  remulg  19713  resubdrg  19714  resubgval  19715  replusg  19716  remulr  19717  re0g  19718  re1r  19719  rele2  19720  relt  19721  reds  19722  redvr  19723  retos  19724  refld  19725  refldcj  19726  regsumsupp  19728  tgioo3  22344  retopn  22888  recms  22889  reust  22890  rrxcph  22901  reefgim  23921  rzgrp  24017  amgmlem  24429  nn0omnd  28974  nn0archi  28976  xrge0slmod  28977  rezh  29145  rrhcn  29171  rerrext  29183  cnrrext  29184  qqtopn  29185  rrxdsfi  38981  amgmwlem  42316
  Copyright terms: Public domain W3C validator