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

Theorem elrpii 10986
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 10985 . 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 1756   class class class wbr 4287   RRcr 9273   0cc0 9274    < clt 9410   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-rp 10984
This theorem is referenced by:  1rp  10987  2rp  10988  iexpcyc  11962  discr  11993  sqrlem7  12730  caurcvgr  13143  epr  13482  aaliou3lem1  21783  aaliou3lem2  21784  aaliou3lem3  21785  pige3  21954  sineq0  21958  cosordlem  21962  tanord1  21968  tanregt0  21970  efif1olem2  21974  argregt0  22034  argrege0  22035  logimul  22038  efopn  22078  cxpsqrlem  22122  isosctrlem1  22191  asinsin  22262  asin1  22264  reasinsin  22266  atanbnd  22296  atan1  22298  log2cnv  22314  basellem1  22393  basellem4  22396  cht3  22486  chtublem  22525  chtub  22526  bposlem6  22603  lgsdir2lem1  22637  lgsdir2lem4  22640  lgsdir2lem5  22641  2sqlem11  22689  chebbnd1lem3  22695  chebbnd1  22696  chto1ub  22700  dchrvmasumiflem1  22725  pntlemg  22822  pntlemr  22826  pntlemf  22829  minvecolem3  24228  ballotlem2  26823  circum  27270  dvtanlem  28394  cntotbnd  28648  heiborlem5  28667  heiborlem7  28669  stoweidlem5  29753  stoweidlem28  29776  stoweidlem59  29807  stoweid  29811  wallispilem3  29815  stirlinglem12  29833  stirlingr  29838  isosctrlem1ALT  31557  sineq0ALT  31560
  Copyright terms: Public domain W3C validator