Theorem rexri 10698

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

Syntax hints:   ∈ wcel 2110  ℝcr 10535  ℝ^*cxr 10673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-xr 10678

This theorem is referenced by:  1xr  10699  xnn0n0n1ge2b  12525  hashgt23el  13784  hashge2el2difr  13838  tanhbnd  15513  halfleoddlt  15710  oprpiece1res1  23554  oprpiece1res2  23555  pcoass  23627  vitalilem4  24211  neghalfpirx  25051  sincosq1sgn  25083  sincosq2sgn  25084  sincosq4sgn  25086  coseq00topi  25087  coseq0negpitopi  25088  tanabsge  25091  sinq12gt0  25092  cosq14gt0  25095  cos02pilt1  25110  cosq34lt1  25111  cosordlem  25114  tanord1  25120  tanord  25121  tanregt0  25122  negpitopissre  25123  ellogrn  25142  logimclad  25155  argregt0  25192  argimgt0  25194  argimlt0  25195  dvloglem  25230  logf1o2  25232  efopnlem2  25239  isosctrlem1  25395  asinneg  25463  asinsinlem  25468  acoscos  25470  reasinsin  25473  atanlogsublem  25492  atantan  25500  atanbndlem  25502  atanbnd  25503  atan1  25505  dchrvmasumlem2  26073  dchrvmasumiflem1  26076  tgldimor  26287  upgrfi  26875  umgrislfupgrlem  26906  upgrewlkle2  27387  upgr2pthnlp  27512  nmoptrii  29870  nmopcoi  29871  sgnsgn  31806  chtvalz  31900  lfuhgr2  32365  usgrcyclgt2v  32378  acycgr2v  32397  cusgracyclt3v  32403  dnizeq0  33814  cnndvlem1  33876  bj-pinftyccb  34502  bj-minftyccb  34506  bj-pinftynminfty  34508  sin2h  34881  cos2h  34882  tan2h  34883  asindmre  34976  dvasin  34977  dvacos  34978  areacirclem1  34981  areaquad  39821  isosctrlem1ALT  41266  sineq0ALT  41269  itgsin0pilem1  42233  fourierdlem24  42415  fourierdlem38  42429  fourierdlem43  42434  fourierdlem44  42435  fourierdlem46  42436  fourierdlem62  42452  fourierdlem74  42464  fourierdlem75  42465  fourierdlem85  42475  fourierdlem88  42478  fourierdlem93  42483  fourierdlem102  42492  fourierdlem103  42493  fourierdlem104  42494  fourierdlem111  42501  fourierdlem112  42502  fourierdlem114  42504  sqwvfoura  42512  sqwvfourb  42513  fourierswlem  42514  fouriersw  42515  fouriercn  42516  salexct2  42621  mod42tp1mod8  43766  bgoldbtbndlem1  43969  bgoldbtbnd  43973  pgrpgt2nabl  44413