MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexri Structured version   Visualization version   GIF version

Theorem rexri 10692
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
StepHypRef Expression
1 rexri.1 . 2 𝐴 ∈ ℝ
2 rexr 10680 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  cr 10529  *cxr 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-xr 10672
This theorem is referenced by:  1xr  10693  xnn0n0n1ge2b  12518  hashgt23el  13785  hashge2el2difr  13839  tanhbnd  15510  halfleoddlt  15707  oprpiece1res1  23560  oprpiece1res2  23561  pcoass  23633  vitalilem4  24219  neghalfpirx  25063  sincosq1sgn  25095  sincosq2sgn  25096  sincosq4sgn  25098  coseq00topi  25099  coseq0negpitopi  25100  tanabsge  25103  sinq12gt0  25104  cosq14gt0  25107  cos02pilt1  25122  cosq34lt1  25123  cosordlem  25126  cos0pilt1  25128  tanord1  25133  tanord  25134  tanregt0  25135  negpitopissre  25136  ellogrn  25155  logimclad  25168  argregt0  25205  argimgt0  25207  argimlt0  25208  dvloglem  25243  logf1o2  25245  efopnlem2  25252  isosctrlem1  25408  asinneg  25476  asinsinlem  25481  acoscos  25483  reasinsin  25486  atanlogsublem  25505  atantan  25513  atanbndlem  25515  atanbnd  25516  atan1  25518  dchrvmasumlem2  26086  dchrvmasumiflem1  26089  tgldimor  26300  upgrfi  26888  umgrislfupgrlem  26919  upgrewlkle2  27400  upgr2pthnlp  27525  nmoptrii  29881  nmopcoi  29882  sgnsgn  31920  chtvalz  32014  lfuhgr2  32479  usgrcyclgt2v  32492  acycgr2v  32511  cusgracyclt3v  32517  dnizeq0  33928  cnndvlem1  33990  bj-pinftyccb  34637  bj-minftyccb  34641  bj-pinftynminfty  34643  sin2h  35046  cos2h  35047  tan2h  35048  asindmre  35139  dvasin  35140  dvacos  35141  areacirclem1  35144  areaquad  40159  isosctrlem1ALT  41633  sineq0ALT  41636  itgsin0pilem1  42585  fourierdlem24  42766  fourierdlem38  42780  fourierdlem43  42785  fourierdlem44  42786  fourierdlem46  42787  fourierdlem62  42803  fourierdlem74  42815  fourierdlem75  42816  fourierdlem85  42826  fourierdlem88  42829  fourierdlem93  42834  fourierdlem102  42843  fourierdlem103  42844  fourierdlem104  42845  fourierdlem111  42852  fourierdlem112  42853  fourierdlem114  42855  sqwvfoura  42863  sqwvfourb  42864  fourierswlem  42865  fouriersw  42866  fouriercn  42867  salexct2  42972  mod42tp1mod8  44113  bgoldbtbndlem1  44316  bgoldbtbnd  44320  pgrpgt2nabl  44761
  Copyright terms: Public domain W3C validator