Theorem elrpii 12380

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

Syntax hints:   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  1rp  12381  2rp  12382  3rp  12383  iexpcyc  13565  discr  13597  epr  15553  aaliou3lem1  24938  aaliou3lem2  24939  aaliou3lem3  24940  pirp  25054  pigt3  25110  efif1olem2  25135  cxpsqrtlem  25293  log2cnv  25530  chtublem  25795  chtub  25796  bposlem6  25873  lgsdir2lem1  25909  lgsdir2lem4  25912  lgsdir2lem5  25913  2sqlem11  26013  chebbnd1lem3  26055  chebbnd1  26056  pntlemg  26182  pntlemr  26186  pntlemf  26189  minvecolem3  28659  dp2lt10  30586  ballotlem2  31856  cntotbnd  35234  heiborlem5  35253  heiborlem7  35255  isosctrlem1ALT  41640  sineq0ALT  41643  limclner  42293  stoweidlem5  42647  stoweidlem28  42670  stoweidlem59  42701  stoweid  42705  stirlinglem12  42727  fourierswlem  42872  fouriersw  42873