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

Theorem elrpd 11338
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 11304 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 668 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   class class class wbr 4426   RRcr 9537   0cc0 9538    < clt 9674   RR+crp 11302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-rp 11303
This theorem is referenced by:  mul2lt0rgt0  11399  mul2lt0bi  11402  xov1plusxeqvd  11776  ltexp2a  12321  expcan  12322  ltexp2  12323  leexp2a  12325  expnlbnd2  12400  discr  12406  sqrlem4  13288  sqrlem7  13291  rpsqrtcl  13307  absrpcl  13330  rlimrege0  13621  mulcn2  13637  fprodle  14028  rprisefaccl  14054  rpefcl  14136  eflt  14149  ef01bndlem  14216  stdbdmopn  21464  methaus  21466  nmrpcl  21564  nlmvscnlem1  21620  metnrmlem1a  21786  icopnfcnv  21866  evth  21883  lebnumlem1  21885  nmoleub2lem3  22022  ipcnlem1  22109  minveclem4  22267  vitalilem4  22446  mbfmulc2lem  22480  itg2gt0  22595  dveflem  22808  dvferm1lem  22813  dvferm2  22816  aaliou3lem3  23165  psercnlem1  23245  pserdvlem1  23247  pserdv  23249  reeff1olem  23266  pilem2  23272  pilem2OLD  23273  pilem3  23274  pilem3OLD  23275  tanrpcl  23324  cosordlem  23345  rplogcl  23418  logdivlti  23434  logdivlt  23435  logdivle  23436  dvloglem  23458  recxpcl  23485  rpcxpcl  23486  mulcxp  23495  cxple2  23507  cxpsqrt  23513  cxpcn3  23553  loglesqrt  23563  atanlogaddlem  23704  atantan  23714  atanbnd  23717  rlimcnp  23756  rlimcnp2  23757  efrlim  23760  cxp2limlem  23766  cxp2lim  23767  cxploglim2  23769  jensen  23779  harmonicubnd  23800  fsumharmonic  23802  lgamgulmlem2  23820  ftalem2  23863  basellem3  23872  basellem8  23877  chtrpcl  23965  fsumvma2  24005  chpval2  24009  chpchtsum  24010  chpub  24011  efexple  24072  chebbnd1lem2  24171  chebbnd1lem3  24172  chebbnd1  24173  chtppilimlem1  24174  chtppilimlem2  24175  chtppilim  24176  chebbnd2  24178  chto1lb  24179  chpchtlim  24180  chpo1ub  24181  rplogsumlem2  24186  dchrisumlema  24189  dchrisumlem3  24192  dchrvmasumlem2  24199  dchrvmasumiflem1  24202  dchrisum0lema  24215  chpdifbndlem1  24254  chpdifbndlem2  24255  chpdifbnd  24256  selberg3lem1  24258  pntrsumo1  24266  pntpbnd1a  24286  pntpbnd1  24287  pntpbnd2  24288  pntpbnd  24289  pntibndlem2  24292  pntibndlem3  24293  pntibnd  24294  pntlemd  24295  pntlem3  24310  pntleml  24312  pnt2  24314  pnt  24315  abvcxp  24316  ostth2lem1  24319  padicabv  24331  ostth2lem3  24336  ostth2lem4  24337  ostth2  24338  ostth3  24339  ttgcontlem1  24761  blocnilem  26290  minvecolem4  26367  minvecolem5  26368  xrge0iifhom  28582  cndprobprob  29097  tan2h  31641  mblfinlem3  31683  mblfinlem4  31684  itg2addnclem  31697  itg2gt0cn  31701  ftc1anclem7  31727  ftc1anc  31729  dvasin  31732  areacirclem1  31736  areacirclem4  31739  areacirc  31741  geomcau  31792  blbnd  31823  prdsbnd2  31831  rrnequiv  31871  pell14qrrp  35414  pellfundex  35440  pellfundrp  35442  rmspecfund  35463  rmspecpos  35470  areaquad  35800  wwlemuld  36231  radcnvrat  36300  binomcxplemdvbinom  36339  binomcxplemnotnn0  36342  supxrgere  37165  supxrgelem  37169  sinaover2ne0  37315  ioodvbdlimc1lem1  37375  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  dvnmul  37387  stoweidlem25  37454  stoweidlem28  37457  stoweidlem42  37472  stoweidlem49  37479  wallispilem3  37498  wallispilem4  37499  wallispi  37501  wallispi2lem1  37502  stirlinglem5  37509  stirlinglem10  37514  fourierdlem4  37542  fourierdlem6  37544  fourierdlem7  37545  fourierdlem19  37557  fourierdlem24  37562  fourierdlem26  37564  fourierdlem30  37568  fourierdlem42  37580  fourierdlem51  37589  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem73  37611  fourierdlem75  37613  fourierdlem79  37617  fourierdlem92  37630  fourierdlem109  37647  fouriersw  37663  etransclem35  37701  m1mod0mod1  38113  rege1logbrege0  39130  fldivexpfllog2  39137  fllog2  39140
  Copyright terms: Public domain W3C validator