Theorem elrpd 9916

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 9878	. 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 4084   RRcr 8019   0cc0 8020   < clt 8202   RR+crp 9876

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4085  df-rp 9877

This theorem is referenced by:  mul2lt0rgt0  9983  mul2lt0np  9986  zltaddlt1le  10230  modqval  10574  ltexp2a  10841  leexp2a  10842  expnlbnd2  10915  nn0ltexp2  10959  resqrexlem1arp  11553  resqrexlemp1rp  11554  resqrexlemcalc2  11563  resqrexlemcalc3  11564  resqrexlemgt0  11568  resqrexlemglsq  11570  rpsqrtcl  11589  absrpclap  11609  rpmaxcl  11771  rpmincl  11786  xrminrpcl  11822  xrbdtri  11824  mulcn2  11860  reccn2ap  11861  climge0  11873  divcnv  12045  georeclim  12061  cvgratnnlembern  12071  cvgratnnlemsumlt  12076  cvgratnnlemfm  12077  cvgratnnlemrate  12078  cvgratnn  12079  cvgratz  12080  rpefcl  12233  efltim  12246  ef01bndlem  12304  pythagtriplem12  12835  pythagtriplem14  12837  pythagtriplem16  12839  bdmopn  15215  mulcncflem  15318  ivthinclemlopn  15347  ivthinclemuopn  15349  dveflem  15437  reeff1olem  15482  pilem3  15494  tanrpcl  15548  cosordlem  15560  rplogcl  15590  logdivlti  15592  cxplt  15627  cxple  15628  rpabscxpbnd  15651  ltexp2  15652  iooref1o  16548