Theorem elrpd 9901

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 9863	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4083  ℝcr 8009  0cc0 8010   < clt 8192  ℝ⁺crp 9861

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-rp 9862

This theorem is referenced by:  mul2lt0rgt0  9968  mul2lt0np  9971  zltaddlt1le  10215  modqval  10558  ltexp2a  10825  leexp2a  10826  expnlbnd2  10899  nn0ltexp2  10943  resqrexlem1arp  11531  resqrexlemp1rp  11532  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemgt0  11546  resqrexlemglsq  11548  rpsqrtcl  11567  absrpclap  11587  rpmaxcl  11749  rpmincl  11764  xrminrpcl  11800  xrbdtri  11802  mulcn2  11838  reccn2ap  11839  climge0  11851  divcnv  12023  georeclim  12039  cvgratnnlembern  12049  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  rpefcl  12211  efltim  12224  ef01bndlem  12282  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  bdmopn  15193  mulcncflem  15296  ivthinclemlopn  15325  ivthinclemuopn  15327  dveflem  15415  reeff1olem  15460  pilem3  15472  tanrpcl  15526  cosordlem  15538  rplogcl  15568  logdivlti  15570  cxplt  15605  cxple  15606  rpabscxpbnd  15629  ltexp2  15630  iooref1o  16462