Theorem rexri 11285

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

This proof depends on syntax axioms:   ∈ wcel 2146  ℝcr 11117  ℝ^*cxr 11260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-xr 11265

This theorem is used by:  1xr  11286  xnn0n0n1ge2b  13175  hashgt23el  14481  hashge2el2difr  14538  tanhbnd  16242  halfleoddlt  16445  oprpiece1res1  25147  oprpiece1res2  25148  pcoass  25220  vitalilem4  25807  neghalfpirx  26668  sincosq1sgn  26700  sincosq2sgn  26701  sincosq4sgn  26703  coseq00topi  26704  coseq0negpitopi  26705  tanabsge  26708  sinq12gt0  26709  cosq14gt0  26712  cos02pilt1  26728  cosq34lt1  26729  cosordlem  26732  cos0pilt1  26734  tanord1  26739  tanord  26740  tanregt0  26741  negpitopissre  26742  ellogrn  26761  logimclad  26774  argregt0  26812  argimgt0  26814  argimlt0  26815  dvloglem  26850  logf1o2  26852  efopnlem2  26859  isosctrlem1  27020  asinneg  27088  asinsinlem  27093  acoscos  27095  reasinsin  27098  atanlogsublem  27117  atantan  27125  atanbndlem  27127  atanbnd  27128  atan1  27130  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  tgldimor  28808  upgrfi  29478  umgrislfupgrlem  29509  upgrewlkle2  29993  upgr2pthnlp  30118  nmoptrii  32483  nmopcoi  32484  sgnsgn  33212  rtelextdg2lem  34147  chtvalz  35048  lfuhgr2  35632  usgrcyclgt2v  35644  acycgr2v  35663  cusgracyclt3v  35669  dnizeq0  37105  cnndvlem1  37167  bj-pinftyccb  37906  bj-minftyccb  37910  bj-pinftynminfty  37912  sin2h  38302  cos2h  38303  tan2h  38304  asindmre  38395  dvasin  38396  dvacos  38397  areacirclem1  38400  acos1half  43160  areaquad  43984  isosctrlem1ALT  45683  sineq0ALT  45686  itgsin0pilem1  46705  fourierdlem24  46886  fourierdlem38  46900  fourierdlem43  46905  fourierdlem44  46906  fourierdlem46  46907  fourierdlem62  46923  fourierdlem74  46935  fourierdlem75  46936  fourierdlem85  46946  fourierdlem88  46949  fourierdlem93  46954  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fourierdlem112  46973  fourierdlem114  46975  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  fouriercn  46987  salexct2  47094  goldrapos  47661  rehalfge1  48117  mod42tp1mod8  48395  bgoldbtbndlem1  48611  bgoldbtbnd  48615  pgrpgt2nabl  49187  sepfsepc  49747