Theorem elrpii 13092

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5102  ℝcr 11170  0cc0 11171   < clt 11314  ℝ⁺crp 13089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13090

This theorem is used by:  1rp  13093  2rp  13094  3rp  13095  5rp  13096  iexpcyc  14318  discr  14351  epr  16343  aaliou3lem1  26632  aaliou3lem2  26633  aaliou3lem3  26634  pirp  26753  pigt3  26809  efif1olem2  26834  cxpsqrtlem  26993  log2cnv  27235  chtublem  27501  chtub  27502  bposlem6  27579  lgsdir2lem1  27615  lgsdir2lem4  27618  lgsdir2lem5  27619  2sqlem11  27719  chebbnd1lem3  27761  chebbnd1  27762  pntlemg  27888  pntlemr  27892  pntlemf  27895  minvecolem3  31411  dp2lt10  33383  ballotlem2  35055  cntotbnd  38650  heiborlem5  38669  heiborlem7  38671  4rp  43279  6rp  43280  7rp  43281  8rp  43282  9rp  43283  isosctrlem1ALT  45860  sineq0ALT  45863  limclner  46583  stoweidlem5  46937  stoweidlem28  46960  stoweidlem59  46991  stoweid  46995  stirlinglem12  47017  fourierswlem  47162  fouriersw  47163  goldrarp  47853