Theorem elrpii 12073

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

Syntax hints:   ∈ wcel 2157   class class class wbr 4841  ℝcr 10221  0cc0 10222   < clt 10361  ℝ⁺crp 12070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-rp 12071

This theorem is referenced by:  1rp  12074  2rp  12075  3rp  12076  iexpcyc  13219  discr  13251  caurcvgr  14742  epr  15269  aaliou3lem1  24435  aaliou3lem2  24436  aaliou3lem3  24437  pirp  24552  pige3  24608  cosordlem  24616  efif1olem2  24628  cxpsqrtlem  24786  log2cnv  25020  cht3  25248  chtublem  25285  chtub  25286  bposlem6  25363  lgsdir2lem1  25399  lgsdir2lem4  25402  lgsdir2lem5  25403  2sqlem11  25503  chebbnd1lem3  25509  chebbnd1  25510  chto1ub  25514  dchrvmasumiflem1  25539  pntlemg  25636  pntlemr  25640  pntlemf  25643  minvecolem3  28249  dp2lt10  30100  ballotlem2  31059  pigt3  33883  cntotbnd  34074  heiborlem5  34093  heiborlem7  34095  isosctrlem1ALT  39918  sineq0ALT  39921  limclner  40615  stoweidlem5  40953  stoweidlem28  40976  stoweidlem59  41007  stoweid  41011  stirlinglem12  41033  fourierswlem  41178  fouriersw  41179