Theorem rexri 10097

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 10085	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ*

Syntax hints:   ∈ wcel 1990  ℝcr 9935  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078

This theorem is referenced by:  xnn0n0n1ge2b  11965  xmulid1  12109  xmulid2  12110  xmulm1  12111  x2times  12129  xov1plusxeqvd  12318  ico01fl0  12620  hashge1  13178  hashgt12el  13210  hashgt12el2  13211  hashge2el2difr  13263  sgn1  13832  fprodge1  14726  tanhbnd  14891  halfleoddlt  15086  isnzr2hash  19264  0ringnnzr  19269  xrsnsgrp  19782  leordtval2  21016  nmoid  22546  metnrmlem1a  22661  metnrmlem1  22662  icopnfcnv  22741  icopnfhmeo  22742  iccpnfcnv  22743  iccpnfhmeo  22744  oprpiece1res1  22750  oprpiece1res2  22751  pcoass  22824  vitalilem4  23380  itg2monolem1  23517  itg2monolem3  23519  abelthlem3  24187  abelth  24195  neghalfpirx  24218  sincosq1sgn  24250  sincosq2sgn  24251  sincosq4sgn  24253  coseq00topi  24254  coseq0negpitopi  24255  tanabsge  24258  sinq12gt0  24259  cosq14gt0  24262  cosordlem  24277  tanord1  24283  tanord  24284  tanregt0  24285  negpitopissre  24286  ellogrn  24306  logimclad  24319  argregt0  24356  argimgt0  24358  argimlt0  24359  dvloglem  24394  logf1o2  24396  dvlog2lem  24398  efopnlem2  24403  isosctrlem1  24548  asinneg  24613  asinsinlem  24618  acoscos  24620  reasinsin  24623  atanlogsublem  24642  atantan  24650  atanbndlem  24652  atanbnd  24653  atan1  24655  scvxcvx  24712  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  pntibndlem1  25278  pntibndlem2  25280  pntibnd  25282  pntlemc  25284  pnt  25303  padicabvf  25320  padicabvcxp  25321  tgldimor  25397  upgrfi  25986  umgrislfupgrlem  26017  upgrewlkle2  26502  upgr2pthnlp  26628  nmopun  28873  nmoptrii  28953  nmopcoi  28954  pjnmopi  29007  xlt2addrd  29523  xdivrec  29635  xrsmulgzz  29678  xrnarchi  29738  unitssxrge0  29946  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  hasheuni  30147  ddemeas  30299  prob01  30475  sgnsgn  30610  chtvalz  30707  dnizeq0  32465  cnndvlem1  32528  bj-pinftyccb  33108  bj-minftyccb  33112  bj-pinftynminfty  33114  sin2h  33399  cos2h  33400  tan2h  33401  broucube  33443  asindmre  33495  dvasin  33496  dvacos  33497  areacirclem1  33500  areaquad  37802  imo72b2  38475  cvgdvgrat  38512  isosctrlem1ALT  39170  sineq0ALT  39173  supxrgelem  39553  xrlexaddrp  39568  infxr  39583  infleinflem2  39587  1xr  39686  limsup10exlem  40004  limsup10ex  40005  liminf10ex  40006  itgsin0pilem1  40165  fourierdlem24  40348  fourierdlem38  40362  fourierdlem43  40367  fourierdlem44  40368  fourierdlem46  40369  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  fourierdlem85  40408  fourierdlem88  40411  fourierdlem93  40416  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  fouriercn  40449  salexct2  40557  salgencntex  40561  ovn0lem  40779  mod42tp1mod8  41519  bgoldbtbndlem1  41693  bgoldbtbnd  41697  pgrpgt2nabl  42147  expnegico01  42308  regt1loggt0  42330  rege1logbrege0  42352  rege1logbzge0  42353  dignnld  42397