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

Theorem elrpii 12380
Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
Hypotheses
Ref Expression
elrpi.1 𝐴 ∈ ℝ
elrpi.2 0 < 𝐴
Assertion
Ref Expression
elrpii 𝐴 ∈ ℝ+

Proof of Theorem elrpii
StepHypRef Expression
1 elrpi.1 . 2 𝐴 ∈ ℝ
2 elrpi.2 . 2 0 < 𝐴
3 elrp 12379 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3mpbir2an 707 1 𝐴 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2105   class class class wbr 5057  cr 10524  0cc0 10525   < clt 10663  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-rp 12378
This theorem is referenced by:  1rp  12381  2rp  12382  3rp  12383  iexpcyc  13557  discr  13589  epr  15549  aaliou3lem1  24858  aaliou3lem2  24859  aaliou3lem3  24860  pirp  24974  pigt3  25030  efif1olem2  25054  cxpsqrtlem  25212  log2cnv  25449  chtublem  25714  chtub  25715  bposlem6  25792  lgsdir2lem1  25828  lgsdir2lem4  25831  lgsdir2lem5  25832  2sqlem11  25932  chebbnd1lem3  25974  chebbnd1  25975  pntlemg  26101  pntlemr  26105  pntlemf  26108  minvecolem3  28580  dp2lt10  30487  ballotlem2  31645  cntotbnd  34955  heiborlem5  34974  heiborlem7  34976  isosctrlem1ALT  41145  sineq0ALT  41148  limclner  41808  stoweidlem5  42167  stoweidlem28  42190  stoweidlem59  42221  stoweid  42225  stirlinglem12  42247  fourierswlem  42392  fouriersw  42393
  Copyright terms: Public domain W3C validator