Theorem elrpii 12945

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037  0cc0 11038   < clt 11179  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-rp 12943

This theorem is referenced by:  1rp  12946  2rp  12947  3rp  12948  5rp  12949  iexpcyc  14169  discr  14202  epr  16175  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem3  26310  pirp  26425  pigt3  26482  efif1olem2  26507  cxpsqrtlem  26666  log2cnv  26908  chtublem  27174  chtub  27175  bposlem6  27252  lgsdir2lem1  27288  lgsdir2lem4  27291  lgsdir2lem5  27292  2sqlem11  27392  chebbnd1lem3  27434  chebbnd1  27435  pntlemg  27561  pntlemr  27565  pntlemf  27568  minvecolem3  30947  dp2lt10  32943  ballotlem2  34633  cntotbnd  38117  heiborlem5  38136  heiborlem7  38138  4rp  42732  6rp  42733  7rp  42734  8rp  42735  9rp  42736  isosctrlem1ALT  45360  sineq0ALT  45363  limclner  46079  stoweidlem5  46433  stoweidlem28  46456  stoweidlem59  46487  stoweid  46491  stirlinglem12  46513  fourierswlem  46658  fouriersw  46659  goldrarp  47332