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

Theorem elrpii 11160
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 11159 . 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 1836   class class class wbr 4380   RRcr 9420   0cc0 9421    < clt 9557   RR+crp 11157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-br 4381  df-rp 11158
This theorem is referenced by:  1rp  11161  2rp  11162  iexpcyc  12194  discr  12224  sqrlem7  13103  caurcvgr  13517  epr  13962  aaliou3lem1  22842  aaliou3lem2  22843  aaliou3lem3  22844  pirp  22958  pige3  23014  cosordlem  23022  efif1olem2  23034  cxpsqrtlem  23189  log2cnv  23410  cht3  23583  chtublem  23622  chtub  23623  bposlem6  23700  lgsdir2lem1  23734  lgsdir2lem4  23737  lgsdir2lem5  23738  2sqlem11  23786  chebbnd1lem3  23792  chebbnd1  23793  chto1ub  23797  dchrvmasumiflem1  23822  pntlemg  23919  pntlemr  23923  pntlemf  23926  minvecolem3  25930  ballotlem2  28646  cntotbnd  30494  heiborlem5  30513  heiborlem7  30515  3rp  31673  limclner  31858  stoweidlem5  31988  stoweidlem28  32011  stoweidlem59  32042  stoweid  32046  stirlinglem12  32068  fourierswlem  32214  fouriersw  32215  isosctrlem1ALT  34116  sineq0ALT  34119
  Copyright terms: Public domain W3C validator