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

Theorem elrpd 12062
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 12027 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 701 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139   class class class wbr 4804  cr 10127  0cc0 10128   < clt 10266  +crp 12025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-rp 12026
This theorem is referenced by:  mul2lt0rgt0  12126  mul2lt0bi  12129  xov1plusxeqvd  12511  zltaddlt1le  12517  ltexp2a  13106  expcan  13107  ltexp2  13108  leexp2a  13110  expnlbnd2  13189  discr  13195  sqrlem4  14185  sqrlem7  14188  rpsqrtcl  14204  absrpcl  14227  rlimrege0  14509  mulcn2  14525  fprodle  14926  rprisefaccl  14953  rpefcl  15033  eflt  15046  ef01bndlem  15113  stdbdmopn  22524  methaus  22526  nmrpcl  22625  nlmvscnlem1  22691  metnrmlem1a  22862  icopnfcnv  22942  evth  22959  lebnumlem1  22961  nmoleub2lem3  23115  ipcnlem1  23244  minveclem4  23403  vitalilem4  23579  mbfmulc2lem  23613  itg2gt0  23726  dveflem  23941  dvferm1lem  23946  dvferm2  23949  aaliou3lem3  24298  psercnlem1  24378  pserdvlem1  24380  pserdv  24382  reeff1olem  24399  pilem2  24405  pilem3  24406  tanrpcl  24455  cosordlem  24476  rplogcl  24549  logdivlti  24565  logdivlt  24566  logdivle  24567  dvloglem  24593  recxpcl  24620  rpcxpcl  24621  mulcxp  24630  cxple2  24642  cxpsqrt  24648  cxpcn3  24688  loglesqrt  24698  atanlogaddlem  24839  atantan  24849  atanbnd  24852  rlimcnp  24891  rlimcnp2  24892  efrlim  24895  cxp2limlem  24901  cxp2lim  24902  cxploglim2  24904  jensen  24914  harmonicubnd  24935  fsumharmonic  24937  lgamgulmlem2  24955  ftalem2  24999  basellem3  25008  basellem8  25013  chtrpcl  25100  fsumvma2  25138  chpval2  25142  chpchtsum  25143  chpub  25144  efexple  25205  chebbnd1lem2  25358  chebbnd1lem3  25359  chebbnd1  25360  chtppilimlem1  25361  chtppilimlem2  25362  chtppilim  25363  chebbnd2  25365  chto1lb  25366  chpchtlim  25367  chpo1ub  25368  rplogsumlem2  25373  dchrisumlema  25376  dchrisumlem3  25379  dchrvmasumlem2  25386  dchrvmasumiflem1  25389  dchrisum0lema  25402  chpdifbndlem1  25441  chpdifbndlem2  25442  chpdifbnd  25443  selberg3lem1  25445  pntrsumo1  25453  pntpbnd1a  25473  pntpbnd1  25474  pntpbnd2  25475  pntpbnd  25476  pntibndlem2  25479  pntibndlem3  25480  pntibnd  25481  pntlemd  25482  pntlem3  25497  pntleml  25499  pnt2  25501  pnt  25502  abvcxp  25503  ostth2lem1  25506  padicabv  25518  ostth2lem3  25523  ostth2lem4  25524  ostth2  25525  ostth3  25526  ttgcontlem1  25964  blocnilem  27968  minvecolem4  28045  minvecolem5  28046  xrge0iifhom  30292  cndprobprob  30809  hgt750lem  31038  unblimceq0lem  32803  unblimceq0  32804  knoppndvlem14  32822  knoppndvlem18  32826  knoppndvlem20  32828  tan2h  33714  mblfinlem3  33761  mblfinlem4  33762  itg2addnclem  33774  itg2gt0cn  33778  ftc1anclem7  33804  ftc1anc  33806  dvasin  33809  areacirclem1  33813  areacirclem4  33816  areacirc  33818  geomcau  33868  blbnd  33899  prdsbnd2  33907  rrnequiv  33947  pell14qrrp  37926  pellfundex  37952  pellfundrp  37954  rmspecfund  37976  rmspecpos  37983  areaquad  38304  wwlemuld  38956  radcnvrat  39015  binomcxplemdvbinom  39054  binomcxplemnotnn0  39057  supxrgere  40047  supxrgelem  40051  xralrple2  40068  xralrple3  40088  sqrlearg  40283  sinaover2ne0  40582  ioodvbdlimc1lem1  40649  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnmul  40661  stoweidlem25  40745  stoweidlem28  40748  stoweidlem42  40762  stoweidlem49  40769  wallispilem3  40787  wallispilem4  40788  wallispi  40790  wallispi2lem1  40791  stirlinglem5  40798  stirlinglem10  40803  fourierdlem4  40831  fourierdlem6  40833  fourierdlem7  40834  fourierdlem19  40846  fourierdlem24  40851  fourierdlem26  40853  fourierdlem30  40857  fourierdlem42  40869  fourierdlem51  40877  fourierdlem63  40889  fourierdlem64  40890  fourierdlem65  40891  fourierdlem73  40899  fourierdlem75  40901  fourierdlem79  40905  fourierdlem92  40918  fourierdlem109  40935  fouriersw  40951  etransclem35  40989  qndenserrnbllem  41017  ioorrnopnlem  41027  hoiqssbllem1  41342  hoiqssbllem2  41343  iunhoiioolem  41395  pimrecltpos  41425  smfrec  41502  smfmullem1  41504  smfmullem2  41505  smfmullem3  41506  m1mod0mod1  41849  rege1logbrege0  42862  fldivexpfllog2  42869  fllog2  42872  amgmwlem  43061
  Copyright terms: Public domain W3C validator