Theorem elrpii 13019

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

Syntax hints:   ∈ wcel 2149   class class class wbr 5111  ℝcr 11099  0cc0 11100   < clt 11243  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-rp 13017

This theorem is referenced by:  1rp  13020  2rp  13021  3rp  13022  5rp  13023  iexpcyc  14243  discr  14276  epr  16264  aaliou3lem1  26472  aaliou3lem2  26473  aaliou3lem3  26474  pirp  26592  pigt3  26649  efif1olem2  26674  cxpsqrtlem  26833  log2cnv  27075  chtublem  27341  chtub  27342  bposlem6  27419  lgsdir2lem1  27455  lgsdir2lem4  27458  lgsdir2lem5  27459  2sqlem11  27559  chebbnd1lem3  27601  chebbnd1  27602  pntlemg  27728  pntlemr  27732  pntlemf  27735  minvecolem3  31169  dp2lt10  33144  ballotlem2  34824  cntotbnd  38370  heiborlem5  38389  heiborlem7  38391  4rp  42986  6rp  42987  7rp  42988  8rp  42989  9rp  42990  isosctrlem1ALT  45569  sineq0ALT  45572  limclner  46292  stoweidlem5  46646  stoweidlem28  46669  stoweidlem59  46700  stoweid  46704  stirlinglem12  46726  fourierswlem  46871  fouriersw  46872  goldrarp  47545