Theorem elrpd 13013

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

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 2704

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 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  mul2lt0rgt0  13077  mul2lt0bi  13080  xov1plusxeqvd  13475  zltaddlt1le  13482  sqn0rp  14092  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2a  14137  expnlbnd2  14197  discr  14203  01sqrexlem4  15192  01sqrexlem7  15195  rpsqrtcl  15211  absrpcl  15235  mulcn2  15540  fprodle  15940  rprisefaccl  15967  rpefcl  16047  eflt  16060  ef01bndlem  16127  stdbdmopn  24027  methaus  24029  nmrpcl  24129  nlmvscnlem1  24203  metnrmlem1a  24374  icopnfcnv  24458  evth  24475  lebnumlem1  24477  nmoleub2lem3  24631  ipcnlem1  24762  minveclem4  24949  pjthlem1  24954  vitalilem4  25128  mbfmulc2lem  25164  itg2gt0  25278  dveflem  25496  dvferm1lem  25501  dvferm2  25504  aaliou3lem3  25857  psercnlem1  25937  pserdvlem1  25939  pserdv  25941  reeff1olem  25958  pilem2  25964  pilem3  25965  tanrpcl  26014  cosordlem  26039  rplogcl  26112  logdivlti  26128  logdivlt  26129  logdivle  26130  recxpcl  26183  rpcxpcl  26184  mulcxp  26193  cxple2  26205  cxpsqrt  26211  cxpcn3  26256  loglesqrt  26266  atanlogaddlem  26418  atantan  26428  atanbnd  26431  rlimcnp  26470  rlimcnp2  26471  efrlim  26474  cxp2limlem  26480  cxp2lim  26481  cxploglim2  26483  jensen  26493  harmonicubnd  26514  fsumharmonic  26516  lgamgulmlem2  26534  ftalem2  26578  basellem3  26587  basellem8  26592  chtrpcl  26679  fsumvma2  26717  chpval2  26721  chpchtsum  26722  chpub  26723  efexple  26784  chebbnd1lem2  26973  chebbnd1lem3  26974  chebbnd1  26975  chtppilimlem1  26976  chtppilimlem2  26977  chtppilim  26978  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  rplogsumlem2  26988  dchrisumlema  26991  dchrisumlem3  26994  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0lema  27017  chpdifbndlem1  27056  chpdifbndlem2  27057  chpdifbnd  27058  selberg3lem1  27060  pntrsumo1  27068  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntpbnd  27091  pntibndlem2  27094  pntibndlem3  27095  pntibnd  27096  pntlemd  27097  pntlem3  27112  pntleml  27114  pnt2  27116  pnt  27117  abvcxp  27118  ostth2lem1  27121  padicabv  27133  ostth2lem3  27138  ostth2lem4  27139  ostth2  27140  ostth3  27141  ttgcontlem1  28142  blocnilem  30057  minvecolem4  30133  minvecolem5  30134  pjhthlem1  30644  eigposi  31089  xrge0iifhom  32917  cndprobprob  33437  hgt750lem  33663  unblimceq0lem  35382  unblimceq0  35383  knoppndvlem14  35401  knoppndvlem18  35405  knoppndvlem20  35407  tan2h  36480  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anc  36569  dvasin  36572  areacirclem1  36576  areacirclem4  36579  areacirc  36581  geomcau  36627  blbnd  36655  prdsbnd2  36663  rrnequiv  36703  relogbcld  40838  logblebd  40841  3lexlogpow5ineq2  40920  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  metakunt29  41013  pell14qrrp  41598  pellfundex  41624  pellfundrp  41626  rmspecfund  41647  rmspecpos  41655  areaquad  41965  wwlemuld  42907  radcnvrat  43073  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  supxrgere  44043  supxrgelem  44047  xralrple2  44064  xralrple3  44084  sqrlearg  44266  sinaover2ne0  44584  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnmul  44659  stoweidlem25  44741  stoweidlem28  44744  stoweidlem42  44758  stoweidlem49  44765  wallispilem3  44783  wallispilem4  44784  wallispi  44786  wallispi2lem1  44787  stirlinglem5  44794  stirlinglem10  44799  fourierdlem4  44827  fourierdlem6  44829  fourierdlem7  44830  fourierdlem19  44842  fourierdlem24  44847  fourierdlem26  44849  fourierdlem30  44853  fourierdlem42  44865  fourierdlem51  44873  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem73  44895  fourierdlem75  44897  fourierdlem79  44901  fourierdlem92  44914  fourierdlem109  44931  fouriersw  44947  etransclem35  44985  qndenserrnbllem  45010  ioorrnopnlem  45020  hoiqssbllem1  45338  hoiqssbllem2  45339  iunhoiioolem  45391  pimrecltpos  45424  smfrec  45505  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  m1mod0mod1  46037  rege1logbrege0  47244  fldivexpfllog2  47251  fllog2  47254  resum2sqrp  47394  eenglngeehlnmlem2  47424  itschlc0xyqsol1  47452  inlinecirc02plem  47472  amgmwlem  47849