Theorem elrpii 12930

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043  0cc0 11044   < clt 11184  ℝ⁺crp 12927

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 12928

This theorem is referenced by:  1rp  12931  2rp  12932  3rp  12933  5rp  12934  iexpcyc  14148  discr  14181  epr  16152  aaliou3lem1  26283  aaliou3lem2  26284  aaliou3lem3  26285  pirp  26403  pigt3  26460  efif1olem2  26485  cxpsqrtlem  26644  log2cnv  26887  chtublem  27155  chtub  27156  bposlem6  27233  lgsdir2lem1  27269  lgsdir2lem4  27272  lgsdir2lem5  27273  2sqlem11  27373  chebbnd1lem3  27415  chebbnd1  27416  pntlemg  27542  pntlemr  27546  pntlemf  27549  minvecolem3  30855  dp2lt10  32854  ballotlem2  34473  cntotbnd  37783  heiborlem5  37802  heiborlem7  37804  4rp  42281  6rp  42282  7rp  42283  8rp  42284  9rp  42285  isosctrlem1ALT  44916  sineq0ALT  44919  limclner  45642  stoweidlem5  45996  stoweidlem28  46019  stoweidlem59  46050  stoweid  46054  stirlinglem12  46076  fourierswlem  46221  fouriersw  46222