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

Theorem elrpii 10571
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 10570 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3mpbir2an 887 1  |-  A  e.  RR+
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   class class class wbr 4172   RRcr 8945   0cc0 8946    < clt 9076   RR+crp 10568
This theorem is referenced by:  1rp  10572  2rp  10573  iexpcyc  11440  discr  11471  sqrlem7  12009  caurcvgr  12422  epr  12762  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem3  20214  pige3  20378  sineq0  20382  cosordlem  20386  tanord1  20392  tanregt0  20394  efif1olem2  20398  argregt0  20458  argrege0  20459  logimul  20462  efopn  20502  cxpsqrlem  20546  isosctrlem1  20615  asinsin  20685  asin1  20687  reasinsin  20689  atanbnd  20719  atan1  20721  log2cnv  20737  basellem1  20816  basellem4  20819  cht3  20909  chtublem  20948  chtub  20949  bposlem6  21026  lgsdir2lem1  21060  lgsdir2lem4  21063  lgsdir2lem5  21064  2sqlem11  21112  chebbnd1lem3  21118  chebbnd1  21119  chto1ub  21123  dchrvmasumiflem1  21148  pntlemg  21245  pntlemr  21249  pntlemf  21252  minvecolem3  22331  ballotlem2  24699  circum  25064  cntotbnd  26395  heiborlem5  26414  heiborlem7  26416  stoweidlem5  27621  stoweidlem28  27644  stoweidlem59  27675  stoweid  27679  wallispilem3  27683  stirlinglem12  27701  stirlingr  27706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-rp 10569
  Copyright terms: Public domain W3C validator