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

Theorem elrpd 11174
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 11141 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 662 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   class class class wbr 4367   RRcr 9402   0cc0 9403    < clt 9539   RR+crp 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-rp 11140
This theorem is referenced by:  xov1plusxeqvd  11587  ltexp2a  12120  expcan  12121  ltexp2  12122  leexp2a  12124  expnlbnd2  12199  discr  12205  sqrlem4  13081  sqrlem7  13084  rpsqrtcl  13100  absrpcl  13123  rlimrege0  13404  mulcn2  13420  rpefcl  13841  eflt  13854  ef01bndlem  13921  stdbdmopn  21106  methaus  21108  nmrpcl  21224  nlmvscnlem1  21280  metnrmlem1a  21447  icopnfcnv  21527  evth  21544  lebnumlem1  21546  nmoleub2lem3  21683  ipcnlem1  21770  minveclem4  21932  vitalilem4  22105  mbfmulc2lem  22139  itg2gt0  22252  dveflem  22465  dvferm1lem  22470  dvferm2  22473  aaliou3lem3  22825  psercnlem1  22905  pserdvlem1  22907  pserdv  22909  reeff1olem  22926  pilem2  22932  pilem3  22933  tanrpcl  22982  cosordlem  23003  rplogcl  23076  logdivlti  23092  logdivlt  23093  logdivle  23094  dvloglem  23116  recxpcl  23143  rpcxpcl  23144  mulcxp  23153  cxple2  23165  cxpsqrt  23171  cxpcn3  23209  loglesqrt  23219  atanlogaddlem  23360  atantan  23370  atanbnd  23373  rlimcnp  23412  rlimcnp2  23413  efrlim  23416  cxp2limlem  23422  cxp2lim  23423  cxploglim2  23425  jensen  23435  harmonicubnd  23456  fsumharmonic  23458  ftalem2  23464  basellem3  23473  basellem8  23478  chtrpcl  23566  fsumvma2  23606  chpval2  23610  chpchtsum  23611  chpub  23612  efexple  23673  chebbnd1lem2  23772  chebbnd1lem3  23773  chebbnd1  23774  chtppilimlem1  23775  chtppilimlem2  23776  chtppilim  23777  chebbnd2  23779  chto1lb  23780  chpchtlim  23781  chpo1ub  23782  rplogsumlem2  23787  dchrisumlema  23790  dchrisumlem3  23793  dchrvmasumlem2  23800  dchrvmasumiflem1  23803  dchrisum0lema  23816  chpdifbndlem1  23855  chpdifbndlem2  23856  chpdifbnd  23857  selberg3lem1  23859  pntrsumo1  23867  pntpbnd1a  23887  pntpbnd1  23888  pntpbnd2  23889  pntpbnd  23890  pntibndlem2  23893  pntibndlem3  23894  pntibnd  23895  pntlemd  23896  pntlem3  23911  pntleml  23913  pnt2  23915  pnt  23916  abvcxp  23917  ostth2lem1  23920  padicabv  23932  ostth2lem3  23937  ostth2lem4  23938  ostth2  23939  ostth3  23940  ttgcontlem1  24309  blocnilem  25836  minvecolem4  25913  minvecolem5  25914  mul2lt0rgt0  27716  mul2lt0bi  27719  xrge0iifhom  28073  cndprobprob  28560  lgamgulmlem2  28761  rprisefaccl  29311  tan2h  30212  mblfinlem3  30218  mblfinlem4  30219  itg2addnclem  30232  itg2gt0cn  30236  ftc1anclem7  30262  ftc1anc  30264  dvasin  30269  areacirclem1  30273  areacirclem4  30276  areacirc  30278  geomcau  30418  blbnd  30449  prdsbnd2  30457  rrnequiv  30497  pell14qrrp  30961  pellfundex  30987  pellfundrp  30989  rmspecfund  31010  rmspecpos  31017  areaquad  31352  radcnvrat  31363  binomcxplemdvbinom  31426  binomcxplemnotnn0  31429  fprodle  31770  sinaover2ne0  31834  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnmul  31906  stoweidlem25  31973  stoweidlem28  31976  stoweidlem42  31990  stoweidlem49  31997  wallispilem3  32015  wallispilem4  32016  wallispi  32018  wallispi2lem1  32019  stirlinglem5  32026  stirlinglem10  32031  fourierdlem4  32059  fourierdlem6  32061  fourierdlem7  32062  fourierdlem19  32074  fourierdlem24  32079  fourierdlem26  32081  fourierdlem30  32085  fourierdlem42  32097  fourierdlem51  32106  fourierdlem63  32118  fourierdlem64  32119  fourierdlem65  32120  fourierdlem73  32128  fourierdlem75  32130  fourierdlem79  32134  fourierdlem92  32147  fourierdlem109  32164  fouriersw  32180  etransclem35  32218  m1mod0mod1  32460  rege1logbrege0  33379  fldivexpfllog2  33386  fllog2  33389  wwlemuld  38497
  Copyright terms: Public domain W3C validator