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

Theorem elrpii 10373
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 10372 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3mpbir2an 886 1  |-  A  e.  RR+
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  1rp  10374  2rp  10375  iexpcyc  11223  discr  11254  sqrlem7  11750  caurcvgr  12162  epr  12502  aaliou3lem1  19738  aaliou3lem2  19739  aaliou3lem3  19740  pige3  19901  sineq0  19905  cosordlem  19909  tanord1  19915  tanregt0  19917  efif1olem2  19921  argregt0  19980  argrege0  19981  logimul  19984  efopn  20021  cxpsqrlem  20065  isosctrlem1  20134  asinsin  20204  asin1  20206  reasinsin  20208  atanbnd  20238  atan1  20240  log2cnv  20256  basellem1  20334  basellem4  20337  cht3  20427  chtublem  20466  chtub  20467  bposlem6  20544  lgsdir2lem1  20578  lgsdir2lem4  20581  lgsdir2lem5  20582  2sqlem11  20630  chebbnd1lem3  20636  chebbnd1  20637  chto1ub  20641  dchrvmasumiflem1  20666  pntlemg  20763  pntlemr  20767  pntlemf  20770  minvecolem3  21471  ballotlem2  23063  circum  24022  cntotbnd  26623  heiborlem5  26642  heiborlem7  26644  stirlinglem12  27937  stirlingr  27942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-rp 10371
  Copyright terms: Public domain W3C validator