Theorem rexri 11194

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

Syntax hints:   ∈ wcel 2114  ℝcr 11028  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-xr 11174

This theorem is referenced by:  1xr  11195  xnn0n0n1ge2b  13074  hashgt23el  14377  hashge2el2difr  14434  tanhbnd  16119  halfleoddlt  16322  oprpiece1res1  24928  oprpiece1res2  24929  pcoass  25001  vitalilem4  25588  neghalfpirx  26443  sincosq1sgn  26475  sincosq2sgn  26476  sincosq4sgn  26478  coseq00topi  26479  coseq0negpitopi  26480  tanabsge  26483  sinq12gt0  26484  cosq14gt0  26487  cos02pilt1  26503  cosq34lt1  26504  cosordlem  26507  cos0pilt1  26509  tanord1  26514  tanord  26515  tanregt0  26516  negpitopissre  26517  ellogrn  26536  logimclad  26549  argregt0  26587  argimgt0  26589  argimlt0  26590  dvloglem  26625  logf1o2  26627  efopnlem2  26634  isosctrlem1  26795  asinneg  26863  asinsinlem  26868  acoscos  26870  reasinsin  26873  atanlogsublem  26892  atantan  26900  atanbndlem  26902  atanbnd  26903  atan1  26905  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  tgldimor  28584  upgrfi  29174  umgrislfupgrlem  29205  upgrewlkle2  29690  upgr2pthnlp  29815  nmoptrii  32180  nmopcoi  32181  sgnsgn  32929  rtelextdg2lem  33886  chtvalz  34789  lfuhgr2  35317  usgrcyclgt2v  35329  acycgr2v  35348  cusgracyclt3v  35354  dnizeq0  36751  cnndvlem1  36813  bj-pinftyccb  37551  bj-minftyccb  37555  bj-pinftynminfty  37557  sin2h  37945  cos2h  37946  tan2h  37947  asindmre  38038  dvasin  38039  dvacos  38040  areacirclem1  38043  acos1half  42804  areaquad  43662  isosctrlem1ALT  45378  sineq0ALT  45381  itgsin0pilem1  46396  fourierdlem24  46577  fourierdlem38  46591  fourierdlem43  46596  fourierdlem44  46597  fourierdlem46  46598  fourierdlem62  46614  fourierdlem74  46626  fourierdlem75  46627  fourierdlem85  46637  fourierdlem88  46640  fourierdlem93  46645  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  fouriercn  46678  salexct2  46785  goldrapos  47345  rehalfge1  47799  mod42tp1mod8  48077  bgoldbtbndlem1  48293  bgoldbtbnd  48297  pgrpgt2nabl  48854  sepfsepc  49415