Theorem elrpii 12954

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  1rp  12955  2rp  12956  3rp  12957  5rp  12958  iexpcyc  14172  discr  14205  epr  16176  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem3  26252  pirp  26370  pigt3  26427  efif1olem2  26452  cxpsqrtlem  26611  log2cnv  26854  chtublem  27122  chtub  27123  bposlem6  27200  lgsdir2lem1  27236  lgsdir2lem4  27239  lgsdir2lem5  27240  2sqlem11  27340  chebbnd1lem3  27382  chebbnd1  27383  pntlemg  27509  pntlemr  27513  pntlemf  27516  minvecolem3  30805  dp2lt10  32804  ballotlem2  34480  cntotbnd  37790  heiborlem5  37809  heiborlem7  37811  4rp  42288  6rp  42289  7rp  42290  8rp  42291  9rp  42292  isosctrlem1ALT  44923  sineq0ALT  44926  limclner  45649  stoweidlem5  46003  stoweidlem28  46026  stoweidlem59  46057  stoweid  46061  stirlinglem12  46083  fourierswlem  46228  fouriersw  46229