Theorem elrpii 12940

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

Syntax hints:   ∈ wcel 2121   class class class wbr 5075  ℝcr 11032  0cc0 11033   < clt 11174  ℝ⁺crp 12937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-rp 12938

This theorem is referenced by:  1rp  12941  2rp  12942  3rp  12943  5rp  12944  iexpcyc  14164  discr  14197  epr  16170  aaliou3lem1  26330  aaliou3lem2  26331  aaliou3lem3  26332  pirp  26447  pigt3  26504  efif1olem2  26529  cxpsqrtlem  26688  log2cnv  26930  chtublem  27196  chtub  27197  bposlem6  27274  lgsdir2lem1  27310  lgsdir2lem4  27313  lgsdir2lem5  27314  2sqlem11  27414  chebbnd1lem3  27456  chebbnd1  27457  pntlemg  27583  pntlemr  27587  pntlemf  27590  minvecolem3  30969  dp2lt10  32966  ballotlem2  34685  cntotbnd  38178  heiborlem5  38197  heiborlem7  38199  4rp  42792  6rp  42793  7rp  42794  8rp  42795  9rp  42796  isosctrlem1ALT  45392  sineq0ALT  45395  limclner  46108  stoweidlem5  46462  stoweidlem28  46485  stoweidlem59  46516  stoweid  46520  stirlinglem12  46542  fourierswlem  46687  fouriersw  46688  goldrarp  47361