Theorem elrpii 13009

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

Syntax hints:   ∈ wcel 2099   class class class wbr 5148  ℝcr 11137  0cc0 11138   < clt 11278  ℝ⁺crp 13006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-rp 13007

This theorem is referenced by:  1rp  13010  2rp  13011  3rp  13012  iexpcyc  14202  discr  14234  epr  16184  aaliou3lem1  26276  aaliou3lem2  26277  aaliou3lem3  26278  pirp  26395  pigt3  26451  efif1olem2  26476  cxpsqrtlem  26635  log2cnv  26875  chtublem  27143  chtub  27144  bposlem6  27221  lgsdir2lem1  27257  lgsdir2lem4  27260  lgsdir2lem5  27261  2sqlem11  27361  chebbnd1lem3  27403  chebbnd1  27404  pntlemg  27530  pntlemr  27534  pntlemf  27537  minvecolem3  30685  dp2lt10  32607  ballotlem2  34108  cntotbnd  37269  heiborlem5  37288  heiborlem7  37290  isosctrlem1ALT  44373  sineq0ALT  44376  limclner  45039  stoweidlem5  45393  stoweidlem28  45416  stoweidlem59  45447  stoweid  45451  stirlinglem12  45473  fourierswlem  45618  fouriersw  45619