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

Theorem elrpd 11037
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 11005 . 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 1756   class class class wbr 4304   RRcr 9293   0cc0 9294    < clt 9430   RR+crp 11003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-rp 11004
This theorem is referenced by:  xov1plusxeqvd  11443  ltexp2a  11927  expcan  11928  ltexp2  11929  leexp2a  11931  expnlbnd2  12007  discr  12013  sqrlem4  12747  sqrlem7  12750  rpsqrcl  12766  absrpcl  12789  rlimrege0  13069  mulcn2  13085  rpefcl  13400  eflt  13413  ef01bndlem  13480  stdbdmopn  20105  methaus  20107  nmrpcl  20223  nlmvscnlem1  20279  metnrmlem1a  20446  icopnfcnv  20526  evth  20543  lebnumlem1  20545  nmoleub2lem3  20682  ipcnlem1  20769  minveclem4  20931  vitalilem4  21103  mbfmulc2lem  21137  itg2gt0  21250  dveflem  21463  dvferm1lem  21468  dvferm2  21471  aaliou3lem3  21822  psercnlem1  21902  pserdvlem1  21904  pserdv  21906  reeff1olem  21923  pilem2  21929  pilem3  21930  tanrpcl  21978  cosordlem  21999  rplogcl  22065  logdivlti  22081  logdivlt  22082  logdivle  22083  dvloglem  22105  recxpcl  22132  rpcxpcl  22133  mulcxp  22142  cxple2  22154  cxpsqr  22160  cxpcn3  22198  loglesqr  22208  atanlogaddlem  22320  atantan  22330  atanbnd  22333  rlimcnp  22371  rlimcnp2  22372  efrlim  22375  cxp2limlem  22381  cxp2lim  22382  cxploglim2  22384  jensen  22394  harmonicubnd  22415  fsumharmonic  22417  ftalem2  22423  basellem3  22432  basellem8  22437  chtrpcl  22525  fsumvma2  22565  chpval2  22569  chpchtsum  22570  chpub  22571  efexple  22632  chebbnd1lem2  22731  chebbnd1lem3  22732  chebbnd1  22733  chtppilimlem1  22734  chtppilimlem2  22735  chtppilim  22736  chebbnd2  22738  chto1lb  22739  chpchtlim  22740  chpo1ub  22741  rplogsumlem2  22746  dchrisumlema  22749  dchrisumlem3  22752  dchrvmasumlem2  22759  dchrvmasumiflem1  22762  dchrisum0lema  22775  chpdifbndlem1  22814  chpdifbndlem2  22815  chpdifbnd  22816  selberg3lem1  22818  pntrsumo1  22826  pntpbnd1a  22846  pntpbnd1  22847  pntpbnd2  22848  pntpbnd  22849  pntibndlem2  22852  pntibndlem3  22853  pntibnd  22854  pntlemd  22855  pntlem3  22870  pntleml  22872  pnt2  22874  pnt  22875  abvcxp  22876  ostth2lem1  22879  padicabv  22891  ostth2lem3  22896  ostth2lem4  22897  ostth2  22898  ostth3  22899  ttgcontlem1  23143  blocnilem  24216  minvecolem4  24293  minvecolem5  24294  mul2lt0rgt0  26051  mul2lt0bi  26054  xrge0iifhom  26379  cndprobprob  26833  signsply0  26964  lgamgulmlem2  27028  rprisefaccl  27538  tan2h  28436  mblfinlem3  28442  mblfinlem4  28443  itg2addnclem  28455  itg2gt0cn  28459  ftc1anclem7  28485  ftc1anc  28487  dvasin  28492  areacirclem1  28496  areacirclem4  28499  areacirc  28501  geomcau  28667  blbnd  28698  prdsbnd2  28706  rrnequiv  28746  pell14qrrp  29213  pellfundex  29239  pellfundrp  29241  rmspecfund  29262  rmspecpos  29269  areaquad  29604  stoweidlem25  29832  stoweidlem28  29835  stoweidlem42  29849  stoweidlem49  29856  wallispilem3  29874  wallispilem4  29875  wallispi  29877  wallispi2lem1  29878  stirlinglem5  29885  stirlinglem10  29890
  Copyright terms: Public domain W3C validator