Theorem elrpii 12977

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

Step	Hyp	Ref	Expression
1		elrpi.1	. 2 ⊢ 𝐴 ∈ ℝ
2		elrpi.2	. 2 ⊢ 0 < 𝐴
3		elrp 12976	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	mpbir2an 710	1 ⊢ 𝐴 ∈ ℝ+

Syntax hints:   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

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 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  1rp  12978  2rp  12979  3rp  12980  iexpcyc  14171  discr  14203  epr  16151  aaliou3lem1  25855  aaliou3lem2  25856  aaliou3lem3  25857  pirp  25971  pigt3  26027  efif1olem2  26052  cxpsqrtlem  26210  log2cnv  26449  chtublem  26714  chtub  26715  bposlem6  26792  lgsdir2lem1  26828  lgsdir2lem4  26831  lgsdir2lem5  26832  2sqlem11  26932  chebbnd1lem3  26974  chebbnd1  26975  pntlemg  27101  pntlemr  27105  pntlemf  27108  minvecolem3  30160  dp2lt10  32081  ballotlem2  33518  cntotbnd  36712  heiborlem5  36731  heiborlem7  36733  isosctrlem1ALT  43743  sineq0ALT  43746  limclner  44415  stoweidlem5  44769  stoweidlem28  44792  stoweidlem59  44823  stoweid  44827  stirlinglem12  44849  fourierswlem  44994  fouriersw  44995