Theorem elrpii 13047

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13045

This theorem is used by:  1rp  13048  2rp  13049  3rp  13050  5rp  13051  iexpcyc  14273  discr  14306  epr  16300  aaliou3lem1  26575  aaliou3lem2  26576  aaliou3lem3  26577  pirp  26696  pigt3  26753  efif1olem2  26778  cxpsqrtlem  26937  log2cnv  27179  chtublem  27445  chtub  27446  bposlem6  27523  lgsdir2lem1  27559  lgsdir2lem4  27562  lgsdir2lem5  27563  2sqlem11  27663  chebbnd1lem3  27705  chebbnd1  27706  pntlemg  27832  pntlemr  27836  pntlemf  27839  minvecolem3  31343  dp2lt10  33316  ballotlem2  34987  cntotbnd  38533  heiborlem5  38552  heiborlem7  38554  4rp  43162  6rp  43163  7rp  43164  8rp  43165  9rp  43166  isosctrlem1ALT  45743  sineq0ALT  45746  limclner  46466  stoweidlem5  46820  stoweidlem28  46843  stoweidlem59  46874  stoweid  46878  stirlinglem12  46900  fourierswlem  47045  fouriersw  47046  goldrarp  47736