Theorem elrpii 12998

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

Syntax hints:   ∈ wcel 2144   class class class wbr 5102  ℝcr 11074  0cc0 11075   < clt 11218  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-rp 12996

This theorem is referenced by:  1rp  12999  2rp  13000  3rp  13001  5rp  13002  iexpcyc  14222  discr  14255  epr  16242  aaliou3lem1  26408  aaliou3lem2  26409  aaliou3lem3  26410  pirp  26528  pigt3  26585  efif1olem2  26610  cxpsqrtlem  26769  log2cnv  27011  chtublem  27277  chtub  27278  bposlem6  27355  lgsdir2lem1  27391  lgsdir2lem4  27394  lgsdir2lem5  27395  2sqlem11  27495  chebbnd1lem3  27537  chebbnd1  27538  pntlemg  27664  pntlemr  27668  pntlemf  27671  minvecolem3  31081  dp2lt10  33063  ballotlem2  34788  cntotbnd  38300  heiborlem5  38319  heiborlem7  38321  4rp  42914  6rp  42915  7rp  42916  8rp  42917  9rp  42918  isosctrlem1ALT  45514  sineq0ALT  45517  limclner  46230  stoweidlem5  46584  stoweidlem28  46607  stoweidlem59  46638  stoweid  46642  stirlinglem12  46664  fourierswlem  46809  fouriersw  46810  goldrarp  47483