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

Theorem elrpii 12923
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 12922 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3mpbir2an 710 1 𝐴 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2107   class class class wbr 5106  cr 11055  0cc0 11056   < clt 11194  +crp 12920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-rp 12921
This theorem is referenced by:  1rp  12924  2rp  12925  3rp  12926  iexpcyc  14117  discr  14149  epr  16095  aaliou3lem1  25718  aaliou3lem2  25719  aaliou3lem3  25720  pirp  25834  pigt3  25890  efif1olem2  25915  cxpsqrtlem  26073  log2cnv  26310  chtublem  26575  chtub  26576  bposlem6  26653  lgsdir2lem1  26689  lgsdir2lem4  26692  lgsdir2lem5  26693  2sqlem11  26793  chebbnd1lem3  26835  chebbnd1  26836  pntlemg  26962  pntlemr  26966  pntlemf  26969  minvecolem3  29860  dp2lt10  31789  ballotlem2  33145  cntotbnd  36301  heiborlem5  36320  heiborlem7  36322  isosctrlem1ALT  43304  sineq0ALT  43307  limclner  43978  stoweidlem5  44332  stoweidlem28  44355  stoweidlem59  44386  stoweid  44390  stirlinglem12  44412  fourierswlem  44557  fouriersw  44558
  Copyright terms: Public domain W3C validator