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

Theorem elrpii 11795
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 11794 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3mpbir2an 954 1 𝐴 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 1987   class class class wbr 4623  cr 9895  0cc0 9896   < clt 10034  +crp 11792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-rp 11793
This theorem is referenced by:  1rp  11796  2rp  11797  3rp  11798  iexpcyc  12925  discr  12957  sqrlem7  13939  caurcvgr  14354  epr  14880  aaliou3lem1  24035  aaliou3lem2  24036  aaliou3lem3  24037  pirp  24151  pige3  24207  cosordlem  24215  efif1olem2  24227  cxpsqrtlem  24382  log2cnv  24605  cht3  24833  chtublem  24870  chtub  24871  bposlem6  24948  lgsdir2lem1  24984  lgsdir2lem4  24987  lgsdir2lem5  24988  2sqlem11  25088  chebbnd1lem3  25094  chebbnd1  25095  chto1ub  25099  dchrvmasumiflem1  25124  pntlemg  25221  pntlemr  25225  pntlemf  25228  minvecolem3  27620  ballotlem2  30373  pigt3  33073  cntotbnd  33266  heiborlem5  33285  heiborlem7  33287  isosctrlem1ALT  38692  sineq0ALT  38695  limclner  39319  stoweidlem5  39559  stoweidlem28  39582  stoweidlem59  39613  stoweid  39617  stirlinglem12  39639  fourierswlem  39784  fouriersw  39785
  Copyright terms: Public domain W3C validator