Theorem rexri 11271

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

This proof depends on syntax axioms:   ∈ wcel 2143  ℝcr 11103  ℝ^*cxr 11246

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-xr 11251

This theorem is used by:  1xr  11272  xnn0n0n1ge2b  13161  hashgt23el  14466  hashge2el2difr  14523  tanhbnd  16221  halfleoddlt  16424  oprpiece1res1  25119  oprpiece1res2  25120  pcoass  25192  vitalilem4  25779  neghalfpirx  26640  sincosq1sgn  26672  sincosq2sgn  26673  sincosq4sgn  26675  coseq00topi  26676  coseq0negpitopi  26677  tanabsge  26680  sinq12gt0  26681  cosq14gt0  26684  cos02pilt1  26700  cosq34lt1  26701  cosordlem  26704  cos0pilt1  26706  tanord1  26711  tanord  26712  tanregt0  26713  negpitopissre  26714  ellogrn  26733  logimclad  26746  argregt0  26784  argimgt0  26786  argimlt0  26787  dvloglem  26822  logf1o2  26824  efopnlem2  26831  isosctrlem1  26992  asinneg  27060  asinsinlem  27065  acoscos  27067  reasinsin  27070  atanlogsublem  27089  atantan  27097  atanbndlem  27099  atanbnd  27100  atan1  27102  dchrvmasumlem2  27671  dchrvmasumiflem1  27674  tgldimor  28780  upgrfi  29450  umgrislfupgrlem  29481  upgrewlkle2  29965  upgr2pthnlp  30090  nmoptrii  32455  nmopcoi  32456  sgnsgn  33184  rtelextdg2lem  34125  chtvalz  35025  lfuhgr2  35619  usgrcyclgt2v  35631  acycgr2v  35650  cusgracyclt3v  35656  dnizeq0  37092  cnndvlem1  37154  bj-pinftyccb  37893  bj-minftyccb  37897  bj-pinftynminfty  37899  sin2h  38289  cos2h  38290  tan2h  38291  asindmre  38382  dvasin  38383  dvacos  38384  areacirclem1  38387  acos1half  43147  areaquad  43971  isosctrlem1ALT  45670  sineq0ALT  45673  itgsin0pilem1  46692  fourierdlem24  46873  fourierdlem38  46887  fourierdlem43  46892  fourierdlem44  46893  fourierdlem46  46894  fourierdlem62  46910  fourierdlem74  46922  fourierdlem75  46923  fourierdlem85  46933  fourierdlem88  46936  fourierdlem93  46941  fourierdlem102  46950  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  fourierdlem112  46960  fourierdlem114  46962  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  fouriercn  46974  salexct2  47081  goldrapos  47648  rehalfge1  48104  mod42tp1mod8  48382  bgoldbtbndlem1  48598  bgoldbtbnd  48602  pgrpgt2nabl  49174  sepfsepc  49734