Theorem elrpd 9901

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

Hypotheses

Ref	Expression
elrpd.1	|- ( ph -> A e. RR )
elrpd.2	|- ( ph -> 0 < A )

Assertion

Ref	Expression
elrpd	|- ( ph -> A e. RR+ )

Proof of Theorem elrpd

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 |- ( ph -> A e. RR )
2		elrpd.2	. 2 |- ( ph -> 0 < A )
3		elrp 9863	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
4	1, 2, 3	sylanbrc 417	1 |- ( ph -> A e. RR+ )

Syntax hints:   -> wi 4   e. wcel 2200   class class class wbr 4083   RRcr 8009   0cc0 8010   < clt 8192   RR+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  11532  resqrexlemp1rp  11533  resqrexlemcalc2  11542  resqrexlemcalc3  11543  resqrexlemgt0  11547  resqrexlemglsq  11549  rpsqrtcl  11568  absrpclap  11588  rpmaxcl  11750  rpmincl  11765  xrminrpcl  11801  xrbdtri  11803  mulcn2  11839  reccn2ap  11840  climge0  11852  divcnv  12024  georeclim  12040  cvgratnnlembern  12050  cvgratnnlemsumlt  12055  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  rpefcl  12212  efltim  12225  ef01bndlem  12283  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  bdmopn  15194  mulcncflem  15297  ivthinclemlopn  15326  ivthinclemuopn  15328  dveflem  15416  reeff1olem  15461  pilem3  15473  tanrpcl  15527  cosordlem  15539  rplogcl  15569  logdivlti  15571  cxplt  15606  cxple  15607  rpabscxpbnd  15630  ltexp2  15631  iooref1o  16490