MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrpii Structured version   Unicode version

Theorem elrpii 11097
Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
Hypotheses
Ref Expression
elrpi.1  |-  A  e.  RR
elrpi.2  |-  0  <  A
Assertion
Ref Expression
elrpii  |-  A  e.  RR+

Proof of Theorem elrpii
StepHypRef Expression
1 elrpi.1 . 2  |-  A  e.  RR
2 elrpi.2 . 2  |-  0  <  A
3 elrp 11096 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3mpbir2an 911 1  |-  A  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   class class class wbr 4392   RRcr 9384   0cc0 9385    < clt 9521   RR+crp 11094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-br 4393  df-rp 11095
This theorem is referenced by:  1rp  11098  2rp  11099  iexpcyc  12073  discr  12104  sqrlem7  12842  caurcvgr  13255  epr  13594  aaliou3lem1  21926  aaliou3lem2  21927  aaliou3lem3  21928  pige3  22097  sineq0  22101  cosordlem  22105  tanord1  22111  tanregt0  22113  efif1olem2  22117  argregt0  22177  argrege0  22178  logimul  22181  efopn  22221  cxpsqrlem  22265  isosctrlem1  22334  asinsin  22405  asin1  22407  reasinsin  22409  atanbnd  22439  atan1  22441  log2cnv  22457  basellem1  22536  basellem4  22539  cht3  22629  chtublem  22668  chtub  22669  bposlem6  22746  lgsdir2lem1  22780  lgsdir2lem4  22783  lgsdir2lem5  22784  2sqlem11  22832  chebbnd1lem3  22838  chebbnd1  22839  chto1ub  22843  dchrvmasumiflem1  22868  pntlemg  22965  pntlemr  22969  pntlemf  22972  minvecolem3  24414  ballotlem2  27007  circum  27455  dvtanlem  28581  cntotbnd  28835  heiborlem5  28854  heiborlem7  28856  stoweidlem5  29940  stoweidlem28  29963  stoweidlem59  29994  stoweid  29998  wallispilem3  30002  stirlinglem12  30020  stirlingr  30025  isosctrlem1ALT  31972  sineq0ALT  31975
  Copyright terms: Public domain W3C validator