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

Theorem rexr 9122
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 9121 . 2  |-  RR  C_  RR*
21sseli 3336 1  |-  ( A  e.  RR  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8981   RR*cxr 9111
This theorem is referenced by:  rexri  9129  lenlt  9146  ltpnf  10713  mnflt  10714  xrltnsym  10722  xrlttr  10725  xrre  10749  xrre3  10751  max1  10765  max2  10767  min1  10768  min2  10769  maxle  10770  lemin  10771  maxlt  10772  ltmin  10773  max0sub  10774  qbtwnxr  10778  xralrple  10783  alrple  10784  xltnegi  10794  rexadd  10810  xaddnemnf  10812  xaddnepnf  10813  xaddcom  10816  xnegdi  10819  xpncan  10822  xnpcan  10823  xleadd1a  10824  xleadd1  10826  xltadd1  10827  xltadd2  10828  xsubge0  10832  rexmul  10842  xadddilem  10865  xadddir  10867  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxrun  10886  supxrunb1  10890  supxrunb2  10891  supxrbnd1  10892  supxrbnd2  10893  xrsup0  10894  supxrbnd  10899  elioo4g  10963  elioc2  10965  elico2  10966  elicc2  10967  iccss  10970  iooshf  10981  iooneg  11009  icoshft  11011  difreicc  11020  hashbnd  11616  elicc4abs  12115  limsupgord  12258  pcadd  13250  ramubcl  13378  lt6abl  15496  xrsmcmn  16716  xrs1mnd  16728  xrs10  16729  xrsdsreval  16735  psmetge0  18335  xmetge0  18366  imasdsf1olem  18395  bl2in  18422  blssps  18446  blss  18447  blcld  18527  icopnfcld  18794  iocmnfcld  18795  bl2ioo  18815  blssioo  18818  xrtgioo  18829  xrsblre  18834  iccntr  18844  icccmplem2  18846  icccmp  18848  reconnlem2  18850  xrge0tsms  18857  icoopnst  18956  iocopnst  18957  ovolfioo  19356  ovolicc2lem1  19405  ovolicc2lem5  19409  voliunlem3  19438  icombl1  19449  icombl  19450  iccvolcl  19453  ovolioo  19454  uniiccdif  19462  volsup2  19489  mbfimasn  19518  ismbf3d  19538  mbfsup  19548  itg2seq  19626  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq3  19641  itg2addlem  19642  itg2gt0  19644  itg2cnlem2  19646  dvlip2  19871  ply1remlem  20077  abelthlem3  20341  abelth  20349  sincosq2sgn  20399  sincosq3sgn  20400  sinq12ge0  20408  sincos6thpi  20415  sineq0  20421  efif1olem1  20436  efif1olem2  20437  efif1o  20440  eff1o  20443  loglesqr  20634  basellem1  20855  pntlemo  21293  nmobndi  22268  nmopub2tALT  23404  nmfnleub2  23421  nmopcoadji  23596  rexdiv  24164  xrge0tsmsd  24215  pnfneige0  24328  lmxrge0  24329  hashf2  24466  sxbrsigalem0  24613  orvcgteel  24717  orvclteel  24722  mblfinlem  26234  itg2addnc  26249  itg2gt0cn  26250  iblabsnclem  26258  bddiblnc  26265  ftc1anclem1  26270  ftc1anclem6  26275  ftc1anclem8  26277  areacirclem6  26287  areacirc  26288  ivthALT  26329  blbnd  26487  icodiamlt  26874  ioovolcl  27709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-xr 9116
  Copyright terms: Public domain W3C validator