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

Theorem rexri 9976
 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 9964 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1977  ℝcr 9814  ℝ*cxr 9952 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957 This theorem is referenced by:  xnn0n0n1ge2b  11841  xmulid1  11981  xmulid2  11982  xmulm1  11983  x2times  12001  xov1plusxeqvd  12189  ico01fl0  12482  hashge1  13039  hashgt12el  13070  hashgt12el2  13071  hashge2el2difr  13118  sgn1  13680  fprodge1  14565  tanhbnd  14730  halfleoddlt  14924  isnzr2hash  19085  0ringnnzr  19090  xrsnsgrp  19601  leordtval2  20826  nmoid  22356  metnrmlem1a  22469  metnrmlem1  22470  icopnfcnv  22549  icopnfhmeo  22550  iccpnfcnv  22551  iccpnfhmeo  22552  oprpiece1res1  22558  oprpiece1res2  22559  pcoass  22632  vitalilem4  23186  itg2monolem1  23323  itg2monolem3  23325  abelthlem3  23991  abelth  23999  neghalfpirx  24022  sincosq1sgn  24054  sincosq2sgn  24055  sincosq4sgn  24057  coseq00topi  24058  coseq0negpitopi  24059  tanabsge  24062  sinq12gt0  24063  cosq14gt0  24066  cosordlem  24081  tanord1  24087  tanord  24088  tanregt0  24089  negpitopissre  24090  ellogrn  24110  logimclad  24123  argregt0  24160  argimgt0  24162  argimlt0  24163  dvloglem  24194  logf1o2  24196  dvlog2lem  24198  efopnlem2  24203  isosctrlem1  24348  asinneg  24413  asinsinlem  24418  acoscos  24420  reasinsin  24423  atanlogsublem  24442  atantan  24450  atanbndlem  24452  atanbnd  24453  atan1  24455  scvxcvx  24512  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  pntibndlem1  25078  pntibndlem2  25080  pntibnd  25082  pntlemc  25084  pnt  25103  padicabvf  25120  padicabvcxp  25121  tgldimor  25197  upgrfi  25758  umgrislfupgrlem  25788  umgrafi  25851  vdgfrgragt2  26554  nmopun  28257  nmoptrii  28337  nmopcoi  28338  pjnmopi  28391  xlt2addrd  28913  xdivrec  28966  xrsmulgzz  29009  xrnarchi  29069  unitssxrge0  29274  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  hasheuni  29474  ddemeas  29626  prob01  29802  sgnsgn  29937  dnizeq0  31635  cnndvlem1  31698  bj-pinftyccb  32285  bj-minftyccb  32289  bj-pinftynminfty  32291  sin2h  32569  cos2h  32570  tan2h  32571  broucube  32613  asindmre  32665  dvasin  32666  dvacos  32667  areacirclem1  32670  areaquad  36821  imo72b2  37497  cvgdvgrat  37534  isosctrlem1ALT  38192  sineq0ALT  38195  supxrgelem  38494  xrlexaddrp  38509  infxr  38524  infleinflem2  38528  itgsin0pilem1  38841  fourierdlem24  39024  fourierdlem38  39038  fourierdlem43  39043  fourierdlem44  39044  fourierdlem46  39045  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  fourierdlem85  39084  fourierdlem88  39087  fourierdlem93  39092  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  fouriercn  39125  salexct2  39233  salgencntex  39237  ovn0lem  39455  mod42tp1mod8  40057  bgoldbtbndlem1  40221  bgoldbtbnd  40225  upgrewlkle2  40808  upgr2pthnlp  40938  frgrwopreglem2  41482  pgrpgt2nabl  41941  expnegico01  42102  regt1loggt0  42128  rege1logbrege0  42150  rege1logbzge0  42151  dignnld  42195
 Copyright terms: Public domain W3C validator