Theorem elrpii 12896

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  0cc0 11009   < clt 11149  ℝ⁺crp 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-rp 12894

This theorem is referenced by:  1rp  12897  2rp  12898  3rp  12899  5rp  12900  iexpcyc  14114  discr  14147  epr  16117  aaliou3lem1  26248  aaliou3lem2  26249  aaliou3lem3  26250  pirp  26368  pigt3  26425  efif1olem2  26450  cxpsqrtlem  26609  log2cnv  26852  chtublem  27120  chtub  27121  bposlem6  27198  lgsdir2lem1  27234  lgsdir2lem4  27237  lgsdir2lem5  27238  2sqlem11  27338  chebbnd1lem3  27380  chebbnd1  27381  pntlemg  27507  pntlemr  27511  pntlemf  27514  minvecolem3  30824  dp2lt10  32833  ballotlem2  34473  cntotbnd  37796  heiborlem5  37815  heiborlem7  37817  4rp  42293  6rp  42294  7rp  42295  8rp  42296  9rp  42297  isosctrlem1ALT  44927  sineq0ALT  44930  limclner  45652  stoweidlem5  46006  stoweidlem28  46029  stoweidlem59  46060  stoweid  46064  stirlinglem12  46086  fourierswlem  46231  fouriersw  46232