Theorem rexri 11255

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

Syntax hints:   ∈ wcel 2145  ℝcr 11087  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-xr 11235

This theorem is referenced by:  1xr  11256  xnn0n0n1ge2b  13148  hashgt23el  14451  hashge2el2difr  14508  tanhbnd  16207  halfleoddlt  16410  oprpiece1res1  25071  oprpiece1res2  25072  pcoass  25144  vitalilem4  25731  neghalfpirx  26589  sincosq1sgn  26621  sincosq2sgn  26622  sincosq4sgn  26624  coseq00topi  26625  coseq0negpitopi  26626  tanabsge  26629  sinq12gt0  26630  cosq14gt0  26633  cos02pilt1  26649  cosq34lt1  26650  cosordlem  26653  cos0pilt1  26655  tanord1  26660  tanord  26661  tanregt0  26662  negpitopissre  26663  ellogrn  26682  logimclad  26695  argregt0  26733  argimgt0  26735  argimlt0  26736  dvloglem  26771  logf1o2  26773  efopnlem2  26780  isosctrlem1  26941  asinneg  27009  asinsinlem  27014  acoscos  27016  reasinsin  27019  atanlogsublem  27038  atantan  27046  atanbndlem  27048  atanbnd  27049  atan1  27051  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  tgldimor  28729  upgrfi  29350  umgrislfupgrlem  29381  upgrewlkle2  29865  upgr2pthnlp  29990  nmoptrii  32355  nmopcoi  32356  sgnsgn  33088  rtelextdg2lem  34033  chtvalz  34933  lfuhgr2  35482  usgrcyclgt2v  35494  acycgr2v  35513  cusgracyclt3v  35519  dnizeq0  36926  cnndvlem1  36988  bj-pinftyccb  37725  bj-minftyccb  37729  bj-pinftynminfty  37731  sin2h  38121  cos2h  38122  tan2h  38123  asindmre  38214  dvasin  38215  dvacos  38216  areacirclem1  38219  acos1half  42979  areaquad  43805  isosctrlem1ALT  45507  sineq0ALT  45510  itgsin0pilem1  46522  fourierdlem24  46703  fourierdlem38  46717  fourierdlem43  46722  fourierdlem44  46723  fourierdlem46  46724  fourierdlem62  46740  fourierdlem74  46752  fourierdlem75  46753  fourierdlem85  46763  fourierdlem88  46766  fourierdlem93  46771  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem112  46790  fourierdlem114  46792  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  fouriercn  46804  salexct2  46911  goldrapos  47475  rehalfge1  47931  mod42tp1mod8  48209  bgoldbtbndlem1  48425  bgoldbtbnd  48429  pgrpgt2nabl  48997  sepfsepc  49557