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

Theorem rexri 10044
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 10032 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  cr 9882  *cxr 10020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3561  df-in 3563  df-ss 3570  df-xr 10025
This theorem is referenced by:  xnn0n0n1ge2b  11912  xmulid1  12055  xmulid2  12056  xmulm1  12057  x2times  12075  xov1plusxeqvd  12263  ico01fl0  12563  hashge1  13121  hashgt12el  13153  hashgt12el2  13154  hashge2el2difr  13204  sgn1  13769  fprodge1  14654  tanhbnd  14819  halfleoddlt  15013  isnzr2hash  19186  0ringnnzr  19191  xrsnsgrp  19704  leordtval2  20929  nmoid  22459  metnrmlem1a  22574  metnrmlem1  22575  icopnfcnv  22654  icopnfhmeo  22655  iccpnfcnv  22656  iccpnfhmeo  22657  oprpiece1res1  22663  oprpiece1res2  22664  pcoass  22737  vitalilem4  23293  itg2monolem1  23430  itg2monolem3  23432  abelthlem3  24098  abelth  24106  neghalfpirx  24129  sincosq1sgn  24161  sincosq2sgn  24162  sincosq4sgn  24164  coseq00topi  24165  coseq0negpitopi  24166  tanabsge  24169  sinq12gt0  24170  cosq14gt0  24173  cosordlem  24188  tanord1  24194  tanord  24195  tanregt0  24196  negpitopissre  24197  ellogrn  24217  logimclad  24230  argregt0  24267  argimgt0  24269  argimlt0  24270  dvloglem  24301  logf1o2  24303  dvlog2lem  24305  efopnlem2  24310  isosctrlem1  24455  asinneg  24520  asinsinlem  24525  acoscos  24527  reasinsin  24530  atanlogsublem  24549  atantan  24557  atanbndlem  24559  atanbnd  24560  atan1  24562  scvxcvx  24619  dchrvmasumlem2  25094  dchrvmasumiflem1  25097  pntibndlem1  25185  pntibndlem2  25187  pntibnd  25189  pntlemc  25191  pnt  25210  padicabvf  25227  padicabvcxp  25228  tgldimor  25304  upgrfi  25889  umgrislfupgrlem  25919  upgrewlkle2  26379  upgr2pthnlp  26504  frgrwopreglem2  27047  nmopun  28734  nmoptrii  28814  nmopcoi  28815  pjnmopi  28868  xlt2addrd  29379  xdivrec  29432  xrsmulgzz  29475  xrnarchi  29535  unitssxrge0  29740  xrge0iifcnv  29773  xrge0iifiso  29775  xrge0iifhom  29777  hasheuni  29940  ddemeas  30092  prob01  30268  sgnsgn  30403  dnizeq0  32128  cnndvlem1  32191  bj-pinftyccb  32762  bj-minftyccb  32766  bj-pinftynminfty  32768  sin2h  33052  cos2h  33053  tan2h  33054  broucube  33096  asindmre  33148  dvasin  33149  dvacos  33150  areacirclem1  33153  areaquad  37304  imo72b2  37978  cvgdvgrat  38015  isosctrlem1ALT  38674  sineq0ALT  38677  supxrgelem  39035  xrlexaddrp  39050  infxr  39065  infleinflem2  39069  itgsin0pilem1  39488  fourierdlem24  39671  fourierdlem38  39685  fourierdlem43  39690  fourierdlem44  39691  fourierdlem46  39692  fourierdlem62  39708  fourierdlem74  39720  fourierdlem75  39721  fourierdlem85  39731  fourierdlem88  39734  fourierdlem93  39739  fourierdlem102  39748  fourierdlem103  39749  fourierdlem104  39750  fourierdlem111  39757  fourierdlem112  39758  fourierdlem114  39760  sqwvfoura  39768  sqwvfourb  39769  fourierswlem  39770  fouriersw  39771  fouriercn  39772  salexct2  39880  salgencntex  39884  ovn0lem  40102  mod42tp1mod8  40834  bgoldbtbndlem1  40998  bgoldbtbnd  41002  pgrpgt2nabl  41451  expnegico01  41612  regt1loggt0  41638  rege1logbrege0  41660  rege1logbzge0  41661  dignnld  41705
  Copyright terms: Public domain W3C validator