MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrpd Structured version   Unicode version

Theorem elrpd 11021
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
StepHypRef Expression
1 elrpd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 elrpd.2 . 2  |-  ( ph  ->  0  <  A )
3 elrp 10989 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 659 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   class class class wbr 4289   RRcr 9277   0cc0 9278    < clt 9414   RR+crp 10987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-rp 10988
This theorem is referenced by:  xov1plusxeqvd  11427  ltexp2a  11911  expcan  11912  ltexp2  11913  leexp2a  11915  expnlbnd2  11991  discr  11997  sqrlem4  12731  sqrlem7  12734  rpsqrcl  12750  absrpcl  12773  rlimrege0  13053  mulcn2  13069  rpefcl  13384  eflt  13397  ef01bndlem  13464  stdbdmopn  20052  methaus  20054  nmrpcl  20170  nlmvscnlem1  20226  metnrmlem1a  20393  icopnfcnv  20473  evth  20490  lebnumlem1  20492  nmoleub2lem3  20629  ipcnlem1  20716  minveclem4  20878  vitalilem4  21050  mbfmulc2lem  21084  itg2gt0  21197  dveflem  21410  dvferm1lem  21415  dvferm2  21418  aaliou3lem3  21769  psercnlem1  21849  pserdvlem1  21851  pserdv  21853  reeff1olem  21870  pilem2  21876  pilem3  21877  tanrpcl  21925  cosordlem  21946  rplogcl  22012  logdivlti  22028  logdivlt  22029  logdivle  22030  dvloglem  22052  recxpcl  22079  rpcxpcl  22080  mulcxp  22089  cxple2  22101  cxpsqr  22107  cxpcn3  22145  loglesqr  22155  atanlogaddlem  22267  atantan  22277  atanbnd  22280  rlimcnp  22318  rlimcnp2  22319  efrlim  22322  cxp2limlem  22328  cxp2lim  22329  cxploglim2  22331  jensen  22341  harmonicubnd  22362  fsumharmonic  22364  ftalem2  22370  basellem3  22379  basellem8  22384  chtrpcl  22472  fsumvma2  22512  chpval2  22516  chpchtsum  22517  chpub  22518  efexple  22579  chebbnd1lem2  22678  chebbnd1lem3  22679  chebbnd1  22680  chtppilimlem1  22681  chtppilimlem2  22682  chtppilim  22683  chebbnd2  22685  chto1lb  22686  chpchtlim  22687  chpo1ub  22688  rplogsumlem2  22693  dchrisumlema  22696  dchrisumlem3  22699  dchrvmasumlem2  22706  dchrvmasumiflem1  22709  dchrisum0lema  22722  chpdifbndlem1  22761  chpdifbndlem2  22762  chpdifbnd  22763  selberg3lem1  22765  pntrsumo1  22773  pntpbnd1a  22793  pntpbnd1  22794  pntpbnd2  22795  pntpbnd  22796  pntibndlem2  22799  pntibndlem3  22800  pntibnd  22801  pntlemd  22802  pntlem3  22817  pntleml  22819  pnt2  22821  pnt  22822  abvcxp  22823  ostth2lem1  22826  padicabv  22838  ostth2lem3  22843  ostth2lem4  22844  ostth2  22845  ostth3  22846  ttgcontlem1  23066  blocnilem  24139  minvecolem4  24216  minvecolem5  24217  mul2lt0rgt0  25974  mul2lt0bi  25977  xrge0iifhom  26303  cndprobprob  26751  signsply0  26882  lgamgulmlem2  26946  rprisefaccl  27455  tan2h  28349  mblfinlem3  28355  mblfinlem4  28356  itg2addnclem  28368  itg2gt0cn  28372  ftc1anclem7  28398  ftc1anc  28400  dvasin  28405  areacirclem1  28409  areacirclem4  28412  areacirc  28414  geomcau  28580  blbnd  28611  prdsbnd2  28619  rrnequiv  28659  pell14qrrp  29126  pellfundex  29152  pellfundrp  29154  rmspecfund  29175  rmspecpos  29182  areaquad  29517  stoweidlem25  29745  stoweidlem28  29748  stoweidlem42  29762  stoweidlem49  29769  wallispilem3  29787  wallispilem4  29788  wallispi  29790  wallispi2lem1  29791  stirlinglem5  29798  stirlinglem10  29803
  Copyright terms: Public domain W3C validator