Theorem elrpii 12733

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 12732	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	mpbir2an 708	1 ⊢ 𝐴 ∈ ℝ+

Syntax hints:   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870  0cc0 10871   < clt 11009  ℝ⁺crp 12730

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-rp 12731

This theorem is referenced by:  1rp  12734  2rp  12735  3rp  12736  iexpcyc  13923  discr  13955  epr  15917  aaliou3lem1  25502  aaliou3lem2  25503  aaliou3lem3  25504  pirp  25618  pigt3  25674  efif1olem2  25699  cxpsqrtlem  25857  log2cnv  26094  chtublem  26359  chtub  26360  bposlem6  26437  lgsdir2lem1  26473  lgsdir2lem4  26476  lgsdir2lem5  26477  2sqlem11  26577  chebbnd1lem3  26619  chebbnd1  26620  pntlemg  26746  pntlemr  26750  pntlemf  26753  minvecolem3  29238  dp2lt10  31158  ballotlem2  32455  cntotbnd  35954  heiborlem5  35973  heiborlem7  35975  isosctrlem1ALT  42554  sineq0ALT  42557  limclner  43192  stoweidlem5  43546  stoweidlem28  43569  stoweidlem59  43600  stoweid  43604  stirlinglem12  43626  fourierswlem  43771  fouriersw  43772