Theorem elrpd 9692

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 9654	. 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 4003   RRcr 7809   0cc0 7810   < clt 7991   RR+crp 9652

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-rp 9653

This theorem is referenced by:  mul2lt0rgt0  9759  mul2lt0np  9762  zltaddlt1le  10006  modqval  10323  ltexp2a  10571  leexp2a  10572  expnlbnd2  10645  nn0ltexp2  10688  resqrexlem1arp  11013  resqrexlemp1rp  11014  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemgt0  11028  resqrexlemglsq  11030  rpsqrtcl  11049  absrpclap  11069  rpmaxcl  11231  rpmincl  11245  xrminrpcl  11281  xrbdtri  11283  mulcn2  11319  reccn2ap  11320  climge0  11332  divcnv  11504  georeclim  11520  cvgratnnlembern  11530  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratnn  11538  cvgratz  11539  rpefcl  11692  efltim  11705  ef01bndlem  11763  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  bdmopn  13974  mulcncflem  14060  ivthinclemlopn  14084  ivthinclemuopn  14086  dveflem  14157  reeff1olem  14162  pilem3  14174  tanrpcl  14228  cosordlem  14240  rplogcl  14270  logdivlti  14272  cxplt  14306  cxple  14307  rpabscxpbnd  14329  ltexp2  14330  iooref1o  14752