Theorem elrpii 13060

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

Syntax hints:   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  0cc0 11184   < clt 11324  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-rp 13058

This theorem is referenced by:  1rp  13061  2rp  13062  3rp  13063  iexpcyc  14256  discr  14289  epr  16256  aaliou3lem1  26402  aaliou3lem2  26403  aaliou3lem3  26404  pirp  26521  pigt3  26578  efif1olem2  26603  cxpsqrtlem  26762  log2cnv  27005  chtublem  27273  chtub  27274  bposlem6  27351  lgsdir2lem1  27387  lgsdir2lem4  27390  lgsdir2lem5  27391  2sqlem11  27491  chebbnd1lem3  27533  chebbnd1  27534  pntlemg  27660  pntlemr  27664  pntlemf  27667  minvecolem3  30908  dp2lt10  32848  ballotlem2  34453  cntotbnd  37756  heiborlem5  37775  heiborlem7  37777  4rp  42287  5rp  42288  6rp  42289  7rp  42290  8rp  42291  9rp  42292  isosctrlem1ALT  44905  sineq0ALT  44908  limclner  45572  stoweidlem5  45926  stoweidlem28  45949  stoweidlem59  45980  stoweid  45984  stirlinglem12  46006  fourierswlem  46151  fouriersw  46152