Theorem rexr 10248

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 10246	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3728	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2127  ℝcr 10098  ℝ^*cxr 10236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708  df-in 3710  df-ss 3717  df-xr 10241

This theorem is referenced by:  rexri  10260  lenlt  10279  ltpnf  12118  mnflt  12121  xrltnsym  12134  xrlttr  12137  xrre  12164  xrre3  12166  max1  12180  max2  12182  min1  12184  min2  12185  maxle  12186  lemin  12187  maxlt  12188  ltmin  12189  max0sub  12191  qbtwnxr  12195  xralrple  12200  alrple  12201  xltnegi  12211  rexadd  12227  xaddnemnf  12231  xaddnepnf  12232  xaddcom  12235  xnegdi  12242  xpncan  12245  xnpcan  12246  xleadd1a  12247  xleadd1  12249  xltadd1  12250  xltadd2  12251  xsubge0  12255  rexmul  12265  xadddilem  12288  xadddir  12290  xrsupsslem  12301  xrinfmsslem  12302  xrub  12306  supxrun  12310  supxrunb1  12313  supxrunb2  12314  supxrbnd1  12315  supxrbnd2  12316  xrsup0  12317  supxrbnd  12322  infmremnf  12337  elioo4g  12398  elioc2  12400  elico2  12401  elicc2  12402  iccss  12405  iooshf  12416  iooneg  12456  icoshft  12458  difreicc  12468  hashbnd  13288  elicc4abs  14229  icodiamlt  14344  limsupgord  14373  pcadd  15766  ramubcl  15895  lt6abl  18467  xrsmcmn  19942  xrs1mnd  19957  xrs10  19958  xrsdsreval  19964  psmetge0  22289  xmetge0  22321  imasdsf1olem  22350  bl2in  22377  blssps  22401  blss  22402  blcld  22482  icopnfcld  22743  iocmnfcld  22744  bl2ioo  22767  blssioo  22770  xrtgioo  22781  xrsblre  22786  iccntr  22796  icccmplem2  22798  icccmp  22800  reconnlem2  22802  xrge0tsms  22809  icoopnst  22910  iocopnst  22911  ovolfioo  23407  ovolicc2lem1  23456  ovolicc2lem5  23460  voliunlem3  23491  icombl1  23502  icombl  23503  iccvolcl  23506  ovolioo  23507  ioovolcl  23509  uniiccdif  23517  volsup2  23544  mbfimasn  23571  ismbf3d  23591  mbfsup  23601  itg2seq  23679  dvlip2  23928  ply1remlem  24092  abelthlem3  24357  abelth  24365  sincosq2sgn  24421  sincosq3sgn  24422  sinq12ge0  24430  sincos6thpi  24437  sineq0  24443  efif1olem1  24458  efif1olem2  24459  efif1o  24462  eff1o  24465  loglesqrt  24669  basellem1  24977  pntlemo  25466  nmobndi  27910  nmopub2tALT  29048  nmfnleub2  29065  nmopcoadji  29240  rexdiv  29914  xrge0tsmsd  30065  pnfneige0  30277  lmxrge0  30278  hashf2  30426  sxbrsigalem0  30613  omssubadd  30642  orvcgteel  30809  orvclteel  30814  sgnclre  30881  sgnneg  30882  signstfvneq0  30929  ivthALT  32607  icorempt2  33481  icoreunrn  33489  iooelexlt  33492  relowlssretop  33493  relowlpssretop  33494  poimir  33724  mblfinlem2  33729  iblabsnclem  33755  bddiblnc  33762  ftc1anclem1  33767  ftc1anclem6  33772  areacirclem5  33786  areacirc  33787  blbnd  33868  iocmbl  38269  supxrre3  40008  supxrgere  40016  infrpge  40034  infxrunb2  40051  infxrbnd2  40052  infleinflem2  40054  xrralrecnnle  40069  supxrunb3  40090  supminfxr2  40166  xrpnf  40183  ioomidp  40212  limsupre  40345  limsupub  40408  limsuppnflem  40414  limsupre3lem  40436  liminfgord  40458  liminflelimsuplem  40479  limsupgtlem  40481  xlimmnfvlem2  40531  xlimmnfv  40532  xlimpnfvlem2  40535  xlimpnfv  40536  icccncfext  40572  volioc  40660  volico  40672  fourierdlem113  40908  meaiuninclem  41169  meaiuninc3v  41173  icoresmbl  41232  ovolval5lem1  41341  mbfresmf  41423  cnfsmf  41424  incsmf  41426  smfconst  41433  decsmf  41450  smfres  41472  smfco  41484  issmfle2d  41490  bgoldbtbndlem3  42174