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

Theorem rexri 11172
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 11160 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cr 11009  *cxr 11147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-in 3916  df-ss 3926  df-xr 11152
This theorem is referenced by:  1xr  11173  xnn0n0n1ge2b  13007  hashgt23el  14278  hashge2el2difr  14334  tanhbnd  16003  halfleoddlt  16204  oprpiece1res1  24266  oprpiece1res2  24267  pcoass  24339  vitalilem4  24927  neghalfpirx  25775  sincosq1sgn  25807  sincosq2sgn  25808  sincosq4sgn  25810  coseq00topi  25811  coseq0negpitopi  25812  tanabsge  25815  sinq12gt0  25816  cosq14gt0  25819  cos02pilt1  25834  cosq34lt1  25835  cosordlem  25838  cos0pilt1  25840  tanord1  25845  tanord  25846  tanregt0  25847  negpitopissre  25848  ellogrn  25867  logimclad  25880  argregt0  25917  argimgt0  25919  argimlt0  25920  dvloglem  25955  logf1o2  25957  efopnlem2  25964  isosctrlem1  26120  asinneg  26188  asinsinlem  26193  acoscos  26195  reasinsin  26198  atanlogsublem  26217  atantan  26225  atanbndlem  26227  atanbnd  26228  atan1  26230  dchrvmasumlem2  26798  dchrvmasumiflem1  26801  tgldimor  27273  upgrfi  27871  umgrislfupgrlem  27902  upgrewlkle2  28383  upgr2pthnlp  28509  nmoptrii  30865  nmopcoi  30866  sgnsgn  32952  chtvalz  33046  lfuhgr2  33516  usgrcyclgt2v  33529  acycgr2v  33548  cusgracyclt3v  33554  dnizeq0  34870  cnndvlem1  34932  bj-pinftyccb  35624  bj-minftyccb  35628  bj-pinftynminfty  35630  sin2h  36000  cos2h  36001  tan2h  36002  asindmre  36093  dvasin  36094  dvacos  36095  areacirclem1  36098  acos1half  40554  areaquad  41453  isosctrlem1ALT  43121  sineq0ALT  43124  itgsin0pilem1  44086  fourierdlem24  44267  fourierdlem38  44281  fourierdlem43  44286  fourierdlem44  44287  fourierdlem46  44288  fourierdlem62  44304  fourierdlem74  44316  fourierdlem75  44317  fourierdlem85  44327  fourierdlem88  44330  fourierdlem93  44335  fourierdlem102  44344  fourierdlem103  44345  fourierdlem104  44346  fourierdlem111  44353  fourierdlem112  44354  fourierdlem114  44356  sqwvfoura  44364  sqwvfourb  44365  fourierswlem  44366  fouriersw  44367  fouriercn  44368  salexct2  44475  mod42tp1mod8  45689  bgoldbtbndlem1  45892  bgoldbtbnd  45896  pgrpgt2nabl  46337  sepfsepc  46855
  Copyright terms: Public domain W3C validator