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

Theorem rexr 9063
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
rexr  |-  ( A  e.  RR  ->  A  e.  RR* )

Proof of Theorem rexr
StepHypRef Expression
1 ressxr 9062 . 2  |-  RR  C_  RR*
21sseli 3287 1  |-  ( A  e.  RR  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   RRcr 8922   RR*cxr 9052
This theorem is referenced by:  rexri  9070  lenlt  9087  ltpnf  10653  mnflt  10654  xrltnsym  10662  xrlttr  10665  xrre  10689  xrre3  10691  max1  10705  max2  10707  min1  10708  min2  10709  maxle  10710  lemin  10711  maxlt  10712  ltmin  10713  max0sub  10714  qbtwnxr  10718  xralrple  10723  alrple  10724  xltnegi  10734  rexadd  10750  xaddnemnf  10752  xaddnepnf  10753  xaddcom  10756  xnegdi  10759  xpncan  10762  xnpcan  10763  xleadd1a  10764  xleadd1  10766  xltadd1  10767  xltadd2  10768  xsubge0  10772  rexmul  10782  xadddilem  10805  xadddir  10807  xrsupsslem  10817  xrinfmsslem  10818  xrub  10822  supxrun  10826  supxrunb1  10830  supxrunb2  10831  supxrbnd1  10832  supxrbnd2  10833  xrsup0  10834  supxrbnd  10839  elioo4g  10903  elioc2  10905  elico2  10906  elicc2  10907  iccss  10910  iooshf  10921  iooneg  10949  icoshft  10951  difreicc  10960  hashbnd  11551  elicc4abs  12050  limsupgord  12193  pcadd  13185  ramubcl  13313  lt6abl  15431  xrsmcmn  16647  xrs1mnd  16659  xrs10  16660  xrsdsreval  16666  xmetge0  18283  imasdsf1olem  18311  bl2in  18331  blss  18346  blcld  18425  icopnfcld  18673  iocmnfcld  18674  bl2ioo  18694  blssioo  18697  xrtgioo  18708  xrsblre  18713  iccntr  18723  icccmplem2  18725  icccmp  18727  reconnlem2  18729  xrge0tsms  18736  icoopnst  18835  iocopnst  18836  ovolfioo  19231  ovolicc2lem1  19280  ovolicc2lem5  19284  voliunlem3  19313  icombl1  19324  icombl  19325  iccvolcl  19328  ovolioo  19329  uniiccdif  19337  volsup2  19364  mbfimasn  19393  ismbf3d  19413  mbfsup  19423  itg2seq  19501  itg2monolem1  19509  itg2monolem2  19510  itg2monolem3  19511  itg2mono  19512  itg2i1fseqle  19513  itg2i1fseq3  19516  itg2addlem  19517  itg2gt0  19519  itg2cnlem2  19521  dvlip2  19746  ply1remlem  19952  abelthlem3  20216  abelth  20224  sincosq2sgn  20274  sincosq3sgn  20275  sinq12ge0  20283  sincos6thpi  20290  sineq0  20296  efif1olem1  20311  efif1olem2  20312  efif1o  20315  eff1o  20318  loglesqr  20509  basellem1  20730  pntlemo  21168  nmobndi  22124  nmopub2tALT  23260  nmfnleub2  23277  nmopcoadji  23452  rexdiv  24010  xrge0tsmsd  24052  pnfneige0  24140  lmxrge0  24141  hashf2  24270  sxbrsigalem0  24415  orvcgteel  24504  orvclteel  24509  itg2gt0cn  25960  iblabsnclem  25968  bddiblnc  25975  areacirclem6  25987  areacirc  25988  ivthALT  26029  blbnd  26187  icodiamlt  26574  ioovolcl  27410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-un 3268  df-in 3270  df-ss 3277  df-xr 9057
  Copyright terms: Public domain W3C validator