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

Theorem elrpd 10388
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 10356 . 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 1684   class class class wbr 4023   RRcr 8736   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  xov1plusxeqvd  10780  ltexp2a  11153  expcan  11154  ltexp2  11155  leexp2a  11157  expnlbnd2  11232  discr  11238  sqrlem4  11731  sqrlem7  11734  rpsqrcl  11750  absrpcl  11773  rlimrege0  12053  mulcn2  12069  rpefcl  12384  eflt  12397  ef01bndlem  12464  stdbdmopn  18064  methaus  18066  nmrpcl  18141  nlmvscnlem1  18197  metnrmlem1a  18362  icopnfcnv  18440  evth  18457  lebnumlem1  18459  nmoleub2lem3  18596  ipcnlem1  18672  minveclem4  18796  vitalilem4  18966  mbfmulc2lem  19002  itg2gt0  19115  dveflem  19326  dvferm1lem  19331  dvferm2  19334  aaliou3lem3  19724  psercnlem1  19801  pserdvlem1  19803  pserdv  19805  reeff1olem  19822  pilem2  19828  pilem3  19829  tanrpcl  19872  cosordlem  19893  rplogcl  19958  logdivlti  19971  logdivlt  19972  logdivle  19973  dvloglem  19995  recxpcl  20022  rpcxpcl  20023  mulcxp  20032  cxple2  20044  cxpsqr  20050  cxpcn3  20088  loglesqr  20098  atanlogaddlem  20209  atantan  20219  atanbnd  20222  rlimcnp  20260  rlimcnp2  20261  efrlim  20264  cxp2limlem  20270  cxp2lim  20271  cxploglim2  20273  jensen  20283  harmonicubnd  20303  fsumharmonic  20305  ftalem2  20311  basellem3  20320  basellem8  20325  chtrpcl  20413  fsumvma2  20453  chpval2  20457  chpchtsum  20458  chpub  20459  efexple  20520  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem1  20622  chtppilimlem2  20623  chtppilim  20624  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  rplogsumlem2  20634  dchrisumlema  20637  dchrisumlem3  20640  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0lema  20663  chpdifbndlem1  20702  chpdifbndlem2  20703  chpdifbnd  20704  selberg3lem1  20706  pntrsumo1  20714  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntpbnd  20737  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemd  20743  pntlem3  20758  pntleml  20760  pnt2  20762  pnt  20763  abvcxp  20764  ostth2lem1  20767  padicabv  20779  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  blocnilem  21382  minvecolem4  21459  minvecolem5  21460  xrge0iifhom  23319  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  areacirclem5  24929  areacirc  24931  lvsovso  25626  geomcau  26475  blbnd  26511  prdsbnd2  26519  rrnequiv  26559  pell14qrrp  26945  pellfundex  26971  pellfundrp  26973  rmspecfund  26994  rmspecpos  27001  stirlinglem5  27827  stirlinglem10  27832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-rp 10355
  Copyright terms: Public domain W3C validator