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

Theorem elrpd 10602
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 10570 . 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 1721   class class class wbr 4172   RRcr 8945   0cc0 8946    < clt 9076   RR+crp 10568
This theorem is referenced by:  xov1plusxeqvd  10997  ltexp2a  11386  expcan  11387  ltexp2  11388  leexp2a  11390  expnlbnd2  11465  discr  11471  sqrlem4  12006  sqrlem7  12009  rpsqrcl  12025  absrpcl  12048  rlimrege0  12328  mulcn2  12344  rpefcl  12660  eflt  12673  ef01bndlem  12740  stdbdmopn  18501  methaus  18503  nmrpcl  18619  nlmvscnlem1  18675  metnrmlem1a  18841  icopnfcnv  18920  evth  18937  lebnumlem1  18939  nmoleub2lem3  19076  ipcnlem1  19152  minveclem4  19286  vitalilem4  19456  mbfmulc2lem  19492  itg2gt0  19605  dveflem  19816  dvferm1lem  19821  dvferm2  19824  aaliou3lem3  20214  psercnlem1  20294  pserdvlem1  20296  pserdv  20298  reeff1olem  20315  pilem2  20321  pilem3  20322  tanrpcl  20365  cosordlem  20386  rplogcl  20452  logdivlti  20468  logdivlt  20469  logdivle  20470  dvloglem  20492  recxpcl  20519  rpcxpcl  20520  mulcxp  20529  cxple2  20541  cxpsqr  20547  cxpcn3  20585  loglesqr  20595  atanlogaddlem  20706  atantan  20716  atanbnd  20719  rlimcnp  20757  rlimcnp2  20758  efrlim  20761  cxp2limlem  20767  cxp2lim  20768  cxploglim2  20770  jensen  20780  harmonicubnd  20801  fsumharmonic  20803  ftalem2  20809  basellem3  20818  basellem8  20823  chtrpcl  20911  fsumvma2  20951  chpval2  20955  chpchtsum  20956  chpub  20957  efexple  21018  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  rplogsumlem2  21132  dchrisumlema  21135  dchrisumlem3  21138  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0lema  21161  chpdifbndlem1  21200  chpdifbndlem2  21201  chpdifbnd  21202  selberg3lem1  21204  pntrsumo1  21212  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntpbnd  21235  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemd  21241  pntlem3  21256  pntleml  21258  pnt2  21260  pnt  21261  abvcxp  21262  ostth2lem1  21265  padicabv  21277  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  blocnilem  22258  minvecolem4  22335  minvecolem5  22336  xrge0iifhom  24276  cndprobprob  24649  lgamgulmlem2  24767  rprisefaccl  25291  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2gt0cn  26159  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  areacirclem5  26185  areacirc  26187  geomcau  26355  blbnd  26386  prdsbnd2  26394  rrnequiv  26434  pell14qrrp  26813  pellfundex  26839  pellfundrp  26841  rmspecfund  26862  rmspecpos  26869  stoweidlem25  27641  stoweidlem28  27644  stoweidlem42  27658  stoweidlem49  27665  wallispilem3  27683  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  stirlinglem5  27694  stirlinglem10  27699
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-rp 10569
  Copyright terms: Public domain W3C validator