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 21623
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 21622 . 2 class fld
2 ccnfld 21364 . . 3 class fld
3 cr 11154 . . 3 class
4 cress 17274 . . 3 class s
52, 3, 4co 7431 . 2 class (ℂflds ℝ)
61, 5wceq 1540 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  21624  remulg  21625  resubdrg  21626  resubgval  21627  replusg  21628  remulr  21629  re0g  21630  re1r  21631  rele2  21632  relt  21633  reds  21634  redvr  21635  retos  21636  refld  21637  refldcj  21638  regsumsupp  21640  rzgrp  21641  tgioo3  24827  recvs  25179  recvsOLD  25180  retopn  25413  recms  25414  reust  25415  rrxcph  25426  rrxdsfi  25445  reefgim  26494  amgmlem  27033  nn0omnd  33373  nn0archi  33375  xrge0slmod  33376  ccfldextrr  33699  ccfldsrarelvec  33721  ccfldextdgrr  33722  rezh  33970  rrhcn  33998  rerrext  34010  cnrrext  34011  qqtopn  34012  bj-rveccmod  37303  amgmwlem  49321
  Copyright terms: Public domain W3C validator