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

Theorem rexri 11220
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 11208 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
31, 2ax-mp 5 1 𝐴 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cr 11057  *cxr 11195
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-in 3922  df-ss 3932  df-xr 11200
This theorem is referenced by:  1xr  11221  xnn0n0n1ge2b  13059  hashgt23el  14331  hashge2el2difr  14387  tanhbnd  16050  halfleoddlt  16251  oprpiece1res1  24330  oprpiece1res2  24331  pcoass  24403  vitalilem4  24991  neghalfpirx  25839  sincosq1sgn  25871  sincosq2sgn  25872  sincosq4sgn  25874  coseq00topi  25875  coseq0negpitopi  25876  tanabsge  25879  sinq12gt0  25880  cosq14gt0  25883  cos02pilt1  25898  cosq34lt1  25899  cosordlem  25902  cos0pilt1  25904  tanord1  25909  tanord  25910  tanregt0  25911  negpitopissre  25912  ellogrn  25931  logimclad  25944  argregt0  25981  argimgt0  25983  argimlt0  25984  dvloglem  26019  logf1o2  26021  efopnlem2  26028  isosctrlem1  26184  asinneg  26252  asinsinlem  26257  acoscos  26259  reasinsin  26262  atanlogsublem  26281  atantan  26289  atanbndlem  26291  atanbnd  26292  atan1  26294  dchrvmasumlem2  26862  dchrvmasumiflem1  26865  tgldimor  27486  upgrfi  28084  umgrislfupgrlem  28115  upgrewlkle2  28596  upgr2pthnlp  28722  nmoptrii  31078  nmopcoi  31079  sgnsgn  33188  chtvalz  33282  lfuhgr2  33752  usgrcyclgt2v  33765  acycgr2v  33784  cusgracyclt3v  33790  dnizeq0  34967  cnndvlem1  35029  bj-pinftyccb  35721  bj-minftyccb  35725  bj-pinftynminfty  35727  sin2h  36097  cos2h  36098  tan2h  36099  asindmre  36190  dvasin  36191  dvacos  36192  areacirclem1  36195  acos1half  40651  areaquad  41579  isosctrlem1ALT  43290  sineq0ALT  43293  itgsin0pilem1  44265  fourierdlem24  44446  fourierdlem38  44460  fourierdlem43  44465  fourierdlem44  44466  fourierdlem46  44467  fourierdlem62  44483  fourierdlem74  44495  fourierdlem75  44496  fourierdlem85  44506  fourierdlem88  44509  fourierdlem93  44514  fourierdlem102  44523  fourierdlem103  44524  fourierdlem104  44525  fourierdlem111  44532  fourierdlem112  44533  fourierdlem114  44535  sqwvfoura  44543  sqwvfourb  44544  fourierswlem  44545  fouriersw  44546  fouriercn  44547  salexct2  44654  mod42tp1mod8  45868  bgoldbtbndlem1  46071  bgoldbtbnd  46075  pgrpgt2nabl  46516  sepfsepc  47034
  Copyright terms: Public domain W3C validator