Theorem elrpii 12488

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5040  ℝcr 10627  0cc0 10628   < clt 10766  ℝ⁺crp 12485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402  df-un 3858  df-sn 4527  df-pr 4529  df-op 4533  df-br 5041  df-rp 12486

This theorem is referenced by:  1rp  12489  2rp  12490  3rp  12491  iexpcyc  13674  discr  13706  epr  15666  aaliou3lem1  25103  aaliou3lem2  25104  aaliou3lem3  25105  pirp  25219  pigt3  25275  efif1olem2  25300  cxpsqrtlem  25458  log2cnv  25695  chtublem  25960  chtub  25961  bposlem6  26038  lgsdir2lem1  26074  lgsdir2lem4  26077  lgsdir2lem5  26078  2sqlem11  26178  chebbnd1lem3  26220  chebbnd1  26221  pntlemg  26347  pntlemr  26351  pntlemf  26354  minvecolem3  28824  dp2lt10  30746  ballotlem2  32038  cntotbnd  35610  heiborlem5  35629  heiborlem7  35631  isosctrlem1ALT  42133  sineq0ALT  42136  limclner  42775  stoweidlem5  43129  stoweidlem28  43152  stoweidlem59  43183  stoweid  43187  stirlinglem12  43209  fourierswlem  43354  fouriersw  43355