Theorem elrpii 12932

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5102  ℝcr 11045  0cc0 11046   < clt 11186  ℝ⁺crp 12929

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-rp 12930

This theorem is referenced by:  1rp  12933  2rp  12934  3rp  12935  5rp  12936  iexpcyc  14150  discr  14183  epr  16153  aaliou3lem1  26284  aaliou3lem2  26285  aaliou3lem3  26286  pirp  26404  pigt3  26461  efif1olem2  26486  cxpsqrtlem  26645  log2cnv  26888  chtublem  27156  chtub  27157  bposlem6  27234  lgsdir2lem1  27270  lgsdir2lem4  27273  lgsdir2lem5  27274  2sqlem11  27374  chebbnd1lem3  27416  chebbnd1  27417  pntlemg  27543  pntlemr  27547  pntlemf  27550  minvecolem3  30856  dp2lt10  32855  ballotlem2  34474  cntotbnd  37784  heiborlem5  37803  heiborlem7  37805  4rp  42282  6rp  42283  7rp  42284  8rp  42285  9rp  42286  isosctrlem1ALT  44917  sineq0ALT  44920  limclner  45643  stoweidlem5  45997  stoweidlem28  46020  stoweidlem59  46051  stoweid  46055  stirlinglem12  46077  fourierswlem  46222  fouriersw  46223