Theorem elrpii 11711

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

Syntax hints:   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  1rp  11712  2rp  11713  3rp  11714  iexpcyc  12831  discr  12863  sqrlem7  13837  caurcvgr  14252  epr  14775  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem3  23903  pirp  24017  pige3  24073  cosordlem  24081  efif1olem2  24093  cxpsqrtlem  24248  log2cnv  24471  cht3  24699  chtublem  24736  chtub  24737  bposlem6  24814  lgsdir2lem1  24850  lgsdir2lem4  24853  lgsdir2lem5  24854  2sqlem11  24954  chebbnd1lem3  24960  chebbnd1  24961  chto1ub  24965  dchrvmasumiflem1  24990  pntlemg  25087  pntlemr  25091  pntlemf  25094  minvecolem3  27116  ballotlem2  29877  pigt3  32572  cntotbnd  32765  heiborlem5  32784  heiborlem7  32786  isosctrlem1ALT  38192  sineq0ALT  38195  limclner  38718  stoweidlem5  38898  stoweidlem28  38921  stoweidlem59  38952  stoweid  38956  stirlinglem12  38978  fourierswlem  39123  fouriersw  39124