MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexr Unicode version

Theorem rexr 9660
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
rexr

Proof of Theorem rexr
StepHypRef Expression
1 ressxr 9658 . 2
21sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cr 9512   cxr 9648
This theorem is referenced by:  rexri  9667  lenlt  9684  ltpnf  11360  mnflt  11362  xrltnsym  11372  xrlttr  11375  xrre  11399  xrre3  11401  max1  11415  max2  11417  min1  11418  min2  11419  maxle  11420  lemin  11421  maxlt  11422  ltmin  11423  max0sub  11424  qbtwnxr  11428  xralrple  11433  alrple  11434  xltnegi  11444  rexadd  11460  xaddnemnf  11462  xaddnepnf  11463  xaddcom  11466  xnegdi  11469  xpncan  11472  xnpcan  11473  xleadd1a  11474  xleadd1  11476  xltadd1  11477  xltadd2  11478  xsubge0  11482  rexmul  11492  xadddilem  11515  xadddir  11517  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrun  11536  supxrunb1  11540  supxrunb2  11541  supxrbnd1  11542  supxrbnd2  11543  xrsup0  11544  supxrbnd  11549  elioo4g  11614  elioc2  11616  elico2  11617  elicc2  11618  iccss  11621  iooshf  11632  iooneg  11669  icoshft  11671  difreicc  11681  hashbnd  12411  elicc4abs  13152  limsupgord  13295  pcadd  14408  ramubcl  14536  lt6abl  16897  xrsmcmn  18441  xrs1mnd  18456  xrs10  18457  xrsdsreval  18463  psmetge0  20816  xmetge0  20847  imasdsf1olem  20876  bl2in  20903  blssps  20927  blss  20928  blcld  21008  icopnfcld  21275  iocmnfcld  21276  bl2ioo  21297  blssioo  21300  xrtgioo  21311  xrsblre  21316  iccntr  21326  icccmplem2  21328  icccmp  21330  reconnlem2  21332  xrge0tsms  21339  icoopnst  21439  iocopnst  21440  ovolfioo  21879  ovolicc2lem1  21928  ovolicc2lem5  21932  voliunlem3  21962  icombl1  21973  icombl  21974  iccvolcl  21977  ovolioo  21978  ioovolcl  21979  uniiccdif  21987  volsup2  22014  mbfimasn  22041  ismbf3d  22061  mbfsup  22071  itg2seq  22149  dvlip2  22396  ply1remlem  22563  abelthlem3  22828  abelth  22836  sincosq2sgn  22892  sincosq3sgn  22893  sinq12ge0  22901  sincos6thpi  22908  sineq0  22914  efif1olem1  22929  efif1olem2  22930  efif1o  22933  eff1o  22936  loglesqrt  23132  basellem1  23354  pntlemo  23792  nmobndi  25690  nmopub2tALT  26828  nmfnleub2  26845  nmopcoadji  27020  rexdiv  27622  xrge0tsmsd  27775  pnfneige0  27933  lmxrge0  27934  hashf2  28090  sxbrsigalem0  28242  orvcgteel  28406  orvclteel  28411  sgnclre  28478  sgnneg  28479  signstfvneq0  28529  mblfinlem2  30052  iblabsnclem  30078  bddiblnc  30085  ftc1anclem1  30090  ftc1anclem6  30095  areacirclem5  30111  areacirc  30112  ivthALT  30153  blbnd  30283  icodiamlt  30756  iocmbl  31180  ioomidp  31554  limsupre  31647  icccncfext  31690  volioc  31771  fourierdlem113  32002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-xr 9653
  Copyright terms: Public domain W3C validator