Theorem elrpd 9850

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
elrpd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
elrpd.2	⊢ (𝜑 → 0 < 𝐴)

Assertion

Ref	Expression
elrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem elrpd

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		elrpd.2	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		elrp 9812	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2178   class class class wbr 4059  ℝcr 7959  0cc0 7960   < clt 8142  ℝ⁺crp 9810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060  df-rp 9811

This theorem is referenced by:  mul2lt0rgt0  9917  mul2lt0np  9920  zltaddlt1le  10164  modqval  10506  ltexp2a  10773  leexp2a  10774  expnlbnd2  10847  nn0ltexp2  10891  resqrexlem1arp  11431  resqrexlemp1rp  11432  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemgt0  11446  resqrexlemglsq  11448  rpsqrtcl  11467  absrpclap  11487  rpmaxcl  11649  rpmincl  11664  xrminrpcl  11700  xrbdtri  11702  mulcn2  11738  reccn2ap  11739  climge0  11751  divcnv  11923  georeclim  11939  cvgratnnlembern  11949  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  rpefcl  12111  efltim  12124  ef01bndlem  12182  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  bdmopn  15091  mulcncflem  15194  ivthinclemlopn  15223  ivthinclemuopn  15225  dveflem  15313  reeff1olem  15358  pilem3  15370  tanrpcl  15424  cosordlem  15436  rplogcl  15466  logdivlti  15468  cxplt  15503  cxple  15504  rpabscxpbnd  15527  ltexp2  15528  iooref1o  16175