Theorem rexri 11291

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

Syntax hints:   ∈ wcel 2108  ℝcr 11126  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-xr 11271

This theorem is referenced by:  1xr  11292  xnn0n0n1ge2b  13146  hashgt23el  14440  hashge2el2difr  14497  tanhbnd  16177  halfleoddlt  16379  oprpiece1res1  24898  oprpiece1res2  24899  pcoass  24973  vitalilem4  25562  neghalfpirx  26425  sincosq1sgn  26457  sincosq2sgn  26458  sincosq4sgn  26460  coseq00topi  26461  coseq0negpitopi  26462  tanabsge  26465  sinq12gt0  26466  cosq14gt0  26469  cos02pilt1  26485  cosq34lt1  26486  cosordlem  26489  cos0pilt1  26491  tanord1  26496  tanord  26497  tanregt0  26498  negpitopissre  26499  ellogrn  26518  logimclad  26531  argregt0  26569  argimgt0  26571  argimlt0  26572  dvloglem  26607  logf1o2  26609  efopnlem2  26616  isosctrlem1  26778  asinneg  26846  asinsinlem  26851  acoscos  26853  reasinsin  26856  atanlogsublem  26875  atantan  26883  atanbndlem  26885  atanbnd  26886  atan1  26888  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  tgldimor  28427  upgrfi  29016  umgrislfupgrlem  29047  upgrewlkle2  29532  upgr2pthnlp  29660  nmoptrii  32021  nmopcoi  32022  sgnsgn  32766  rtelextdg2lem  33706  chtvalz  34607  lfuhgr2  35087  usgrcyclgt2v  35099  acycgr2v  35118  cusgracyclt3v  35124  dnizeq0  36439  cnndvlem1  36501  bj-pinftyccb  37185  bj-minftyccb  37189  bj-pinftynminfty  37191  sin2h  37580  cos2h  37581  tan2h  37582  asindmre  37673  dvasin  37674  dvacos  37675  areacirclem1  37678  acos1half  42348  areaquad  43187  isosctrlem1ALT  44906  sineq0ALT  44909  itgsin0pilem1  45927  fourierdlem24  46108  fourierdlem38  46122  fourierdlem43  46127  fourierdlem44  46128  fourierdlem46  46129  fourierdlem62  46145  fourierdlem74  46157  fourierdlem75  46158  fourierdlem85  46168  fourierdlem88  46171  fourierdlem93  46176  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  fouriercn  46209  salexct2  46316  rehalfge1  47312  mod42tp1mod8  47564  bgoldbtbndlem1  47767  bgoldbtbnd  47771  pgrpgt2nabl  48289  sepfsepc  48850