Theorem elrpd 13074

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 13036	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  0cc0 11155   < clt 11295  ℝ⁺crp 13034

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-rp 13035

This theorem is referenced by:  mul2lt0rgt0  13138  mul2lt0bi  13141  xov1plusxeqvd  13538  zltaddlt1le  13545  sqn0rp  14167  ltexp2a  14206  expcan  14209  ltexp2  14210  leexp2a  14212  expnlbnd2  14273  discr  14279  01sqrexlem4  15284  01sqrexlem7  15287  rpsqrtcl  15303  absrpcl  15327  mulcn2  15632  fprodle  16032  rprisefaccl  16059  rpefcl  16140  eflt  16153  ef01bndlem  16220  stdbdmopn  24531  methaus  24533  nmrpcl  24633  nlmvscnlem1  24707  metnrmlem1a  24880  icopnfcnv  24973  evth  24991  lebnumlem1  24993  nmoleub2lem3  25148  ipcnlem1  25279  minveclem4  25466  pjthlem1  25471  vitalilem4  25646  mbfmulc2lem  25682  itg2gt0  25795  dveflem  26017  dvferm1lem  26022  dvferm2  26025  aaliou3lem3  26386  psercnlem1  26469  pserdvlem1  26471  pserdv  26473  reeff1olem  26490  pilem2  26496  pilem3  26497  tanrpcl  26546  cosordlem  26572  rplogcl  26646  logdivlti  26662  logdivlt  26663  logdivle  26664  recxpcl  26717  rpcxpcl  26718  mulcxp  26727  cxple2  26739  cxpsqrt  26745  cxpcn3  26791  loglesqrt  26804  atanlogaddlem  26956  atantan  26966  atanbnd  26969  rlimcnp  27008  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  cxp2limlem  27019  cxp2lim  27020  cxploglim2  27022  jensen  27032  harmonicubnd  27053  fsumharmonic  27055  lgamgulmlem2  27073  ftalem2  27117  basellem3  27126  basellem8  27131  chtrpcl  27218  fsumvma2  27258  chpval2  27262  chpchtsum  27263  chpub  27264  efexple  27325  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  rplogsumlem2  27529  dchrisumlema  27532  dchrisumlem3  27535  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0lema  27558  chpdifbndlem1  27597  chpdifbndlem2  27598  chpdifbnd  27599  selberg3lem1  27601  pntrsumo1  27609  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntpbnd  27632  pntibndlem2  27635  pntibndlem3  27636  pntibnd  27637  pntlemd  27638  pntlem3  27653  pntleml  27655  pnt2  27657  pnt  27658  abvcxp  27659  ostth2lem1  27662  padicabv  27674  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  ttgcontlem1  28899  blocnilem  30823  minvecolem4  30899  minvecolem5  30900  pjhthlem1  31410  eigposi  31855  2sqr3minply  33791  xrge0iifhom  33936  cndprobprob  34440  hgt750lem  34666  unblimceq0lem  36507  unblimceq0  36508  knoppndvlem14  36526  knoppndvlem18  36530  knoppndvlem20  36532  tan2h  37619  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2gt0cn  37682  ftc1anclem7  37706  ftc1anc  37708  dvasin  37711  areacirclem1  37715  areacirclem4  37718  areacirc  37720  geomcau  37766  blbnd  37794  prdsbnd2  37802  rrnequiv  37842  relogbcld  41974  logblebd  41977  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks6d1c7lem1  42181  metakunt29  42234  explt1d  42358  expeq1d  42359  pell14qrrp  42871  pellfundex  42897  pellfundrp  42899  rmspecfund  42920  rmspecpos  42928  areaquad  43228  wwlemuld  44169  radcnvrat  44333  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  supxrgere  45344  supxrgelem  45348  xralrple2  45365  xralrple3  45385  sqrlearg  45566  sinaover2ne0  45883  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  stoweidlem25  46040  stoweidlem28  46043  stoweidlem42  46057  stoweidlem49  46064  wallispilem3  46082  wallispilem4  46083  wallispi  46085  wallispi2lem1  46086  stirlinglem5  46093  stirlinglem10  46098  fourierdlem4  46126  fourierdlem6  46128  fourierdlem7  46129  fourierdlem19  46141  fourierdlem24  46146  fourierdlem26  46148  fourierdlem30  46152  fourierdlem42  46164  fourierdlem51  46172  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem73  46194  fourierdlem75  46196  fourierdlem79  46200  fourierdlem92  46213  fourierdlem109  46230  fouriersw  46246  etransclem35  46284  qndenserrnbllem  46309  ioorrnopnlem  46319  hoiqssbllem1  46637  hoiqssbllem2  46638  iunhoiioolem  46690  pimrecltpos  46723  smfrec  46804  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  m1mod0mod1  47356  rege1logbrege0  48479  fldivexpfllog2  48486  fllog2  48489  resum2sqrp  48629  eenglngeehlnmlem2  48659  itschlc0xyqsol1  48687  inlinecirc02plem  48707  amgmwlem  49321