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

Theorem rexri 9063
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 9056 . 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 1717   RRcr 8915   RR*cxr 9045
This theorem is referenced by:  xmulid1  10783  xmulid2  10784  xmulm1  10785  x2times  10803  xov1plusxeqvd  10966  hashge1  11583  hashgt12el  11602  hashgt12el2  11603  tanhbnd  12682  leordtval2  17191  nmoid  18640  metnrmlem1a  18752  metnrmlem1  18753  icopnfcnv  18831  icopnfhmeo  18832  iccpnfcnv  18833  iccpnfhmeo  18834  oprpiece1res1  18840  oprpiece1res2  18841  pcoass  18913  vitalilem4  19363  itg2monolem1  19502  itg2monolem3  19504  abelthlem3  20209  abelth  20217  sincosq1sgn  20266  sincosq4sgn  20269  coseq00topi  20270  coseq0negpitopi  20271  tanabsge  20274  sinq12gt0  20275  cosq14gt0  20278  cosordlem  20293  tanord1  20299  tanord  20300  tanregt0  20301  negpitopissre  20302  ellogrn  20317  logimclad  20330  argregt0  20365  argimgt0  20367  argimlt0  20368  dvloglem  20399  logf1o2  20401  dvlog2lem  20403  efopnlem2  20408  isosctrlem1  20522  asinneg  20586  asinsinlem  20591  acoscos  20593  reasinsin  20596  atanlogsublem  20615  atantan  20623  atanbndlem  20625  atanbnd  20626  atan1  20628  scvxcvx  20684  basellem4  20726  dchrvmasumlem2  21052  dchrvmasumiflem1  21055  pntibndlem1  21143  pntibndlem2  21145  pntibnd  21147  pntlemc  21149  pnt  21168  padicabvf  21185  padicabvcxp  21186  umgrafi  21217  nmopun  23358  nmoptrii  23438  nmopcoi  23439  pjnmopi  23492  xlt2addrd  23953  xdivrec  24004  xrsmulgzz  24026  unitssxrge0  24095  xrge0iifcnv  24116  xrge0iifiso  24118  xrge0iifhom  24120  hasheuni  24264  prob01  24443  dvreasin  25973  areacirclem2  25975  itgsin0pilem1  27405  vdgfrgragt2  27774  sgn1  27861
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 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-in 3263  df-ss 3270  df-xr 9050
  Copyright terms: Public domain W3C validator