Theorem elrpii 12910

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5097  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12907

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-rp 12908

This theorem is referenced by:  1rp  12911  2rp  12912  3rp  12913  5rp  12914  iexpcyc  14132  discr  14165  epr  16135  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem3  26310  pirp  26428  pigt3  26485  efif1olem2  26510  cxpsqrtlem  26669  log2cnv  26912  chtublem  27180  chtub  27181  bposlem6  27258  lgsdir2lem1  27294  lgsdir2lem4  27297  lgsdir2lem5  27298  2sqlem11  27398  chebbnd1lem3  27440  chebbnd1  27441  pntlemg  27567  pntlemr  27571  pntlemf  27574  minvecolem3  30932  dp2lt10  32944  ballotlem2  34625  cntotbnd  37966  heiborlem5  37985  heiborlem7  37987  4rp  42592  6rp  42593  7rp  42594  8rp  42595  9rp  42596  isosctrlem1ALT  45211  sineq0ALT  45214  limclner  45932  stoweidlem5  46286  stoweidlem28  46309  stoweidlem59  46340  stoweid  46344  stirlinglem12  46366  fourierswlem  46511  fouriersw  46512