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

Theorem elrpd 12421
Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
elrpd.1 (𝜑𝐴 ∈ ℝ)
elrpd.2 (𝜑 → 0 < 𝐴)
Assertion
Ref Expression
elrpd (𝜑𝐴 ∈ ℝ+)

Proof of Theorem elrpd
StepHypRef Expression
1 elrpd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 elrpd.2 . 2 (𝜑 → 0 < 𝐴)
3 elrp 12384 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 586 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115   class class class wbr 5052  cr 10528  0cc0 10529   < clt 10667  +crp 12382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3142  df-v 3482  df-un 3924  df-sn 4550  df-pr 4552  df-op 4556  df-br 5053  df-rp 12383
This theorem is referenced by:  mul2lt0rgt0  12485  mul2lt0bi  12488  xov1plusxeqvd  12881  zltaddlt1le  12888  sqn0rp  13493  ltexp2a  13531  expcan  13534  ltexp2  13535  leexp2a  13537  expnlbnd2  13596  discr  13602  sqrlem4  14601  sqrlem7  14604  rpsqrtcl  14620  absrpcl  14644  mulcn2  14948  fprodle  15346  rprisefaccl  15373  rpefcl  15453  eflt  15466  ef01bndlem  15533  stdbdmopn  23121  methaus  23123  nmrpcl  23222  nlmvscnlem1  23288  metnrmlem1a  23459  icopnfcnv  23543  evth  23560  lebnumlem1  23562  nmoleub2lem3  23716  ipcnlem1  23845  minveclem4  24032  pjthlem1  24037  vitalilem4  24211  mbfmulc2lem  24247  itg2gt0  24360  dveflem  24578  dvferm1lem  24583  dvferm2  24586  aaliou3lem3  24936  psercnlem1  25016  pserdvlem1  25018  pserdv  25020  reeff1olem  25037  pilem2  25043  pilem3  25044  tanrpcl  25093  cosordlem  25118  rplogcl  25191  logdivlti  25207  logdivlt  25208  logdivle  25209  recxpcl  25262  rpcxpcl  25263  mulcxp  25272  cxple2  25284  cxpsqrt  25290  cxpcn3  25333  loglesqrt  25343  atanlogaddlem  25495  atantan  25505  atanbnd  25508  rlimcnp  25547  rlimcnp2  25548  efrlim  25551  cxp2limlem  25557  cxp2lim  25558  cxploglim2  25560  jensen  25570  harmonicubnd  25591  fsumharmonic  25593  lgamgulmlem2  25611  ftalem2  25655  basellem3  25664  basellem8  25669  chtrpcl  25756  fsumvma2  25794  chpval2  25798  chpchtsum  25799  chpub  25800  efexple  25861  chebbnd1lem2  26050  chebbnd1lem3  26051  chebbnd1  26052  chtppilimlem1  26053  chtppilimlem2  26054  chtppilim  26055  chebbnd2  26057  chto1lb  26058  chpchtlim  26059  chpo1ub  26060  rplogsumlem2  26065  dchrisumlema  26068  dchrisumlem3  26071  dchrvmasumlem2  26078  dchrvmasumiflem1  26081  dchrisum0lema  26094  chpdifbndlem1  26133  chpdifbndlem2  26134  chpdifbnd  26135  selberg3lem1  26137  pntrsumo1  26145  pntpbnd1a  26165  pntpbnd1  26166  pntpbnd2  26167  pntpbnd  26168  pntibndlem2  26171  pntibndlem3  26172  pntibnd  26173  pntlemd  26174  pntlem3  26189  pntleml  26191  pnt2  26193  pnt  26194  abvcxp  26195  ostth2lem1  26198  padicabv  26210  ostth2lem3  26215  ostth2lem4  26216  ostth2  26217  ostth3  26218  ttgcontlem1  26675  blocnilem  28583  minvecolem4  28659  minvecolem5  28660  pjhthlem1  29170  eigposi  29615  xrge0iifhom  31205  cndprobprob  31721  hgt750lem  31947  unblimceq0lem  33870  unblimceq0  33871  knoppndvlem14  33889  knoppndvlem18  33893  knoppndvlem20  33895  tan2h  34959  mblfinlem3  35006  mblfinlem4  35007  itg2addnclem  35018  itg2gt0cn  35022  ftc1anclem7  35046  ftc1anc  35048  dvasin  35051  areacirclem1  35055  areacirclem4  35058  areacirc  35060  geomcau  35107  blbnd  35135  prdsbnd2  35143  rrnequiv  35183  relogbcld  39169  logblebd  39172  3lexlogpow5ineq2  39248  pell14qrrp  39654  pellfundex  39680  pellfundrp  39682  rmspecfund  39703  rmspecpos  39710  areaquad  40019  wwlemuld  40715  radcnvrat  40875  binomcxplemdvbinom  40914  binomcxplemnotnn0  40917  supxrgere  41828  supxrgelem  41832  xralrple2  41849  xralrple3  41869  sqrlearg  42053  sinaover2ne0  42373  ioodvbdlimc1lem1  42436  ioodvbdlimc1lem2  42437  ioodvbdlimc2lem  42439  dvnmul  42448  stoweidlem25  42530  stoweidlem28  42533  stoweidlem42  42547  stoweidlem49  42554  wallispilem3  42572  wallispilem4  42573  wallispi  42575  wallispi2lem1  42576  stirlinglem5  42583  stirlinglem10  42588  fourierdlem4  42616  fourierdlem6  42618  fourierdlem7  42619  fourierdlem19  42631  fourierdlem24  42636  fourierdlem26  42638  fourierdlem30  42642  fourierdlem42  42654  fourierdlem51  42662  fourierdlem63  42674  fourierdlem64  42675  fourierdlem65  42676  fourierdlem73  42684  fourierdlem75  42686  fourierdlem79  42690  fourierdlem92  42703  fourierdlem109  42720  fouriersw  42736  etransclem35  42774  qndenserrnbllem  42799  ioorrnopnlem  42809  hoiqssbllem1  43124  hoiqssbllem2  43125  iunhoiioolem  43177  pimrecltpos  43207  smfrec  43284  smfmullem1  43286  smfmullem2  43287  smfmullem3  43288  m1mod0mod1  43749  rege1logbrege0  44834  fldivexpfllog2  44841  fllog2  44844  resum2sqrp  44973  eenglngeehlnmlem2  45003  itschlc0xyqsol1  45031  inlinecirc02plem  45051  amgmwlem  45181
  Copyright terms: Public domain W3C validator