Theorem rexri 11370

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

This proof depends on syntax axioms:   ∈ wcel 2144  ℝcr 11202  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-xr 11350

This theorem is used by:  1xr  11371  xnn0n0n1ge2b  13264  hashgt23el  14572  hashge2el2difr  14629  tanhbnd  16334  halfleoddlt  16537  oprpiece1res1  25277  oprpiece1res2  25278  pcoass  25350  vitalilem4  25937  neghalfpirx  26800  sincosq1sgn  26832  sincosq2sgn  26833  sincosq4sgn  26835  coseq00topi  26836  coseq0negpitopi  26837  tanabsge  26840  sinq12gt0  26841  cosq14gt0  26844  cos02pilt1  26859  cosq34lt1  26860  cosordlem  26863  cos0pilt1  26865  tanord1  26870  tanord  26871  tanregt0  26872  negpitopissre  26873  ellogrn  26892  logimclad  26905  argregt0  26943  argimgt0  26945  argimlt0  26946  dvloglem  26981  logf1o2  26983  efopnlem2  26990  isosctrlem1  27151  asinneg  27219  asinsinlem  27224  acoscos  27226  reasinsin  27229  atanlogsublem  27248  atantan  27256  atanbndlem  27258  atanbnd  27259  atan1  27261  dchrvmasumlem2  27830  dchrvmasumiflem1  27833  tgldimor  28970  upgrfi  29674  umgrislfupgrlem  29705  lfuhgr2  29732  upgrewlkle2  30192  upgr2pthnlp  30323  nmoptrii  32701  nmopcoi  32702  sgnsgn  33468  rtelextdg2lem  34404  chtvalz  35304  usgrcyclgt2v  35986  acycgr2v  35991  cusgracyclt3v  35997  dnizeq0  37433  cnndvlem1  37495  bj-pinftyccb  38235  bj-minftyccb  38239  bj-pinftynminfty  38241  sin2h  38626  cos2h  38627  tan2h  38628  asindmre  38714  dvasin  38715  dvacos  38716  areacirclem1  38719  acos1half  43502  areaquad  44311  isosctrlem1ALT  46009  sineq0ALT  46012  itgsin0pilem1  47053  fourierdlem24  47234  fourierdlem38  47248  fourierdlem43  47253  fourierdlem44  47254  fourierdlem46  47255  fourierdlem62  47271  fourierdlem74  47283  fourierdlem75  47284  fourierdlem85  47294  fourierdlem88  47297  fourierdlem93  47302  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fourierdlem112  47321  fourierdlem114  47323  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  fouriercn  47335  salexct2  47442  goldrapos  48023  rehalfge1  48502  mod42tp1mod8  48780  bgoldbtbndlem1  48996  bgoldbtbnd  49000  pgrpgt2nabl  49571  sepfsepc  50135