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

Theorem rexri 10135
Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
Hypothesis
Ref Expression
rexri.1 𝐴 ∈ ℝ
Assertion
Ref Expression
rexri 𝐴 ∈ ℝ*

Proof of Theorem rexri
StepHypRef Expression
1 rexri.1 . 2 𝐴 ∈ ℝ
2 rexr 10123 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  cr 9973  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-xr 10116
This theorem is referenced by:  xnn0n0n1ge2b  12003  xmulid1  12147  xmulid2  12148  xmulm1  12149  x2times  12167  xov1plusxeqvd  12356  ico01fl0  12660  hashge1  13216  hashgt12el  13248  hashgt12el2  13249  hashge2el2difr  13301  sgn1  13876  fprodge1  14770  tanhbnd  14935  halfleoddlt  15133  isnzr2hash  19312  0ringnnzr  19317  xrsnsgrp  19830  leordtval2  21064  nmoid  22593  metnrmlem1a  22708  metnrmlem1  22709  icopnfcnv  22788  icopnfhmeo  22789  iccpnfcnv  22790  iccpnfhmeo  22791  oprpiece1res1  22797  oprpiece1res2  22798  pcoass  22870  vitalilem4  23425  itg2monolem1  23562  itg2monolem3  23564  abelthlem3  24232  abelth  24240  neghalfpirx  24263  sincosq1sgn  24295  sincosq2sgn  24296  sincosq4sgn  24298  coseq00topi  24299  coseq0negpitopi  24300  tanabsge  24303  sinq12gt0  24304  cosq14gt0  24307  cosordlem  24322  tanord1  24328  tanord  24329  tanregt0  24330  negpitopissre  24331  ellogrn  24351  logimclad  24364  argregt0  24401  argimgt0  24403  argimlt0  24404  dvloglem  24439  logf1o2  24441  dvlog2lem  24443  efopnlem2  24448  isosctrlem1  24593  asinneg  24658  asinsinlem  24663  acoscos  24665  reasinsin  24668  atanlogsublem  24687  atantan  24695  atanbndlem  24697  atanbnd  24698  atan1  24700  scvxcvx  24757  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  pntibndlem1  25323  pntibndlem2  25325  pntibnd  25327  pntlemc  25329  pnt  25348  padicabvf  25365  padicabvcxp  25366  tgldimor  25442  upgrfi  26031  umgrislfupgrlem  26062  upgrewlkle2  26558  upgr2pthnlp  26684  nmopun  29001  nmoptrii  29081  nmopcoi  29082  pjnmopi  29135  xlt2addrd  29651  xdivrec  29763  xrsmulgzz  29806  xrnarchi  29866  unitssxrge0  30074  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  hasheuni  30275  ddemeas  30427  prob01  30603  sgnsgn  30738  chtvalz  30835  dnizeq0  32590  cnndvlem1  32653  bj-pinftyccb  33238  bj-minftyccb  33242  bj-pinftynminfty  33244  sin2h  33529  cos2h  33530  tan2h  33531  broucube  33573  asindmre  33625  dvasin  33626  dvacos  33627  areacirclem1  33630  areaquad  38119  imo72b2  38792  cvgdvgrat  38829  isosctrlem1ALT  39484  sineq0ALT  39487  supxrgelem  39866  xrlexaddrp  39881  infxr  39896  infleinflem2  39900  1xr  39999  limsup10exlem  40322  limsup10ex  40323  liminf10ex  40324  itgsin0pilem1  40483  fourierdlem24  40666  fourierdlem38  40680  fourierdlem43  40685  fourierdlem44  40686  fourierdlem46  40687  fourierdlem62  40703  fourierdlem74  40715  fourierdlem75  40716  fourierdlem85  40726  fourierdlem88  40729  fourierdlem93  40734  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  fouriercn  40767  salexct2  40875  salgencntex  40879  ovn0lem  41100  mod42tp1mod8  41844  bgoldbtbndlem1  42018  bgoldbtbnd  42022  pgrpgt2nabl  42472  expnegico01  42633  regt1loggt0  42655  rege1logbrege0  42677  rege1logbzge0  42678  dignnld  42722
  Copyright terms: Public domain W3C validator