Theorem elrpd 12934

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  0cc0 11009   < clt 11149  ℝ⁺crp 12893

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-rp 12894

This theorem is referenced by:  mul2lt0rgt0  12998  mul2lt0bi  13001  xov1plusxeqvd  13401  zltaddlt1le  13408  sqn0rp  14034  ltexp2a  14073  expcan  14076  ltexp2  14077  leexp2a  14079  expnlbnd2  14141  discr  14147  01sqrexlem4  15152  01sqrexlem7  15155  rpsqrtcl  15171  absrpcl  15195  mulcn2  15503  fprodle  15903  rprisefaccl  15930  rpefcl  16013  eflt  16026  ef01bndlem  16093  stdbdmopn  24404  methaus  24406  nmrpcl  24506  nlmvscnlem1  24572  metnrmlem1a  24745  icopnfcnv  24838  evth  24856  lebnumlem1  24858  nmoleub2lem3  25013  ipcnlem1  25143  minveclem4  25330  pjthlem1  25335  vitalilem4  25510  mbfmulc2lem  25546  itg2gt0  25659  dveflem  25881  dvferm1lem  25886  dvferm2  25889  aaliou3lem3  26250  psercnlem1  26333  pserdvlem1  26335  pserdv  26337  reeff1olem  26354  pilem2  26360  pilem3  26361  tanrpcl  26411  cosordlem  26437  rplogcl  26511  logdivlti  26527  logdivlt  26528  logdivle  26529  recxpcl  26582  rpcxpcl  26583  mulcxp  26592  cxple2  26604  cxpsqrt  26610  cxpcn3  26656  loglesqrt  26669  atanlogaddlem  26821  atantan  26831  atanbnd  26834  rlimcnp  26873  rlimcnp2  26874  efrlim  26877  efrlimOLD  26878  cxp2limlem  26884  cxp2lim  26885  cxploglim2  26887  jensen  26897  harmonicubnd  26918  fsumharmonic  26920  lgamgulmlem2  26938  ftalem2  26982  basellem3  26991  basellem8  26996  chtrpcl  27083  fsumvma2  27123  chpval2  27127  chpchtsum  27128  chpub  27129  efexple  27190  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  chtppilimlem1  27382  chtppilimlem2  27383  chtppilim  27384  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ub  27389  rplogsumlem2  27394  dchrisumlema  27397  dchrisumlem3  27400  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0lema  27423  chpdifbndlem1  27462  chpdifbndlem2  27463  chpdifbnd  27464  selberg3lem1  27466  pntrsumo1  27474  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntpbnd  27497  pntibndlem2  27500  pntibndlem3  27501  pntibnd  27502  pntlemd  27503  pntlem3  27518  pntleml  27520  pnt2  27522  pnt  27523  abvcxp  27524  ostth2lem1  27527  padicabv  27539  ostth2lem3  27544  ostth2lem4  27545  ostth2  27546  ostth3  27547  ttgcontlem1  28830  blocnilem  30748  minvecolem4  30824  minvecolem5  30825  pjhthlem1  31335  eigposi  31780  2sqr3minply  33753  xrge0iifhom  33910  cndprobprob  34412  hgt750lem  34625  unblimceq0lem  36490  unblimceq0  36491  knoppndvlem14  36509  knoppndvlem18  36513  knoppndvlem20  36515  tan2h  37602  mblfinlem3  37649  mblfinlem4  37650  itg2addnclem  37661  itg2gt0cn  37665  ftc1anclem7  37689  ftc1anc  37691  dvasin  37694  areacirclem1  37698  areacirclem4  37701  areacirc  37703  geomcau  37749  blbnd  37777  prdsbnd2  37785  rrnequiv  37825  relogbcld  41956  logblebd  41959  3lexlogpow5ineq2  42038  3lexlogpow2ineq1  42041  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p1  42059  aks6d1c7lem1  42163  explt1d  42306  expeq1d  42307  pell14qrrp  42843  pellfundex  42869  pellfundrp  42871  rmspecfund  42892  rmspecpos  42899  areaquad  43199  wwlemuld  44139  radcnvrat  44297  binomcxplemdvbinom  44336  binomcxplemnotnn0  44339  supxrgere  45323  supxrgelem  45327  xralrple2  45344  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  48553  fldivexpfllog2  48560  fllog2  48563  resum2sqrp  48703  eenglngeehlnmlem2  48733  itschlc0xyqsol1  48761  inlinecirc02plem  48781  amgmwlem  49797