Theorem elrpd 12999

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

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		elrpd.2	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		elrp 12960	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075   < clt 11215  ℝ⁺crp 12958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-rp 12959

This theorem is referenced by:  mul2lt0rgt0  13063  mul2lt0bi  13066  xov1plusxeqvd  13466  zltaddlt1le  13473  sqn0rp  14099  ltexp2a  14138  expcan  14141  ltexp2  14142  leexp2a  14144  expnlbnd2  14206  discr  14212  01sqrexlem4  15218  01sqrexlem7  15221  rpsqrtcl  15237  absrpcl  15261  mulcn2  15569  fprodle  15969  rprisefaccl  15996  rpefcl  16079  eflt  16092  ef01bndlem  16159  stdbdmopn  24413  methaus  24415  nmrpcl  24515  nlmvscnlem1  24581  metnrmlem1a  24754  icopnfcnv  24847  evth  24865  lebnumlem1  24867  nmoleub2lem3  25022  ipcnlem1  25152  minveclem4  25339  pjthlem1  25344  vitalilem4  25519  mbfmulc2lem  25555  itg2gt0  25668  dveflem  25890  dvferm1lem  25895  dvferm2  25898  aaliou3lem3  26259  psercnlem1  26342  pserdvlem1  26344  pserdv  26346  reeff1olem  26363  pilem2  26369  pilem3  26370  tanrpcl  26420  cosordlem  26446  rplogcl  26520  logdivlti  26536  logdivlt  26537  logdivle  26538  recxpcl  26591  rpcxpcl  26592  mulcxp  26601  cxple2  26613  cxpsqrt  26619  cxpcn3  26665  loglesqrt  26678  atanlogaddlem  26830  atantan  26840  atanbnd  26843  rlimcnp  26882  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  cxp2limlem  26893  cxp2lim  26894  cxploglim2  26896  jensen  26906  harmonicubnd  26927  fsumharmonic  26929  lgamgulmlem2  26947  ftalem2  26991  basellem3  27000  basellem8  27005  chtrpcl  27092  fsumvma2  27132  chpval2  27136  chpchtsum  27137  chpub  27138  efexple  27199  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  chtppilimlem2  27392  chtppilim  27393  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ub  27398  rplogsumlem2  27403  dchrisumlema  27406  dchrisumlem3  27409  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0lema  27432  chpdifbndlem1  27471  chpdifbndlem2  27472  chpdifbnd  27473  selberg3lem1  27475  pntrsumo1  27483  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntpbnd  27506  pntibndlem2  27509  pntibndlem3  27510  pntibnd  27511  pntlemd  27512  pntlem3  27527  pntleml  27529  pnt2  27531  pnt  27532  abvcxp  27533  ostth2lem1  27536  padicabv  27548  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  ostth3  27556  ttgcontlem1  28819  blocnilem  30740  minvecolem4  30816  minvecolem5  30817  pjhthlem1  31327  eigposi  31772  2sqr3minply  33777  xrge0iifhom  33934  cndprobprob  34436  hgt750lem  34649  unblimceq0lem  36501  unblimceq0  36502  knoppndvlem14  36520  knoppndvlem18  36524  knoppndvlem20  36526  tan2h  37613  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anc  37702  dvasin  37705  areacirclem1  37709  areacirclem4  37712  areacirc  37714  geomcau  37760  blbnd  37788  prdsbnd2  37796  rrnequiv  37836  relogbcld  41968  logblebd  41971  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks6d1c7lem1  42175  explt1d  42318  expeq1d  42319  pell14qrrp  42855  pellfundex  42881  pellfundrp  42883  rmspecfund  42904  rmspecpos  42912  areaquad  43212  wwlemuld  44152  radcnvrat  44310  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  supxrgere  45336  supxrgelem  45340  xralrple2  45357  xralrple3  45377  sqrlearg  45558  sinaover2ne0  45873  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  stoweidlem25  46030  stoweidlem28  46033  stoweidlem42  46047  stoweidlem49  46054  wallispilem3  46072  wallispilem4  46073  wallispi  46075  wallispi2lem1  46076  stirlinglem5  46083  stirlinglem10  46088  fourierdlem4  46116  fourierdlem6  46118  fourierdlem7  46119  fourierdlem19  46131  fourierdlem24  46136  fourierdlem26  46138  fourierdlem30  46142  fourierdlem42  46154  fourierdlem51  46162  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem73  46184  fourierdlem75  46186  fourierdlem79  46190  fourierdlem92  46203  fourierdlem109  46220  fouriersw  46236  etransclem35  46274  qndenserrnbllem  46299  ioorrnopnlem  46309  hoiqssbllem1  46627  hoiqssbllem2  46628  iunhoiioolem  46680  pimrecltpos  46713  smfrec  46794  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  m1mod0mod1  47359  rege1logbrege0  48551  fldivexpfllog2  48558  fllog2  48561  resum2sqrp  48701  eenglngeehlnmlem2  48731  itschlc0xyqsol1  48759  inlinecirc02plem  48779  amgmwlem  49795