Theorem elrpii 13011

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

Syntax hints:   ∈ wcel 2108   class class class wbr 5119  ℝcr 11128  0cc0 11129   < clt 11269  ℝ⁺crp 13008

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-rp 13009

This theorem is referenced by:  1rp  13012  2rp  13013  3rp  13014  5rp  13015  iexpcyc  14225  discr  14258  epr  16226  aaliou3lem1  26302  aaliou3lem2  26303  aaliou3lem3  26304  pirp  26422  pigt3  26479  efif1olem2  26504  cxpsqrtlem  26663  log2cnv  26906  chtublem  27174  chtub  27175  bposlem6  27252  lgsdir2lem1  27288  lgsdir2lem4  27291  lgsdir2lem5  27292  2sqlem11  27392  chebbnd1lem3  27434  chebbnd1  27435  pntlemg  27561  pntlemr  27565  pntlemf  27568  minvecolem3  30857  dp2lt10  32858  ballotlem2  34521  cntotbnd  37820  heiborlem5  37839  heiborlem7  37841  4rp  42349  6rp  42350  7rp  42351  8rp  42352  9rp  42353  isosctrlem1ALT  44958  sineq0ALT  44961  limclner  45680  stoweidlem5  46034  stoweidlem28  46057  stoweidlem59  46088  stoweid  46092  stirlinglem12  46114  fourierswlem  46259  fouriersw  46260