Theorem rexri 10299

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

Step	Hyp	Ref	Expression
1		rexri.1	. 2 ⊢ 𝐴 ∈ ℝ
2		rexr 10287	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ*

Syntax hints:   ∈ wcel 2145  ℝcr 10137  ℝ^*cxr 10275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-xr 10280

This theorem is referenced by:  xnn0n0n1ge2b  12170  xmulid1  12314  xmulid2  12315  xmulm1  12316  x2times  12334  xov1plusxeqvd  12525  ico01fl0  12828  hashge1  13380  hashgt12el  13412  hashgt12el2  13413  hashge2el2difr  13465  sgn1  14040  fprodge1  14932  tanhbnd  15097  halfleoddlt  15294  isnzr2hash  19479  0ringnnzr  19484  xrsnsgrp  19997  leordtval2  21237  nmoid  22766  metnrmlem1a  22881  metnrmlem1  22882  icopnfcnv  22961  icopnfhmeo  22962  iccpnfcnv  22963  iccpnfhmeo  22964  oprpiece1res1  22970  oprpiece1res2  22971  pcoass  23043  vitalilem4  23599  itg2monolem1  23737  itg2monolem3  23739  abelthlem3  24407  abelth  24415  neghalfpirx  24439  sincosq1sgn  24471  sincosq2sgn  24472  sincosq4sgn  24474  coseq00topi  24475  coseq0negpitopi  24476  tanabsge  24479  sinq12gt0  24480  cosq14gt0  24483  cosordlem  24498  tanord1  24504  tanord  24505  tanregt0  24506  negpitopissre  24507  ellogrn  24527  logimclad  24540  argregt0  24577  argimgt0  24579  argimlt0  24580  dvloglem  24615  logf1o2  24617  dvlog2lem  24619  efopnlem2  24624  isosctrlem1  24769  asinneg  24834  asinsinlem  24839  acoscos  24841  reasinsin  24844  atanlogsublem  24863  atantan  24871  atanbndlem  24873  atanbnd  24874  atan1  24876  scvxcvx  24933  dchrvmasumlem2  25408  dchrvmasumiflem1  25411  pntibndlem1  25499  pntibndlem2  25501  pntibnd  25503  pntlemc  25505  pnt  25524  padicabvf  25541  padicabvcxp  25542  tgldimor  25618  upgrfi  26207  umgrislfupgrlem  26238  upgrewlkle2  26737  upgr2pthnlp  26863  nmopun  29213  nmoptrii  29293  nmopcoi  29294  pjnmopi  29347  xlt2addrd  29863  xdivrec  29975  xrsmulgzz  30018  xrnarchi  30078  unitssxrge0  30286  xrge0iifcnv  30319  xrge0iifiso  30321  xrge0iifhom  30323  hasheuni  30487  ddemeas  30639  prob01  30815  sgnsgn  30950  chtvalz  31047  dnizeq0  32802  cnndvlem1  32865  bj-pinftyccb  33445  bj-minftyccb  33449  bj-pinftynminfty  33451  sin2h  33732  cos2h  33733  tan2h  33734  broucube  33776  asindmre  33827  dvasin  33828  dvacos  33829  areacirclem1  33832  areaquad  38328  imo72b2  39001  cvgdvgrat  39038  isosctrlem1ALT  39692  sineq0ALT  39695  supxrgelem  40069  xrlexaddrp  40084  infxr  40099  infleinflem2  40103  1xr  40202  limsup10exlem  40522  limsup10ex  40523  liminf10ex  40524  itgsin0pilem1  40683  fourierdlem24  40865  fourierdlem38  40879  fourierdlem43  40884  fourierdlem44  40885  fourierdlem46  40886  fourierdlem62  40902  fourierdlem74  40914  fourierdlem75  40915  fourierdlem85  40925  fourierdlem88  40928  fourierdlem93  40933  fourierdlem102  40942  fourierdlem103  40943  fourierdlem104  40944  fourierdlem111  40951  fourierdlem112  40952  fourierdlem114  40954  sqwvfoura  40962  sqwvfourb  40963  fourierswlem  40964  fouriersw  40965  fouriercn  40966  salexct2  41074  salgencntex  41078  ovn0lem  41299  mod42tp1mod8  42047  bgoldbtbndlem1  42221  bgoldbtbnd  42225  pgrpgt2nabl  42675  expnegico01  42836  regt1loggt0  42858  rege1logbrege0  42880  rege1logbzge0  42881  dignnld  42925