Theorem rexri 11295

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℝcr 11127  ℝ^*cxr 11270

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-xr 11275

This theorem is used by:  1xr  11296  xnn0n0n1ge2b  13187  hashgt23el  14493  hashge2el2difr  14550  tanhbnd  16255  halfleoddlt  16458  oprpiece1res1  25185  oprpiece1res2  25186  pcoass  25258  vitalilem4  25845  neghalfpirx  26711  sincosq1sgn  26743  sincosq2sgn  26744  sincosq4sgn  26746  coseq00topi  26747  coseq0negpitopi  26748  tanabsge  26751  sinq12gt0  26752  cosq14gt0  26755  cos02pilt1  26771  cosq34lt1  26772  cosordlem  26775  cos0pilt1  26777  tanord1  26782  tanord  26783  tanregt0  26784  negpitopissre  26785  ellogrn  26804  logimclad  26817  argregt0  26855  argimgt0  26857  argimlt0  26858  dvloglem  26893  logf1o2  26895  efopnlem2  26902  isosctrlem1  27063  asinneg  27131  asinsinlem  27136  acoscos  27138  reasinsin  27141  atanlogsublem  27160  atantan  27168  atanbndlem  27170  atanbnd  27171  atan1  27173  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  tgldimor  28852  upgrfi  29556  umgrislfupgrlem  29587  lfuhgr2  29614  upgrewlkle2  30074  upgr2pthnlp  30205  nmoptrii  32583  nmopcoi  32584  sgnsgn  33309  rtelextdg2lem  34244  chtvalz  35145  usgrcyclgt2v  35732  acycgr2v  35737  cusgracyclt3v  35743  dnizeq0  37180  cnndvlem1  37242  bj-pinftyccb  37981  bj-minftyccb  37985  bj-pinftynminfty  37987  sin2h  38372  cos2h  38373  tan2h  38374  asindmre  38460  dvasin  38461  dvacos  38462  areacirclem1  38465  acos1half  43241  areaquad  44065  isosctrlem1ALT  45764  sineq0ALT  45767  itgsin0pilem1  46786  fourierdlem24  46967  fourierdlem38  46981  fourierdlem43  46986  fourierdlem44  46987  fourierdlem46  46988  fourierdlem62  47004  fourierdlem74  47016  fourierdlem75  47017  fourierdlem85  47027  fourierdlem88  47030  fourierdlem93  47035  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  fourierdlem114  47056  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  fouriercn  47068  salexct2  47175  goldrapos  47756  rehalfge1  48235  mod42tp1mod8  48513  bgoldbtbndlem1  48729  bgoldbtbnd  48733  pgrpgt2nabl  49304  sepfsepc  49862