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

Theorem elrpd 11361
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 11327 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 677 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   class class class wbr 4395   RRcr 9556   0cc0 9557    < clt 9693   RR+crp 11325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-rp 11326
This theorem is referenced by:  mul2lt0rgt0  11422  mul2lt0bi  11425  xov1plusxeqvd  11804  ltexp2a  12362  expcan  12363  ltexp2  12364  leexp2a  12366  expnlbnd2  12441  discr  12447  sqrlem4  13386  sqrlem7  13389  rpsqrtcl  13405  absrpcl  13428  rlimrege0  13720  mulcn2  13736  fprodle  14127  rprisefaccl  14153  rpefcl  14235  eflt  14248  ef01bndlem  14315  stdbdmopn  21611  methaus  21613  nmrpcl  21711  nlmvscnlem1  21767  metnrmlem1a  21953  metnrmlem1aOLD  21968  icopnfcnv  22048  evth  22065  lebnumlem1  22067  lebnumlem1OLD  22070  nmoleub2lem3  22207  ipcnlem1  22294  minveclem4  22452  minveclem4OLD  22464  vitalilem4  22648  mbfmulc2lem  22682  itg2gt0  22797  dveflem  23010  dvferm1lem  23015  dvferm2  23018  aaliou3lem3  23379  psercnlem1  23459  pserdvlem1  23461  pserdv  23463  reeff1olem  23480  pilem2  23486  pilem2OLD  23487  pilem3  23488  pilem3OLD  23489  tanrpcl  23538  cosordlem  23559  rplogcl  23632  logdivlti  23648  logdivlt  23649  logdivle  23650  dvloglem  23672  recxpcl  23699  rpcxpcl  23700  mulcxp  23709  cxple2  23721  cxpsqrt  23727  cxpcn3  23767  loglesqrt  23777  atanlogaddlem  23918  atantan  23928  atanbnd  23931  rlimcnp  23970  rlimcnp2  23971  efrlim  23974  cxp2limlem  23980  cxp2lim  23981  cxploglim2  23983  jensen  23993  harmonicubnd  24014  fsumharmonic  24016  lgamgulmlem2  24034  ftalem2  24077  basellem3  24088  basellem8  24093  chtrpcl  24181  fsumvma2  24221  chpval2  24225  chpchtsum  24226  chpub  24227  efexple  24288  chebbnd1lem2  24387  chebbnd1lem3  24388  chebbnd1  24389  chtppilimlem1  24390  chtppilimlem2  24391  chtppilim  24392  chebbnd2  24394  chto1lb  24395  chpchtlim  24396  chpo1ub  24397  rplogsumlem2  24402  dchrisumlema  24405  dchrisumlem3  24408  dchrvmasumlem2  24415  dchrvmasumiflem1  24418  dchrisum0lema  24431  chpdifbndlem1  24470  chpdifbndlem2  24471  chpdifbnd  24472  selberg3lem1  24474  pntrsumo1  24482  pntpbnd1a  24502  pntpbnd1  24503  pntpbnd2  24504  pntpbnd  24505  pntibndlem2  24508  pntibndlem3  24509  pntibnd  24510  pntlemd  24511  pntlem3  24526  pntleml  24528  pnt2  24530  pnt  24531  abvcxp  24532  ostth2lem1  24535  padicabv  24547  ostth2lem3  24552  ostth2lem4  24553  ostth2  24554  ostth3  24555  ttgcontlem1  24994  blocnilem  26526  minvecolem4  26603  minvecolem5  26604  minvecolem4OLD  26613  minvecolem5OLD  26614  xrge0iifhom  28817  cndprobprob  29344  tan2h  32001  mblfinlem3  32043  mblfinlem4  32044  itg2addnclem  32057  itg2gt0cn  32061  ftc1anclem7  32087  ftc1anc  32089  dvasin  32092  areacirclem1  32096  areacirclem4  32099  areacirc  32101  geomcau  32152  blbnd  32183  prdsbnd2  32191  rrnequiv  32231  pell14qrrp  35777  pellfundex  35805  pellfundrp  35807  rmspecfund  35828  rmspecpos  35835  areaquad  36172  wwlemuld  36665  radcnvrat  36733  binomcxplemdvbinom  36772  binomcxplemnotnn0  36775  supxrgere  37643  supxrgelem  37647  xralrple2  37664  sinaover2ne0  37840  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnmul  37915  stoweidlem25  37997  stoweidlem28  38000  stoweidlem42  38015  stoweidlem49  38022  wallispilem3  38041  wallispilem4  38042  wallispi  38044  wallispi2lem1  38045  stirlinglem5  38052  stirlinglem10  38057  fourierdlem4  38085  fourierdlem6  38087  fourierdlem7  38088  fourierdlem19  38100  fourierdlem24  38105  fourierdlem26  38107  fourierdlem30  38111  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem51  38133  fourierdlem63  38145  fourierdlem64  38146  fourierdlem65  38147  fourierdlem73  38155  fourierdlem75  38157  fourierdlem79  38161  fourierdlem92  38174  fourierdlem109  38191  fouriersw  38207  etransclem35  38246  qndenserrnbllem  38275  hoiqssbllem1  38562  hoiqssbllem2  38563  m1mod0mod1  38868  rege1logbrege0  40877  fldivexpfllog2  40884  fllog2  40887
  Copyright terms: Public domain W3C validator