Theorem elrpii 13123

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

This proof depends on syntax axioms:   ∈ wcel 2144   class class class wbr 5102  ℝcr 11199  0cc0 11200   < clt 11343  ℝ⁺crp 13120

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13121

This theorem is used by:  1rp  13124  2rp  13125  3rp  13126  5rp  13127  iexpcyc  14351  discr  14384  epr  16376  aaliou3lem1  26669  aaliou3lem2  26670  aaliou3lem3  26671  pirp  26790  pigt3  26846  efif1olem2  26871  cxpsqrtlem  27030  log2cnv  27272  chtublem  27538  chtub  27539  bposlem6  27616  lgsdir2lem1  27652  lgsdir2lem4  27655  lgsdir2lem5  27656  2sqlem11  27756  chebbnd1lem3  27798  chebbnd1  27799  pntlemg  27925  pntlemr  27929  pntlemf  27932  minvecolem3  31478  dp2lt10  33450  ballotlem2  35121  cntotbnd  38731  heiborlem5  38750  heiborlem7  38752  4rp  43358  6rp  43359  7rp  43360  8rp  43361  9rp  43362  isosctrlem1ALT  45916  sineq0ALT  45919  limclner  46661  stoweidlem5  47015  stoweidlem28  47038  stoweidlem59  47069  stoweid  47073  stirlinglem12  47095  fourierswlem  47240  fouriersw  47241  goldrarp  47931