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

Theorem elrpd 11335
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 11301 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 669 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   class class class wbr 4401   RRcr 9535   0cc0 9536    < clt 9672   RR+crp 11299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-rp 11300
This theorem is referenced by:  mul2lt0rgt0  11396  mul2lt0bi  11399  xov1plusxeqvd  11775  ltexp2a  12321  expcan  12322  ltexp2  12323  leexp2a  12325  expnlbnd2  12400  discr  12406  sqrlem4  13302  sqrlem7  13305  rpsqrtcl  13321  absrpcl  13344  rlimrege0  13636  mulcn2  13652  fprodle  14043  rprisefaccl  14069  rpefcl  14151  eflt  14164  ef01bndlem  14231  stdbdmopn  21526  methaus  21528  nmrpcl  21626  nlmvscnlem1  21682  metnrmlem1a  21868  metnrmlem1aOLD  21883  icopnfcnv  21963  evth  21980  lebnumlem1  21982  lebnumlem1OLD  21985  nmoleub2lem3  22122  ipcnlem1  22209  minveclem4  22367  minveclem4OLD  22379  vitalilem4  22562  mbfmulc2lem  22596  itg2gt0  22711  dveflem  22924  dvferm1lem  22929  dvferm2  22932  aaliou3lem3  23293  psercnlem1  23373  pserdvlem1  23375  pserdv  23377  reeff1olem  23394  pilem2  23400  pilem2OLD  23401  pilem3  23402  pilem3OLD  23403  tanrpcl  23452  cosordlem  23473  rplogcl  23546  logdivlti  23562  logdivlt  23563  logdivle  23564  dvloglem  23586  recxpcl  23613  rpcxpcl  23614  mulcxp  23623  cxple2  23635  cxpsqrt  23641  cxpcn3  23681  loglesqrt  23691  atanlogaddlem  23832  atantan  23842  atanbnd  23845  rlimcnp  23884  rlimcnp2  23885  efrlim  23888  cxp2limlem  23894  cxp2lim  23895  cxploglim2  23897  jensen  23907  harmonicubnd  23928  fsumharmonic  23930  lgamgulmlem2  23948  ftalem2  23991  basellem3  24002  basellem8  24007  chtrpcl  24095  fsumvma2  24135  chpval2  24139  chpchtsum  24140  chpub  24141  efexple  24202  chebbnd1lem2  24301  chebbnd1lem3  24302  chebbnd1  24303  chtppilimlem1  24304  chtppilimlem2  24305  chtppilim  24306  chebbnd2  24308  chto1lb  24309  chpchtlim  24310  chpo1ub  24311  rplogsumlem2  24316  dchrisumlema  24319  dchrisumlem3  24322  dchrvmasumlem2  24329  dchrvmasumiflem1  24332  dchrisum0lema  24345  chpdifbndlem1  24384  chpdifbndlem2  24385  chpdifbnd  24386  selberg3lem1  24388  pntrsumo1  24396  pntpbnd1a  24416  pntpbnd1  24417  pntpbnd2  24418  pntpbnd  24419  pntibndlem2  24422  pntibndlem3  24423  pntibnd  24424  pntlemd  24425  pntlem3  24440  pntleml  24442  pnt2  24444  pnt  24445  abvcxp  24446  ostth2lem1  24449  padicabv  24461  ostth2lem3  24466  ostth2lem4  24467  ostth2  24468  ostth3  24469  ttgcontlem1  24908  blocnilem  26438  minvecolem4  26515  minvecolem5  26516  minvecolem4OLD  26525  minvecolem5OLD  26526  xrge0iifhom  28736  cndprobprob  29264  tan2h  31930  mblfinlem3  31972  mblfinlem4  31973  itg2addnclem  31986  itg2gt0cn  31990  ftc1anclem7  32016  ftc1anc  32018  dvasin  32021  areacirclem1  32025  areacirclem4  32028  areacirc  32030  geomcau  32081  blbnd  32112  prdsbnd2  32120  rrnequiv  32160  pell14qrrp  35700  pellfundex  35728  pellfundrp  35730  rmspecfund  35751  rmspecpos  35758  areaquad  36095  wwlemuld  36588  radcnvrat  36657  binomcxplemdvbinom  36696  binomcxplemnotnn0  36699  supxrgere  37550  supxrgelem  37554  xralrple2  37571  sinaover2ne0  37737  ioodvbdlimc1lem1  37797  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem1OLD  37799  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvnmul  37812  stoweidlem25  37879  stoweidlem28  37882  stoweidlem42  37897  stoweidlem49  37904  wallispilem3  37923  wallispilem4  37924  wallispi  37926  wallispi2lem1  37927  stirlinglem5  37934  stirlinglem10  37939  fourierdlem4  37967  fourierdlem6  37969  fourierdlem7  37970  fourierdlem19  37982  fourierdlem24  37987  fourierdlem26  37989  fourierdlem30  37993  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem51  38015  fourierdlem63  38027  fourierdlem64  38028  fourierdlem65  38029  fourierdlem73  38037  fourierdlem75  38039  fourierdlem79  38043  fourierdlem92  38056  fourierdlem109  38073  fouriersw  38089  etransclem35  38128  qndenserrnbllem  38157  hoiqssbllem1  38438  hoiqssbllem2  38439  m1mod0mod1  38717  rege1logbrege0  40356  fldivexpfllog2  40363  fllog2  40366
  Copyright terms: Public domain W3C validator