Theorem elrpd 12931

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005  0cc0 11006   < clt 11146  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-rp 12891

This theorem is referenced by:  mul2lt0rgt0  12995  mul2lt0bi  12998  xov1plusxeqvd  13398  zltaddlt1le  13405  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  24433  methaus  24435  nmrpcl  24535  nlmvscnlem1  24601  metnrmlem1a  24774  icopnfcnv  24867  evth  24885  lebnumlem1  24887  nmoleub2lem3  25042  ipcnlem1  25172  minveclem4  25359  pjthlem1  25364  vitalilem4  25539  mbfmulc2lem  25575  itg2gt0  25688  dveflem  25910  dvferm1lem  25915  dvferm2  25918  aaliou3lem3  26279  psercnlem1  26362  pserdvlem1  26364  pserdv  26366  reeff1olem  26383  pilem2  26389  pilem3  26390  tanrpcl  26440  cosordlem  26466  rplogcl  26540  logdivlti  26556  logdivlt  26557  logdivle  26558  recxpcl  26611  rpcxpcl  26612  mulcxp  26621  cxple2  26633  cxpsqrt  26639  cxpcn3  26685  loglesqrt  26698  atanlogaddlem  26850  atantan  26860  atanbnd  26863  rlimcnp  26902  rlimcnp2  26903  efrlim  26906  efrlimOLD  26907  cxp2limlem  26913  cxp2lim  26914  cxploglim2  26916  jensen  26926  harmonicubnd  26947  fsumharmonic  26949  lgamgulmlem2  26967  ftalem2  27011  basellem3  27020  basellem8  27025  chtrpcl  27112  fsumvma2  27152  chpval2  27156  chpchtsum  27157  chpub  27158  efexple  27219  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ub  27418  rplogsumlem2  27423  dchrisumlema  27426  dchrisumlem3  27429  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0lema  27452  chpdifbndlem1  27491  chpdifbndlem2  27492  chpdifbnd  27493  selberg3lem1  27495  pntrsumo1  27503  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntpbnd  27526  pntibndlem2  27529  pntibndlem3  27530  pntibnd  27531  pntlemd  27532  pntlem3  27547  pntleml  27549  pnt2  27551  pnt  27552  abvcxp  27553  ostth2lem1  27556  padicabv  27568  ostth2lem3  27573  ostth2lem4  27574  ostth2  27575  ostth3  27576  ttgcontlem1  28863  blocnilem  30784  minvecolem4  30860  minvecolem5  30861  pjhthlem1  31371  eigposi  31816  2sqr3minply  33793  xrge0iifhom  33950  cndprobprob  34451  hgt750lem  34664  unblimceq0lem  36550  unblimceq0  36551  knoppndvlem14  36569  knoppndvlem18  36573  knoppndvlem20  36575  tan2h  37662  mblfinlem3  37709  mblfinlem4  37710  itg2addnclem  37721  itg2gt0cn  37725  ftc1anclem7  37749  ftc1anc  37751  dvasin  37754  areacirclem1  37758  areacirclem4  37761  areacirc  37763  geomcau  37809  blbnd  37837  prdsbnd2  37845  rrnequiv  37885  relogbcld  42076  logblebd  42079  3lexlogpow5ineq2  42158  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1p1p3  42172  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p1  42179  aks6d1c7lem1  42283  explt1d  42426  expeq1d  42427  pell14qrrp  42963  pellfundex  42989  pellfundrp  42991  rmspecfund  43012  rmspecpos  43019  areaquad  43319  wwlemuld  44259  radcnvrat  44417  binomcxplemdvbinom  44456  binomcxplemnotnn0  44459  supxrgere  45442  supxrgelem  45446  xralrple2  45463  xralrple3  45482  sqrlearg  45663  sinaover2ne0  45976  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnmul  46051  stoweidlem25  46133  stoweidlem28  46136  stoweidlem42  46150  stoweidlem49  46157  wallispilem3  46175  wallispilem4  46176  wallispi  46178  wallispi2lem1  46179  stirlinglem5  46186  stirlinglem10  46191  fourierdlem4  46219  fourierdlem6  46221  fourierdlem7  46222  fourierdlem19  46234  fourierdlem24  46239  fourierdlem26  46241  fourierdlem30  46245  fourierdlem42  46257  fourierdlem51  46265  fourierdlem63  46277  fourierdlem64  46278  fourierdlem65  46279  fourierdlem73  46287  fourierdlem75  46289  fourierdlem79  46293  fourierdlem92  46306  fourierdlem109  46323  fouriersw  46339  etransclem35  46377  qndenserrnbllem  46402  ioorrnopnlem  46412  hoiqssbllem1  46730  hoiqssbllem2  46731  iunhoiioolem  46783  pimrecltpos  46816  smfrec  46897  smfmullem1  46899  smfmullem2  46900  smfmullem3  46901  m1mod0mod1  47464  rege1logbrege0  48669  fldivexpfllog2  48676  fllog2  48679  resum2sqrp  48819  eenglngeehlnmlem2  48849  itschlc0xyqsol1  48877  inlinecirc02plem  48897  amgmwlem  49913