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

Theorem elrpd 12111
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 12073 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 579 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157   class class class wbr 4842  cr 10222  0cc0 10223   < clt 10362  +crp 12071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843  df-rp 12072
This theorem is referenced by:  mul2lt0rgt0  12175  mul2lt0bi  12178  xov1plusxeqvd  12569  zltaddlt1le  12575  ltexp2a  13163  expcan  13164  ltexp2  13165  leexp2a  13167  expnlbnd2  13246  discr  13252  sqrlem4  14324  sqrlem7  14327  rpsqrtcl  14343  absrpcl  14366  rlimrege0  14648  mulcn2  14664  fprodle  15060  rprisefaccl  15087  rpefcl  15167  eflt  15180  ef01bndlem  15247  stdbdmopn  22648  methaus  22650  nmrpcl  22749  nlmvscnlem1  22815  metnrmlem1a  22986  icopnfcnv  23066  evth  23083  lebnumlem1  23085  nmoleub2lem3  23239  ipcnlem1  23368  minveclem4  23539  pjthlem1  23544  vitalilem4  23716  mbfmulc2lem  23752  itg2gt0  23865  dveflem  24080  dvferm1lem  24085  dvferm2  24088  aaliou3lem3  24437  psercnlem1  24517  pserdvlem1  24519  pserdv  24521  reeff1olem  24538  pilem2  24544  pilem3  24545  pilem3OLD  24546  tanrpcl  24595  cosordlem  24616  rplogcl  24688  logdivlti  24704  logdivlt  24705  logdivle  24706  dvloglem  24732  recxpcl  24759  rpcxpcl  24760  mulcxp  24769  cxple2  24781  cxpsqrt  24787  cxpcn3  24830  loglesqrt  24840  atanlogaddlem  24989  atantan  24999  atanbnd  25002  rlimcnp  25041  rlimcnp2  25042  efrlim  25045  cxp2limlem  25051  cxp2lim  25052  cxploglim2  25054  jensen  25064  harmonicubnd  25085  fsumharmonic  25087  lgamgulmlem2  25105  ftalem2  25149  basellem3  25158  basellem8  25163  chtrpcl  25250  fsumvma2  25288  chpval2  25292  chpchtsum  25293  chpub  25294  efexple  25355  chebbnd1lem2  25508  chebbnd1lem3  25509  chebbnd1  25510  chtppilimlem1  25511  chtppilimlem2  25512  chtppilim  25513  chebbnd2  25515  chto1lb  25516  chpchtlim  25517  chpo1ub  25518  rplogsumlem2  25523  dchrisumlema  25526  dchrisumlem3  25529  dchrvmasumlem2  25536  dchrvmasumiflem1  25539  dchrisum0lema  25552  chpdifbndlem1  25591  chpdifbndlem2  25592  chpdifbnd  25593  selberg3lem1  25595  pntrsumo1  25603  pntpbnd1a  25623  pntpbnd1  25624  pntpbnd2  25625  pntpbnd  25626  pntibndlem2  25629  pntibndlem3  25630  pntibnd  25631  pntlemd  25632  pntlem3  25647  pntleml  25649  pnt2  25651  pnt  25652  abvcxp  25653  ostth2lem1  25656  padicabv  25668  ostth2lem3  25673  ostth2lem4  25674  ostth2  25675  ostth3  25676  ttgcontlem1  26115  blocnilem  28177  minvecolem4  28254  minvecolem5  28255  pjhthlem1  28768  eigposi  29213  xrge0iifhom  30492  cndprobprob  31010  hgt750lem  31242  unblimceq0lem  32998  unblimceq0  32999  knoppndvlem14  33017  knoppndvlem18  33021  knoppndvlem20  33023  tan2h  33883  mblfinlem3  33930  mblfinlem4  33931  itg2addnclem  33942  itg2gt0cn  33946  ftc1anclem7  33972  ftc1anc  33974  dvasin  33977  areacirclem1  33981  areacirclem4  33984  areacirc  33986  geomcau  34035  blbnd  34066  prdsbnd2  34074  rrnequiv  34114  pell14qrrp  38199  pellfundex  38225  pellfundrp  38227  rmspecfund  38248  rmspecpos  38255  areaquad  38575  wwlemuld  39225  radcnvrat  39284  binomcxplemdvbinom  39323  binomcxplemnotnn0  39326  supxrgere  40282  supxrgelem  40286  xralrple2  40303  xralrple3  40323  sqrlearg  40513  sinaover2ne0  40812  ioodvbdlimc1lem1  40879  ioodvbdlimc1lem2  40880  ioodvbdlimc2lem  40882  dvnmul  40891  stoweidlem25  40974  stoweidlem28  40977  stoweidlem42  40991  stoweidlem49  40998  wallispilem3  41016  wallispilem4  41017  wallispi  41019  wallispi2lem1  41020  stirlinglem5  41027  stirlinglem10  41032  fourierdlem4  41060  fourierdlem6  41062  fourierdlem7  41063  fourierdlem19  41075  fourierdlem24  41080  fourierdlem26  41082  fourierdlem30  41086  fourierdlem42  41098  fourierdlem51  41106  fourierdlem63  41118  fourierdlem64  41119  fourierdlem65  41120  fourierdlem73  41128  fourierdlem75  41130  fourierdlem79  41134  fourierdlem92  41147  fourierdlem109  41164  fouriersw  41180  etransclem35  41218  qndenserrnbllem  41246  ioorrnopnlem  41256  hoiqssbllem1  41571  hoiqssbllem2  41572  iunhoiioolem  41624  pimrecltpos  41654  smfrec  41731  smfmullem1  41733  smfmullem2  41734  smfmullem3  41735  m1mod0mod1  42168  rege1logbrege0  43140  fldivexpfllog2  43147  fllog2  43150  amgmwlem  43339
  Copyright terms: Public domain W3C validator