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

Theorem elrpii 10357
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 10356 . 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 1684   class class class wbr 4023   RRcr 8736   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  1rp  10358  2rp  10359  iexpcyc  11207  discr  11238  sqrlem7  11734  caurcvgr  12146  epr  12486  aaliou3lem1  19722  aaliou3lem2  19723  aaliou3lem3  19724  pige3  19885  sineq0  19889  cosordlem  19893  tanord1  19899  tanregt0  19901  efif1olem2  19905  argregt0  19964  argrege0  19965  logimul  19968  efopn  20005  cxpsqrlem  20049  isosctrlem1  20118  asinsin  20188  asin1  20190  reasinsin  20192  atanbnd  20222  atan1  20224  log2cnv  20240  basellem1  20318  basellem4  20321  cht3  20411  chtublem  20450  chtub  20451  bposlem6  20528  lgsdir2lem1  20562  lgsdir2lem4  20565  lgsdir2lem5  20566  2sqlem11  20614  chebbnd1lem3  20620  chebbnd1  20621  chto1ub  20625  dchrvmasumiflem1  20650  pntlemg  20747  pntlemr  20751  pntlemf  20754  minvecolem3  21455  ballotlem2  23047  circum  24007  cntotbnd  26520  heiborlem5  26539  heiborlem7  26541  stirlinglem12  27834  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-rp 10355
  Copyright terms: Public domain W3C validator