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

Theorem elrpd 10404
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 10372 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 645 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  xov1plusxeqvd  10796  ltexp2a  11169  expcan  11170  ltexp2  11171  leexp2a  11173  expnlbnd2  11248  discr  11254  sqrlem4  11747  sqrlem7  11750  rpsqrcl  11766  absrpcl  11789  rlimrege0  12069  mulcn2  12085  rpefcl  12400  eflt  12413  ef01bndlem  12480  stdbdmopn  18080  methaus  18082  nmrpcl  18157  nlmvscnlem1  18213  metnrmlem1a  18378  icopnfcnv  18456  evth  18473  lebnumlem1  18475  nmoleub2lem3  18612  ipcnlem1  18688  minveclem4  18812  vitalilem4  18982  mbfmulc2lem  19018  itg2gt0  19131  dveflem  19342  dvferm1lem  19347  dvferm2  19350  aaliou3lem3  19740  psercnlem1  19817  pserdvlem1  19819  pserdv  19821  reeff1olem  19838  pilem2  19844  pilem3  19845  tanrpcl  19888  cosordlem  19909  rplogcl  19974  logdivlti  19987  logdivlt  19988  logdivle  19989  dvloglem  20011  recxpcl  20038  rpcxpcl  20039  mulcxp  20048  cxple2  20060  cxpsqr  20066  cxpcn3  20104  loglesqr  20114  atanlogaddlem  20225  atantan  20235  atanbnd  20238  rlimcnp  20276  rlimcnp2  20277  efrlim  20280  cxp2limlem  20286  cxp2lim  20287  cxploglim2  20289  jensen  20299  harmonicubnd  20319  fsumharmonic  20321  ftalem2  20327  basellem3  20336  basellem8  20341  chtrpcl  20429  fsumvma2  20469  chpval2  20473  chpchtsum  20474  chpub  20475  efexple  20536  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  chtppilimlem2  20639  chtppilim  20640  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ub  20645  rplogsumlem2  20650  dchrisumlema  20653  dchrisumlem3  20656  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0lema  20679  chpdifbndlem1  20718  chpdifbndlem2  20719  chpdifbnd  20720  selberg3lem1  20722  pntrsumo1  20730  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntpbnd  20753  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemd  20759  pntlem3  20774  pntleml  20776  pnt2  20778  pnt  20779  abvcxp  20780  ostth2lem1  20783  padicabv  20795  ostth2lem3  20800  ostth2lem4  20801  ostth2  20802  ostth3  20803  blocnilem  21398  minvecolem4  21475  minvecolem5  21476  xrge0iifhom  23334  itg2addnclem  25003  itg2gt0cn  25006  dvreasin  25026  areacirclem2  25028  areacirclem3  25029  areacirclem5  25032  areacirc  25034  lvsovso  25729  geomcau  26578  blbnd  26614  prdsbnd2  26622  rrnequiv  26662  pell14qrrp  27048  pellfundex  27074  pellfundrp  27076  rmspecfund  27097  rmspecpos  27104  stirlinglem5  27930  stirlinglem10  27935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-rp 10371
  Copyright terms: Public domain W3C validator