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

Theorem elrpii 11219
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 11218 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3mpbir2an 918 1  |-  A  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   class class class wbr 4447   RRcr 9487   0cc0 9488    < clt 9624   RR+crp 11216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-rp 11217
This theorem is referenced by:  1rp  11220  2rp  11221  iexpcyc  12236  discr  12267  sqrlem7  13041  caurcvgr  13455  epr  13798  aaliou3lem1  22472  aaliou3lem2  22473  aaliou3lem3  22474  pige3  22643  sineq0  22647  cosordlem  22651  tanord1  22657  tanregt0  22659  efif1olem2  22663  argregt0  22723  argrege0  22724  logimul  22727  efopn  22767  cxpsqrtlem  22811  isosctrlem1  22880  asinsin  22951  asin1  22953  reasinsin  22955  atanbnd  22985  atan1  22987  log2cnv  23003  basellem1  23082  basellem4  23085  cht3  23175  chtublem  23214  chtub  23215  bposlem6  23292  lgsdir2lem1  23326  lgsdir2lem4  23329  lgsdir2lem5  23330  2sqlem11  23378  chebbnd1lem3  23384  chebbnd1  23385  chto1ub  23389  dchrvmasumiflem1  23414  pntlemg  23511  pntlemr  23515  pntlemf  23518  minvecolem3  25468  ballotlem2  28067  circum  28515  dvtanlem  29641  cntotbnd  29895  heiborlem5  29914  heiborlem7  29916  3rp  31048  stoweidlem5  31305  stoweidlem28  31328  stoweidlem59  31359  stoweid  31363  wallispilem3  31367  stirlinglem12  31385  stirlingr  31390  dirker2re  31392  dirkerdenne0  31393  dirkerval2  31394  dirkercncflem1  31403  dirkercncflem4  31406  fourierdlem77  31484  fourierswlem  31531  fouriersw  31532  isosctrlem1ALT  32814  sineq0ALT  32817
  Copyright terms: Public domain W3C validator