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

Theorem elrpii 11229
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 11228 . 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 1802   class class class wbr 4434   RRcr 9491   0cc0 9492    < clt 9628   RR+crp 11226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-rp 11227
This theorem is referenced by:  1rp  11230  2rp  11231  iexpcyc  12248  discr  12279  sqrlem7  13058  caurcvgr  13472  epr  13815  aaliou3lem1  22607  aaliou3lem2  22608  aaliou3lem3  22609  pirp  22723  pige3  22779  cosordlem  22787  efif1olem2  22799  cxpsqrtlem  22952  log2cnv  23144  cht3  23316  chtublem  23355  chtub  23356  bposlem6  23433  lgsdir2lem1  23467  lgsdir2lem4  23470  lgsdir2lem5  23471  2sqlem11  23519  chebbnd1lem3  23525  chebbnd1  23526  chto1ub  23530  dchrvmasumiflem1  23555  pntlemg  23652  pntlemr  23656  pntlemf  23659  minvecolem3  25661  ballotlem2  28297  cntotbnd  30264  heiborlem5  30283  heiborlem7  30285  3rp  31420  limclner  31565  stoweidlem5  31676  stoweidlem28  31699  stoweidlem59  31730  stoweid  31734  stirlinglem12  31756  fourierswlem  31902  fouriersw  31903  isosctrlem1ALT  33462  sineq0ALT  33465
  Copyright terms: Public domain W3C validator