Theorem rexri 11192

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

Syntax hints:   ∈ wcel 2109  ℝcr 11027  ℝ^*cxr 11167

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-xr 11172

This theorem is referenced by:  1xr  11193  xnn0n0n1ge2b  13052  hashgt23el  14349  hashge2el2difr  14406  tanhbnd  16088  halfleoddlt  16291  oprpiece1res1  24865  oprpiece1res2  24866  pcoass  24940  vitalilem4  25528  neghalfpirx  26391  sincosq1sgn  26423  sincosq2sgn  26424  sincosq4sgn  26426  coseq00topi  26427  coseq0negpitopi  26428  tanabsge  26431  sinq12gt0  26432  cosq14gt0  26435  cos02pilt1  26451  cosq34lt1  26452  cosordlem  26455  cos0pilt1  26457  tanord1  26462  tanord  26463  tanregt0  26464  negpitopissre  26465  ellogrn  26484  logimclad  26497  argregt0  26535  argimgt0  26537  argimlt0  26538  dvloglem  26573  logf1o2  26575  efopnlem2  26582  isosctrlem1  26744  asinneg  26812  asinsinlem  26817  acoscos  26819  reasinsin  26822  atanlogsublem  26841  atantan  26849  atanbndlem  26851  atanbnd  26852  atan1  26854  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  tgldimor  28465  upgrfi  29054  umgrislfupgrlem  29085  upgrewlkle2  29570  upgr2pthnlp  29695  nmoptrii  32056  nmopcoi  32057  sgnsgn  32799  rtelextdg2lem  33692  chtvalz  34596  lfuhgr2  35091  usgrcyclgt2v  35103  acycgr2v  35122  cusgracyclt3v  35128  dnizeq0  36448  cnndvlem1  36510  bj-pinftyccb  37194  bj-minftyccb  37198  bj-pinftynminfty  37200  sin2h  37589  cos2h  37590  tan2h  37591  asindmre  37682  dvasin  37683  dvacos  37684  areacirclem1  37687  acos1half  42331  areaquad  43189  isosctrlem1ALT  44907  sineq0ALT  44910  itgsin0pilem1  45932  fourierdlem24  46113  fourierdlem38  46127  fourierdlem43  46132  fourierdlem44  46133  fourierdlem46  46134  fourierdlem62  46150  fourierdlem74  46162  fourierdlem75  46163  fourierdlem85  46173  fourierdlem88  46176  fourierdlem93  46181  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fourierdlem112  46200  fourierdlem114  46202  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  fouriercn  46214  salexct2  46321  rehalfge1  47320  mod42tp1mod8  47587  bgoldbtbndlem1  47790  bgoldbtbnd  47794  pgrpgt2nabl  48351  sepfsepc  48913