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

Theorem elrpd 10646
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 10614 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 646 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4212   RRcr 8989   0cc0 8990    < clt 9120   RR+crp 10612
This theorem is referenced by:  xov1plusxeqvd  11041  ltexp2a  11431  expcan  11432  ltexp2  11433  leexp2a  11435  expnlbnd2  11510  discr  11516  sqrlem4  12051  sqrlem7  12054  rpsqrcl  12070  absrpcl  12093  rlimrege0  12373  mulcn2  12389  rpefcl  12705  eflt  12718  ef01bndlem  12785  stdbdmopn  18548  methaus  18550  nmrpcl  18666  nlmvscnlem1  18722  metnrmlem1a  18888  icopnfcnv  18967  evth  18984  lebnumlem1  18986  nmoleub2lem3  19123  ipcnlem1  19199  minveclem4  19333  vitalilem4  19503  mbfmulc2lem  19539  itg2gt0  19652  dveflem  19863  dvferm1lem  19868  dvferm2  19871  aaliou3lem3  20261  psercnlem1  20341  pserdvlem1  20343  pserdv  20345  reeff1olem  20362  pilem2  20368  pilem3  20369  tanrpcl  20412  cosordlem  20433  rplogcl  20499  logdivlti  20515  logdivlt  20516  logdivle  20517  dvloglem  20539  recxpcl  20566  rpcxpcl  20567  mulcxp  20576  cxple2  20588  cxpsqr  20594  cxpcn3  20632  loglesqr  20642  atanlogaddlem  20753  atantan  20763  atanbnd  20766  rlimcnp  20804  rlimcnp2  20805  efrlim  20808  cxp2limlem  20814  cxp2lim  20815  cxploglim2  20817  jensen  20827  harmonicubnd  20848  fsumharmonic  20850  ftalem2  20856  basellem3  20865  basellem8  20870  chtrpcl  20958  fsumvma2  20998  chpval2  21002  chpchtsum  21003  chpub  21004  efexple  21065  chebbnd1lem2  21164  chebbnd1lem3  21165  chebbnd1  21166  chtppilimlem1  21167  chtppilimlem2  21168  chtppilim  21169  chebbnd2  21171  chto1lb  21172  chpchtlim  21173  chpo1ub  21174  rplogsumlem2  21179  dchrisumlema  21182  dchrisumlem3  21185  dchrvmasumlem2  21192  dchrvmasumiflem1  21195  dchrisum0lema  21208  chpdifbndlem1  21247  chpdifbndlem2  21248  chpdifbnd  21249  selberg3lem1  21251  pntrsumo1  21259  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntpbnd  21282  pntibndlem2  21285  pntibndlem3  21286  pntibnd  21287  pntlemd  21288  pntlem3  21303  pntleml  21305  pnt2  21307  pnt  21308  abvcxp  21309  ostth2lem1  21312  padicabv  21324  ostth2lem3  21329  ostth2lem4  21330  ostth2  21331  ostth3  21332  blocnilem  22305  minvecolem4  22382  minvecolem5  22383  xrge0iifhom  24323  cndprobprob  24696  lgamgulmlem2  24814  rprisefaccl  25339  mblfinlem3  26245  mblfinlem4  26246  itg2addnclem  26256  itg2gt0cn  26260  ftc1anclem7  26286  ftc1anc  26288  dvreasin  26290  areacirclem1  26292  areacirclem4  26295  areacirc  26297  geomcau  26465  blbnd  26496  prdsbnd2  26504  rrnequiv  26544  pell14qrrp  26923  pellfundex  26949  pellfundrp  26951  rmspecfund  26972  rmspecpos  26979  stoweidlem25  27750  stoweidlem28  27753  stoweidlem42  27767  stoweidlem49  27774  wallispilem3  27792  wallispilem4  27793  wallispi  27795  wallispi2lem1  27796  stirlinglem5  27803  stirlinglem10  27808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-rp 10613
  Copyright terms: Public domain W3C validator