Theorem elrpii 13037

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

Syntax hints:   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  0cc0 11155   < clt 11295  ℝ⁺crp 13034

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-rp 13035

This theorem is referenced by:  1rp  13038  2rp  13039  3rp  13040  5rp  13041  iexpcyc  14246  discr  14279  epr  16244  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem3  26386  pirp  26503  pigt3  26560  efif1olem2  26585  cxpsqrtlem  26744  log2cnv  26987  chtublem  27255  chtub  27256  bposlem6  27333  lgsdir2lem1  27369  lgsdir2lem4  27372  lgsdir2lem5  27373  2sqlem11  27473  chebbnd1lem3  27515  chebbnd1  27516  pntlemg  27642  pntlemr  27646  pntlemf  27649  minvecolem3  30895  dp2lt10  32866  ballotlem2  34491  cntotbnd  37803  heiborlem5  37822  heiborlem7  37824  4rp  42334  6rp  42335  7rp  42336  8rp  42337  9rp  42338  isosctrlem1ALT  44954  sineq0ALT  44957  limclner  45666  stoweidlem5  46020  stoweidlem28  46043  stoweidlem59  46074  stoweid  46078  stirlinglem12  46100  fourierswlem  46245  fouriersw  46246