Theorem elrpd 9693

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 9655	. 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 2148   class class class wbr 4004   RRcr 7810   0cc0 7811   < clt 7992   RR+crp 9653

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-rp 9654

This theorem is referenced by:  mul2lt0rgt0  9760  mul2lt0np  9763  zltaddlt1le  10007  modqval  10324  ltexp2a  10572  leexp2a  10573  expnlbnd2  10646  nn0ltexp2  10689  resqrexlem1arp  11014  resqrexlemp1rp  11015  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemgt0  11029  resqrexlemglsq  11031  rpsqrtcl  11050  absrpclap  11070  rpmaxcl  11232  rpmincl  11246  xrminrpcl  11282  xrbdtri  11284  mulcn2  11320  reccn2ap  11321  climge0  11333  divcnv  11505  georeclim  11521  cvgratnnlembern  11531  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  cvgratz  11540  rpefcl  11693  efltim  11706  ef01bndlem  11764  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  bdmopn  14007  mulcncflem  14093  ivthinclemlopn  14117  ivthinclemuopn  14119  dveflem  14190  reeff1olem  14195  pilem3  14207  tanrpcl  14261  cosordlem  14273  rplogcl  14303  logdivlti  14305  cxplt  14339  cxple  14340  rpabscxpbnd  14362  ltexp2  14363  iooref1o  14785