Theorem rexri 11237

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

Syntax hints:   ∈ wcel 2141  ℝcr 11069  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-xr 11217

This theorem is referenced by:  1xr  11238  xnn0n0n1ge2b  13131  hashgt23el  14434  hashge2el2difr  14491  tanhbnd  16176  halfleoddlt  16379  oprpiece1res1  24993  oprpiece1res2  24994  pcoass  25066  vitalilem4  25653  neghalfpirx  26508  sincosq1sgn  26540  sincosq2sgn  26541  sincosq4sgn  26543  coseq00topi  26544  coseq0negpitopi  26545  tanabsge  26548  sinq12gt0  26549  cosq14gt0  26552  cos02pilt1  26568  cosq34lt1  26569  cosordlem  26572  cos0pilt1  26574  tanord1  26579  tanord  26580  tanregt0  26581  negpitopissre  26582  ellogrn  26601  logimclad  26614  argregt0  26652  argimgt0  26654  argimlt0  26655  dvloglem  26690  logf1o2  26692  efopnlem2  26699  isosctrlem1  26860  asinneg  26928  asinsinlem  26933  acoscos  26935  reasinsin  26938  atanlogsublem  26957  atantan  26965  atanbndlem  26967  atanbnd  26968  atan1  26970  dchrvmasumlem2  27539  dchrvmasumiflem1  27542  tgldimor  28648  upgrfi  29238  umgrislfupgrlem  29269  upgrewlkle2  29753  upgr2pthnlp  29878  nmoptrii  32243  nmopcoi  32244  sgnsgn  32993  rtelextdg2lem  33984  chtvalz  34887  lfuhgr2  35433  usgrcyclgt2v  35445  acycgr2v  35464  cusgracyclt3v  35470  dnizeq0  36877  cnndvlem1  36939  bj-pinftyccb  37677  bj-minftyccb  37681  bj-pinftynminfty  37683  sin2h  38073  cos2h  38074  tan2h  38075  asindmre  38166  dvasin  38167  dvacos  38168  areacirclem1  38171  acos1half  42931  areaquad  43757  isosctrlem1ALT  45473  sineq0ALT  45476  itgsin0pilem1  46488  fourierdlem24  46669  fourierdlem38  46683  fourierdlem43  46688  fourierdlem44  46689  fourierdlem46  46690  fourierdlem62  46706  fourierdlem74  46718  fourierdlem75  46719  fourierdlem85  46729  fourierdlem88  46732  fourierdlem93  46737  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem112  46756  fourierdlem114  46758  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  fouriercn  46770  salexct2  46877  goldrapos  47441  rehalfge1  47897  mod42tp1mod8  48175  bgoldbtbndlem1  48391  bgoldbtbnd  48395  pgrpgt2nabl  48952  sepfsepc  49513