Theorem rexri 9646

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

Step	Hyp	Ref	Expression
1		rexri.1	. 2 |- A e. RR
2		rexr 9639	. 2 |- ( A e. RR -> A e. RR* )
3	1, 2	ax-mp 5	1 |- A e. RR*

Syntax hints:   e. wcel 1767   RRcr 9491   RR*cxr 9627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-xr 9632

This theorem is referenced by:  xmulid1  11471  xmulid2  11472  xmulm1  11473  x2times  11491  xov1plusxeqvd  11666  hashge1  12425  hashgt12el  12446  hashgt12el2  12447  tanhbnd  13757  isnzr2hash  17711  0rngnnzr  17716  leordtval2  19507  nmoid  21012  metnrmlem1a  21125  metnrmlem1  21126  icopnfcnv  21205  icopnfhmeo  21206  iccpnfcnv  21207  iccpnfhmeo  21208  oprpiece1res1  21214  oprpiece1res2  21215  pcoass  21287  vitalilem4  21783  itg2monolem1  21920  itg2monolem3  21922  abelthlem3  22590  abelth  22598  neghalfpirx  22620  sincosq1sgn  22652  sincosq4sgn  22655  coseq00topi  22656  coseq0negpitopi  22657  tanabsge  22660  sinq12gt0  22661  cosq14gt0  22664  cosordlem  22679  tanord1  22685  tanord  22686  tanregt0  22687  negpitopissre  22688  ellogrn  22703  logimclad  22716  argregt0  22751  argimgt0  22753  argimlt0  22754  dvloglem  22785  logf1o2  22787  dvlog2lem  22789  efopnlem2  22794  isosctrlem1  22908  asinneg  22973  asinsinlem  22978  acoscos  22980  reasinsin  22983  atanlogsublem  23002  atantan  23010  atanbndlem  23012  atanbnd  23013  atan1  23015  scvxcvx  23071  dchrvmasumlem2  23439  dchrvmasumiflem1  23442  pntibndlem1  23530  pntibndlem2  23532  pntibnd  23534  pntlemc  23536  pnt  23555  padicabvf  23572  padicabvcxp  23573  tgldimor  23649  umgrafi  24026  vdgfrgragt2  24732  nmopun  26637  nmoptrii  26717  nmopcoi  26718  pjnmopi  26771  xlt2addrd  27274  xdivrec  27319  xrsmulgzz  27356  xrnarchi  27418  unitssxrge0  27546  xrge0iifcnv  27579  xrge0iifiso  27581  xrge0iifhom  27583  hasheuni  27759  ddemeas  27876  prob01  28020  sgnsgn  28155  sin2h  29650  cos2h  29651  tan2h  29652  asindmre  29707  dvasin  29708  dvacos  29709  areacirclem1  29712  areaquad  30817  itgsin0pilem1  31295  fourierdlem24  31459  fourierdlem38  31473  fourierdlem43  31478  fourierdlem44  31479  fourierdlem46  31481  fourierdlem62  31497  fourierdlem74  31509  fourierdlem75  31510  fourierdlem85  31520  fourierdlem88  31523  fourierdlem93  31528  fourierdlem102  31537  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fourierdlem112  31547  fourierdlem114  31549  sqwvfoura  31557  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560  fouriercn  31561  pgrpgt2nabl  32056  isosctrlem1ALT  32832  sineq0ALT  32835  bj-flbi3  33697  bj-pinftyccb  33714  bj-minftyccb  33718  bj-pinftynminfty  33720