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

Theorem rexri 9130
Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
Hypothesis
Ref Expression
rexri.1  |-  A  e.  RR
Assertion
Ref Expression
rexri  |-  A  e. 
RR*

Proof of Theorem rexri
StepHypRef Expression
1 rexri.1 . 2  |-  A  e.  RR
2 rexr 9123 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
31, 2ax-mp 8 1  |-  A  e. 
RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   RRcr 8982   RR*cxr 9112
This theorem is referenced by:  xmulid1  10851  xmulid2  10852  xmulm1  10853  x2times  10871  xov1plusxeqvd  11034  hashge1  11656  hashgt12el  11675  hashgt12el2  11676  tanhbnd  12755  leordtval2  17269  nmoid  18769  metnrmlem1a  18881  metnrmlem1  18882  icopnfcnv  18960  icopnfhmeo  18961  iccpnfcnv  18962  iccpnfhmeo  18963  oprpiece1res1  18969  oprpiece1res2  18970  pcoass  19042  vitalilem4  19496  itg2monolem1  19635  itg2monolem3  19637  abelthlem3  20342  abelth  20350  sincosq1sgn  20399  sincosq4sgn  20402  coseq00topi  20403  coseq0negpitopi  20404  tanabsge  20407  sinq12gt0  20408  cosq14gt0  20411  cosordlem  20426  tanord1  20432  tanord  20433  tanregt0  20434  negpitopissre  20435  ellogrn  20450  logimclad  20463  argregt0  20498  argimgt0  20500  argimlt0  20501  dvloglem  20532  logf1o2  20534  dvlog2lem  20536  efopnlem2  20541  isosctrlem1  20655  asinneg  20719  asinsinlem  20724  acoscos  20726  reasinsin  20729  atanlogsublem  20748  atantan  20756  atanbndlem  20758  atanbnd  20759  atan1  20761  scvxcvx  20817  basellem4  20859  dchrvmasumlem2  21185  dchrvmasumiflem1  21188  pntibndlem1  21276  pntibndlem2  21278  pntibnd  21280  pntlemc  21282  pnt  21301  padicabvf  21318  padicabvcxp  21319  umgrafi  21350  nmopun  23510  nmoptrii  23590  nmopcoi  23591  pjnmopi  23644  xlt2addrd  24117  xdivrec  24166  xrsmulgzz  24193  xrnarchi  24247  unitssxrge0  24291  xrge0iifcnv  24312  xrge0iifiso  24314  xrge0iifhom  24316  hasheuni  24468  prob01  24664  dvreasin  26281  areacirclem2  26283  itgsin0pilem1  27712  vdgfrgragt2  28356  sgn1  28460  isosctrlem1ALT  28984  sineq0ALT  28987
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-un 3318  df-in 3320  df-ss 3327  df-xr 9117
  Copyright terms: Public domain W3C validator