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

Theorem elrpd 11265
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 11233 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 664 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   class class class wbr 4437   RRcr 9494   0cc0 9495    < clt 9631   RR+crp 11231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-rp 11232
This theorem is referenced by:  xov1plusxeqvd  11677  ltexp2a  12199  expcan  12200  ltexp2  12201  leexp2a  12203  expnlbnd2  12279  discr  12285  sqrlem4  13061  sqrlem7  13064  rpsqrtcl  13080  absrpcl  13103  rlimrege0  13384  mulcn2  13400  rpefcl  13821  eflt  13834  ef01bndlem  13901  stdbdmopn  20999  methaus  21001  nmrpcl  21117  nlmvscnlem1  21173  metnrmlem1a  21340  icopnfcnv  21420  evth  21437  lebnumlem1  21439  nmoleub2lem3  21576  ipcnlem1  21663  minveclem4  21825  vitalilem4  21998  mbfmulc2lem  22032  itg2gt0  22145  dveflem  22358  dvferm1lem  22363  dvferm2  22366  aaliou3lem3  22718  psercnlem1  22798  pserdvlem1  22800  pserdv  22802  reeff1olem  22819  pilem2  22825  pilem3  22826  tanrpcl  22875  cosordlem  22896  rplogcl  22967  logdivlti  22983  logdivlt  22984  logdivle  22985  dvloglem  23007  recxpcl  23034  rpcxpcl  23035  mulcxp  23044  cxple2  23056  cxpsqrt  23062  cxpcn3  23100  loglesqrt  23110  atanlogaddlem  23222  atantan  23232  atanbnd  23235  rlimcnp  23273  rlimcnp2  23274  efrlim  23277  cxp2limlem  23283  cxp2lim  23284  cxploglim2  23286  jensen  23296  harmonicubnd  23317  fsumharmonic  23319  ftalem2  23325  basellem3  23334  basellem8  23339  chtrpcl  23427  fsumvma2  23467  chpval2  23471  chpchtsum  23472  chpub  23473  efexple  23534  chebbnd1lem2  23633  chebbnd1lem3  23634  chebbnd1  23635  chtppilimlem1  23636  chtppilimlem2  23637  chtppilim  23638  chebbnd2  23640  chto1lb  23641  chpchtlim  23642  chpo1ub  23643  rplogsumlem2  23648  dchrisumlema  23651  dchrisumlem3  23654  dchrvmasumlem2  23661  dchrvmasumiflem1  23664  dchrisum0lema  23677  chpdifbndlem1  23716  chpdifbndlem2  23717  chpdifbnd  23718  selberg3lem1  23720  pntrsumo1  23728  pntpbnd1a  23748  pntpbnd1  23749  pntpbnd2  23750  pntpbnd  23751  pntibndlem2  23754  pntibndlem3  23755  pntibnd  23756  pntlemd  23757  pntlem3  23772  pntleml  23774  pnt2  23776  pnt  23777  abvcxp  23778  ostth2lem1  23781  padicabv  23793  ostth2lem3  23798  ostth2lem4  23799  ostth2  23800  ostth3  23801  ttgcontlem1  24166  blocnilem  25697  minvecolem4  25774  minvecolem5  25775  mul2lt0rgt0  27544  mul2lt0bi  27547  xrge0iifhom  27897  cndprobprob  28355  lgamgulmlem2  28550  rprisefaccl  29121  tan2h  30023  mblfinlem3  30029  mblfinlem4  30030  itg2addnclem  30042  itg2gt0cn  30046  ftc1anclem7  30072  ftc1anc  30074  dvasin  30079  areacirclem1  30083  areacirclem4  30086  areacirc  30088  geomcau  30228  blbnd  30259  prdsbnd2  30267  rrnequiv  30307  pell14qrrp  30772  pellfundex  30798  pellfundrp  30800  rmspecfund  30821  rmspecpos  30828  areaquad  31160  radcnvrat  31171  fprodle  31558  sinaover2ne0  31622  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmul  31694  stoweidlem25  31761  stoweidlem28  31764  stoweidlem42  31778  stoweidlem49  31785  wallispilem3  31803  wallispilem4  31804  wallispi  31806  wallispi2lem1  31807  stirlinglem5  31814  stirlinglem10  31819  fourierdlem4  31847  fourierdlem6  31849  fourierdlem7  31850  fourierdlem19  31862  fourierdlem24  31867  fourierdlem26  31869  fourierdlem30  31873  fourierdlem42  31885  fourierdlem51  31894  fourierdlem63  31906  fourierdlem64  31907  fourierdlem65  31908  fourierdlem73  31916  fourierdlem75  31918  fourierdlem79  31922  fourierdlem92  31935  fourierdlem109  31952  fouriersw  31968  etransclem35  32006  wwlemuld  37772
  Copyright terms: Public domain W3C validator