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

Theorem elrpd 11253
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 11221 . 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 1767   class class class wbr 4447   RRcr 9490   0cc0 9491    < clt 9627   RR+crp 11219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-rp 11220
This theorem is referenced by:  xov1plusxeqvd  11665  ltexp2a  12184  expcan  12185  ltexp2  12186  leexp2a  12188  expnlbnd2  12264  discr  12270  sqrlem4  13041  sqrlem7  13044  rpsqrtcl  13060  absrpcl  13083  rlimrege0  13364  mulcn2  13380  rpefcl  13699  eflt  13712  ef01bndlem  13779  stdbdmopn  20772  methaus  20774  nmrpcl  20890  nlmvscnlem1  20946  metnrmlem1a  21113  icopnfcnv  21193  evth  21210  lebnumlem1  21212  nmoleub2lem3  21349  ipcnlem1  21436  minveclem4  21598  vitalilem4  21771  mbfmulc2lem  21805  itg2gt0  21918  dveflem  22131  dvferm1lem  22136  dvferm2  22139  aaliou3lem3  22490  psercnlem1  22570  pserdvlem1  22572  pserdv  22574  reeff1olem  22591  pilem2  22597  pilem3  22598  tanrpcl  22646  cosordlem  22667  rplogcl  22733  logdivlti  22749  logdivlt  22750  logdivle  22751  dvloglem  22773  recxpcl  22800  rpcxpcl  22801  mulcxp  22810  cxple2  22822  cxpsqrt  22828  cxpcn3  22866  loglesqrt  22876  atanlogaddlem  22988  atantan  22998  atanbnd  23001  rlimcnp  23039  rlimcnp2  23040  efrlim  23043  cxp2limlem  23049  cxp2lim  23050  cxploglim2  23052  jensen  23062  harmonicubnd  23083  fsumharmonic  23085  ftalem2  23091  basellem3  23100  basellem8  23105  chtrpcl  23193  fsumvma2  23233  chpval2  23237  chpchtsum  23238  chpub  23239  efexple  23300  chebbnd1lem2  23399  chebbnd1lem3  23400  chebbnd1  23401  chtppilimlem1  23402  chtppilimlem2  23403  chtppilim  23404  chebbnd2  23406  chto1lb  23407  chpchtlim  23408  chpo1ub  23409  rplogsumlem2  23414  dchrisumlema  23417  dchrisumlem3  23420  dchrvmasumlem2  23427  dchrvmasumiflem1  23430  dchrisum0lema  23443  chpdifbndlem1  23482  chpdifbndlem2  23483  chpdifbnd  23484  selberg3lem1  23486  pntrsumo1  23494  pntpbnd1a  23514  pntpbnd1  23515  pntpbnd2  23516  pntpbnd  23517  pntibndlem2  23520  pntibndlem3  23521  pntibnd  23522  pntlemd  23523  pntlem3  23538  pntleml  23540  pnt2  23542  pnt  23543  abvcxp  23544  ostth2lem1  23547  padicabv  23559  ostth2lem3  23564  ostth2lem4  23565  ostth2  23566  ostth3  23567  ttgcontlem1  23880  blocnilem  25411  minvecolem4  25488  minvecolem5  25489  mul2lt0rgt0  27250  mul2lt0bi  27253  xrge0iifhom  27571  cndprobprob  28033  signsply0  28164  lgamgulmlem2  28228  rprisefaccl  28738  tan2h  29640  mblfinlem3  29646  mblfinlem4  29647  itg2addnclem  29659  itg2gt0cn  29663  ftc1anclem7  29689  ftc1anc  29691  dvasin  29696  areacirclem1  29700  areacirclem4  29703  areacirc  29705  geomcau  29871  blbnd  29902  prdsbnd2  29910  rrnequiv  29950  pell14qrrp  30416  pellfundex  30442  pellfundrp  30444  rmspecfund  30465  rmspecpos  30472  areaquad  30805  abssubrp  31050  sinaover2ne0  31220  ioodvbdlimc1lem1  31277  ioodvbdlimc1lem2  31278  ioodvbdlimc2lem  31280  stoweidlem25  31341  stoweidlem28  31344  stoweidlem42  31358  stoweidlem49  31365  wallispilem3  31383  wallispilem4  31384  wallispi  31386  wallispi2lem1  31387  stirlinglem5  31394  stirlinglem10  31399  fourierdlem6  31429  fourierdlem7  31430  fourierdlem19  31442  fourierdlem24  31447  fourierdlem26  31449  fourierdlem30  31453  fourierdlem42  31465  fourierdlem45  31468  fourierdlem51  31474  fourierdlem63  31486  fourierdlem64  31487  fourierdlem65  31488  fourierdlem73  31496  fourierdlem75  31498  fourierdlem79  31502  fourierdlem89  31512  fourierdlem90  31513  fourierdlem91  31514  fourierdlem92  31515  fourierdlem109  31532  fouriersw  31548
  Copyright terms: Public domain W3C validator