Theorem elrpd 12968

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043  0cc0 11044   < clt 11184  ℝ⁺crp 12927

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-rp 12928

This theorem is referenced by:  mul2lt0rgt0  13032  mul2lt0bi  13035  xov1plusxeqvd  13435  zltaddlt1le  13442  sqn0rp  14068  ltexp2a  14107  expcan  14110  ltexp2  14111  leexp2a  14113  expnlbnd2  14175  discr  14181  01sqrexlem4  15187  01sqrexlem7  15190  rpsqrtcl  15206  absrpcl  15230  mulcn2  15538  fprodle  15938  rprisefaccl  15965  rpefcl  16048  eflt  16061  ef01bndlem  16128  stdbdmopn  24439  methaus  24441  nmrpcl  24541  nlmvscnlem1  24607  metnrmlem1a  24780  icopnfcnv  24873  evth  24891  lebnumlem1  24893  nmoleub2lem3  25048  ipcnlem1  25178  minveclem4  25365  pjthlem1  25370  vitalilem4  25545  mbfmulc2lem  25581  itg2gt0  25694  dveflem  25916  dvferm1lem  25921  dvferm2  25924  aaliou3lem3  26285  psercnlem1  26368  pserdvlem1  26370  pserdv  26372  reeff1olem  26389  pilem2  26395  pilem3  26396  tanrpcl  26446  cosordlem  26472  rplogcl  26546  logdivlti  26562  logdivlt  26563  logdivle  26564  recxpcl  26617  rpcxpcl  26618  mulcxp  26627  cxple2  26639  cxpsqrt  26645  cxpcn3  26691  loglesqrt  26704  atanlogaddlem  26856  atantan  26866  atanbnd  26869  rlimcnp  26908  rlimcnp2  26909  efrlim  26912  efrlimOLD  26913  cxp2limlem  26919  cxp2lim  26920  cxploglim2  26922  jensen  26932  harmonicubnd  26953  fsumharmonic  26955  lgamgulmlem2  26973  ftalem2  27017  basellem3  27026  basellem8  27031  chtrpcl  27118  fsumvma2  27158  chpval2  27162  chpchtsum  27163  chpub  27164  efexple  27225  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  chtppilimlem1  27417  chtppilimlem2  27418  chtppilim  27419  chebbnd2  27421  chto1lb  27422  chpchtlim  27423  chpo1ub  27424  rplogsumlem2  27429  dchrisumlema  27432  dchrisumlem3  27435  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0lema  27458  chpdifbndlem1  27497  chpdifbndlem2  27498  chpdifbnd  27499  selberg3lem1  27501  pntrsumo1  27509  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntpbnd  27532  pntibndlem2  27535  pntibndlem3  27536  pntibnd  27537  pntlemd  27538  pntlem3  27553  pntleml  27555  pnt2  27557  pnt  27558  abvcxp  27559  ostth2lem1  27562  padicabv  27574  ostth2lem3  27579  ostth2lem4  27580  ostth2  27581  ostth3  27582  ttgcontlem1  28865  blocnilem  30783  minvecolem4  30859  minvecolem5  30860  pjhthlem1  31370  eigposi  31815  2sqr3minply  33763  xrge0iifhom  33920  cndprobprob  34422  hgt750lem  34635  unblimceq0lem  36487  unblimceq0  36488  knoppndvlem14  36506  knoppndvlem18  36510  knoppndvlem20  36512  tan2h  37599  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem  37658  itg2gt0cn  37662  ftc1anclem7  37686  ftc1anc  37688  dvasin  37691  areacirclem1  37695  areacirclem4  37698  areacirc  37700  geomcau  37746  blbnd  37774  prdsbnd2  37782  rrnequiv  37822  relogbcld  41954  logblebd  41957  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks6d1c7lem1  42161  explt1d  42304  expeq1d  42305  pell14qrrp  42841  pellfundex  42867  pellfundrp  42869  rmspecfund  42890  rmspecpos  42898  areaquad  43198  wwlemuld  44138  radcnvrat  44296  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  supxrgere  45322  supxrgelem  45326  xralrple2  45343  xralrple3  45363  sqrlearg  45544  sinaover2ne0  45859  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  stoweidlem25  46016  stoweidlem28  46019  stoweidlem42  46033  stoweidlem49  46040  wallispilem3  46058  wallispilem4  46059  wallispi  46061  wallispi2lem1  46062  stirlinglem5  46069  stirlinglem10  46074  fourierdlem4  46102  fourierdlem6  46104  fourierdlem7  46105  fourierdlem19  46117  fourierdlem24  46122  fourierdlem26  46124  fourierdlem30  46128  fourierdlem42  46140  fourierdlem51  46148  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem73  46170  fourierdlem75  46172  fourierdlem79  46176  fourierdlem92  46189  fourierdlem109  46206  fouriersw  46222  etransclem35  46260  qndenserrnbllem  46285  ioorrnopnlem  46295  hoiqssbllem1  46613  hoiqssbllem2  46614  iunhoiioolem  46666  pimrecltpos  46699  smfrec  46780  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  m1mod0mod1  47348  rege1logbrege0  48540  fldivexpfllog2  48547  fllog2  48550  resum2sqrp  48690  eenglngeehlnmlem2  48720  itschlc0xyqsol1  48748  inlinecirc02plem  48768  amgmwlem  49784