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

Theorem elrpd 12955
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 12918 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 584 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  cr 11051  0cc0 11052   < clt 11190  +crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-rp 12917
This theorem is referenced by:  mul2lt0rgt0  13019  mul2lt0bi  13022  xov1plusxeqvd  13416  zltaddlt1le  13423  sqn0rp  14033  ltexp2a  14072  expcan  14075  ltexp2  14076  leexp2a  14078  expnlbnd2  14138  discr  14144  01sqrexlem4  15131  01sqrexlem7  15134  rpsqrtcl  15150  absrpcl  15174  mulcn2  15479  fprodle  15880  rprisefaccl  15907  rpefcl  15987  eflt  16000  ef01bndlem  16067  stdbdmopn  23877  methaus  23879  nmrpcl  23979  nlmvscnlem1  24053  metnrmlem1a  24224  icopnfcnv  24308  evth  24325  lebnumlem1  24327  nmoleub2lem3  24481  ipcnlem1  24612  minveclem4  24799  pjthlem1  24804  vitalilem4  24978  mbfmulc2lem  25014  itg2gt0  25128  dveflem  25346  dvferm1lem  25351  dvferm2  25354  aaliou3lem3  25707  psercnlem1  25787  pserdvlem1  25789  pserdv  25791  reeff1olem  25808  pilem2  25814  pilem3  25815  tanrpcl  25864  cosordlem  25889  rplogcl  25962  logdivlti  25978  logdivlt  25979  logdivle  25980  recxpcl  26033  rpcxpcl  26034  mulcxp  26043  cxple2  26055  cxpsqrt  26061  cxpcn3  26104  loglesqrt  26114  atanlogaddlem  26266  atantan  26276  atanbnd  26279  rlimcnp  26318  rlimcnp2  26319  efrlim  26322  cxp2limlem  26328  cxp2lim  26329  cxploglim2  26331  jensen  26341  harmonicubnd  26362  fsumharmonic  26364  lgamgulmlem2  26382  ftalem2  26426  basellem3  26435  basellem8  26440  chtrpcl  26527  fsumvma2  26565  chpval2  26569  chpchtsum  26570  chpub  26571  efexple  26632  chebbnd1lem2  26821  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  chtppilimlem2  26825  chtppilim  26826  chebbnd2  26828  chto1lb  26829  chpchtlim  26830  chpo1ub  26831  rplogsumlem2  26836  dchrisumlema  26839  dchrisumlem3  26842  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  dchrisum0lema  26865  chpdifbndlem1  26904  chpdifbndlem2  26905  chpdifbnd  26906  selberg3lem1  26908  pntrsumo1  26916  pntpbnd1a  26936  pntpbnd1  26937  pntpbnd2  26938  pntpbnd  26939  pntibndlem2  26942  pntibndlem3  26943  pntibnd  26944  pntlemd  26945  pntlem3  26960  pntleml  26962  pnt2  26964  pnt  26965  abvcxp  26966  ostth2lem1  26969  padicabv  26981  ostth2lem3  26986  ostth2lem4  26987  ostth2  26988  ostth3  26989  ttgcontlem1  27836  blocnilem  29749  minvecolem4  29825  minvecolem5  29826  pjhthlem1  30336  eigposi  30781  xrge0iifhom  32521  cndprobprob  33041  hgt750lem  33267  unblimceq0lem  34972  unblimceq0  34973  knoppndvlem14  34991  knoppndvlem18  34995  knoppndvlem20  34997  tan2h  36073  mblfinlem3  36120  mblfinlem4  36121  itg2addnclem  36132  itg2gt0cn  36136  ftc1anclem7  36160  ftc1anc  36162  dvasin  36165  areacirclem1  36169  areacirclem4  36172  areacirc  36174  geomcau  36221  blbnd  36249  prdsbnd2  36257  rrnequiv  36297  relogbcld  40433  logblebd  40436  3lexlogpow5ineq2  40515  3lexlogpow2ineq1  40518  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  metakunt29  40608  pell14qrrp  41186  pellfundex  41212  pellfundrp  41214  rmspecfund  41235  rmspecpos  41243  areaquad  41553  wwlemuld  42435  radcnvrat  42601  binomcxplemdvbinom  42640  binomcxplemnotnn0  42643  supxrgere  43574  supxrgelem  43578  xralrple2  43595  xralrple3  43615  sqrlearg  43798  sinaover2ne0  44116  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnmul  44191  stoweidlem25  44273  stoweidlem28  44276  stoweidlem42  44290  stoweidlem49  44297  wallispilem3  44315  wallispilem4  44316  wallispi  44318  wallispi2lem1  44319  stirlinglem5  44326  stirlinglem10  44331  fourierdlem4  44359  fourierdlem6  44361  fourierdlem7  44362  fourierdlem19  44374  fourierdlem24  44379  fourierdlem26  44381  fourierdlem30  44385  fourierdlem42  44397  fourierdlem51  44405  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem73  44427  fourierdlem75  44429  fourierdlem79  44433  fourierdlem92  44446  fourierdlem109  44463  fouriersw  44479  etransclem35  44517  qndenserrnbllem  44542  ioorrnopnlem  44552  hoiqssbllem1  44870  hoiqssbllem2  44871  iunhoiioolem  44923  pimrecltpos  44956  smfrec  45037  smfmullem1  45039  smfmullem2  45040  smfmullem3  45041  m1mod0mod1  45568  rege1logbrege0  46651  fldivexpfllog2  46658  fllog2  46661  resum2sqrp  46801  eenglngeehlnmlem2  46831  itschlc0xyqsol1  46859  inlinecirc02plem  46879  amgmwlem  47256
  Copyright terms: Public domain W3C validator