Theorem elrpii 13035

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

Syntax hints:   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152  0cc0 11153   < clt 11293  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-rp 13033

This theorem is referenced by:  1rp  13036  2rp  13037  3rp  13038  5rp  13039  iexpcyc  14243  discr  14276  epr  16241  aaliou3lem1  26399  aaliou3lem2  26400  aaliou3lem3  26401  pirp  26518  pigt3  26575  efif1olem2  26600  cxpsqrtlem  26759  log2cnv  27002  chtublem  27270  chtub  27271  bposlem6  27348  lgsdir2lem1  27384  lgsdir2lem4  27387  lgsdir2lem5  27388  2sqlem11  27488  chebbnd1lem3  27530  chebbnd1  27531  pntlemg  27657  pntlemr  27661  pntlemf  27664  minvecolem3  30905  dp2lt10  32851  ballotlem2  34470  cntotbnd  37783  heiborlem5  37802  heiborlem7  37804  4rp  42313  6rp  42314  7rp  42315  8rp  42316  9rp  42317  isosctrlem1ALT  44932  sineq0ALT  44935  limclner  45607  stoweidlem5  45961  stoweidlem28  45984  stoweidlem59  46015  stoweid  46019  stirlinglem12  46041  fourierswlem  46186  fouriersw  46187