Theorem elrpii 13025

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

This proof depends on syntax axioms:   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105  0cc0 11106   < clt 11249  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-rp 13023

This theorem is used by:  1rp  13026  2rp  13027  3rp  13028  5rp  13029  iexpcyc  14250  discr  14283  epr  16270  aaliou3lem1  26516  aaliou3lem2  26517  aaliou3lem3  26518  pirp  26637  pigt3  26694  efif1olem2  26719  cxpsqrtlem  26878  log2cnv  27120  chtublem  27386  chtub  27387  bposlem6  27464  lgsdir2lem1  27500  lgsdir2lem4  27503  lgsdir2lem5  27504  2sqlem11  27604  chebbnd1lem3  27646  chebbnd1  27647  pntlemg  27773  pntlemr  27777  pntlemf  27780  minvecolem3  31239  dp2lt10  33214  ballotlem2  34888  cntotbnd  38475  heiborlem5  38494  heiborlem7  38496  4rp  43089  6rp  43090  7rp  43091  8rp  43092  9rp  43093  isosctrlem1ALT  45670  sineq0ALT  45673  limclner  46393  stoweidlem5  46747  stoweidlem28  46770  stoweidlem59  46801  stoweid  46805  stirlinglem12  46827  fourierswlem  46972  fouriersw  46973  goldrarp  47649