Theorem elrpii 12922

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5100  ℝcr 11039  0cc0 11040   < clt 11180  ℝ⁺crp 12919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12920

This theorem is referenced by:  1rp  12923  2rp  12924  3rp  12925  5rp  12926  iexpcyc  14144  discr  14177  epr  16147  aaliou3lem1  26323  aaliou3lem2  26324  aaliou3lem3  26325  pirp  26443  pigt3  26500  efif1olem2  26525  cxpsqrtlem  26684  log2cnv  26927  chtublem  27195  chtub  27196  bposlem6  27273  lgsdir2lem1  27309  lgsdir2lem4  27312  lgsdir2lem5  27313  2sqlem11  27413  chebbnd1lem3  27455  chebbnd1  27456  pntlemg  27582  pntlemr  27586  pntlemf  27589  minvecolem3  30970  dp2lt10  32982  ballotlem2  34673  cntotbnd  38076  heiborlem5  38095  heiborlem7  38097  4rp  42699  6rp  42700  7rp  42701  8rp  42702  9rp  42703  isosctrlem1ALT  45318  sineq0ALT  45321  limclner  46038  stoweidlem5  46392  stoweidlem28  46415  stoweidlem59  46446  stoweid  46450  stirlinglem12  46472  fourierswlem  46617  fouriersw  46618