Theorem rexri 11239

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

Syntax hints:   ∈ wcel 2109  ℝcr 11074  ℝ^*cxr 11214

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219

This theorem is referenced by:  1xr  11240  xnn0n0n1ge2b  13099  hashgt23el  14396  hashge2el2difr  14453  tanhbnd  16136  halfleoddlt  16339  oprpiece1res1  24856  oprpiece1res2  24857  pcoass  24931  vitalilem4  25519  neghalfpirx  26382  sincosq1sgn  26414  sincosq2sgn  26415  sincosq4sgn  26417  coseq00topi  26418  coseq0negpitopi  26419  tanabsge  26422  sinq12gt0  26423  cosq14gt0  26426  cos02pilt1  26442  cosq34lt1  26443  cosordlem  26446  cos0pilt1  26448  tanord1  26453  tanord  26454  tanregt0  26455  negpitopissre  26456  ellogrn  26475  logimclad  26488  argregt0  26526  argimgt0  26528  argimlt0  26529  dvloglem  26564  logf1o2  26566  efopnlem2  26573  isosctrlem1  26735  asinneg  26803  asinsinlem  26808  acoscos  26810  reasinsin  26813  atanlogsublem  26832  atantan  26840  atanbndlem  26842  atanbnd  26843  atan1  26845  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  tgldimor  28436  upgrfi  29025  umgrislfupgrlem  29056  upgrewlkle2  29541  upgr2pthnlp  29669  nmoptrii  32030  nmopcoi  32031  sgnsgn  32773  rtelextdg2lem  33723  chtvalz  34627  lfuhgr2  35113  usgrcyclgt2v  35125  acycgr2v  35144  cusgracyclt3v  35150  dnizeq0  36470  cnndvlem1  36532  bj-pinftyccb  37216  bj-minftyccb  37220  bj-pinftynminfty  37222  sin2h  37611  cos2h  37612  tan2h  37613  asindmre  37704  dvasin  37705  dvacos  37706  areacirclem1  37709  acos1half  42353  areaquad  43212  isosctrlem1ALT  44930  sineq0ALT  44933  itgsin0pilem1  45955  fourierdlem24  46136  fourierdlem38  46150  fourierdlem43  46155  fourierdlem44  46156  fourierdlem46  46157  fourierdlem62  46173  fourierdlem74  46185  fourierdlem75  46186  fourierdlem85  46196  fourierdlem88  46199  fourierdlem93  46204  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  fouriercn  46237  salexct2  46344  rehalfge1  47340  mod42tp1mod8  47607  bgoldbtbndlem1  47810  bgoldbtbnd  47814  pgrpgt2nabl  48358  sepfsepc  48920