Theorem elrpd 12698

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-rp 12660

This theorem is referenced by:  mul2lt0rgt0  12762  mul2lt0bi  12765  xov1plusxeqvd  13159  zltaddlt1le  13166  sqn0rp  13774  ltexp2a  13812  expcan  13815  ltexp2  13816  leexp2a  13818  expnlbnd2  13877  discr  13883  sqrlem4  14885  sqrlem7  14888  rpsqrtcl  14904  absrpcl  14928  mulcn2  15233  fprodle  15634  rprisefaccl  15661  rpefcl  15741  eflt  15754  ef01bndlem  15821  stdbdmopn  23580  methaus  23582  nmrpcl  23682  nlmvscnlem1  23756  metnrmlem1a  23927  icopnfcnv  24011  evth  24028  lebnumlem1  24030  nmoleub2lem3  24184  ipcnlem1  24314  minveclem4  24501  pjthlem1  24506  vitalilem4  24680  mbfmulc2lem  24716  itg2gt0  24830  dveflem  25048  dvferm1lem  25053  dvferm2  25056  aaliou3lem3  25409  psercnlem1  25489  pserdvlem1  25491  pserdv  25493  reeff1olem  25510  pilem2  25516  pilem3  25517  tanrpcl  25566  cosordlem  25591  rplogcl  25664  logdivlti  25680  logdivlt  25681  logdivle  25682  recxpcl  25735  rpcxpcl  25736  mulcxp  25745  cxple2  25757  cxpsqrt  25763  cxpcn3  25806  loglesqrt  25816  atanlogaddlem  25968  atantan  25978  atanbnd  25981  rlimcnp  26020  rlimcnp2  26021  efrlim  26024  cxp2limlem  26030  cxp2lim  26031  cxploglim2  26033  jensen  26043  harmonicubnd  26064  fsumharmonic  26066  lgamgulmlem2  26084  ftalem2  26128  basellem3  26137  basellem8  26142  chtrpcl  26229  fsumvma2  26267  chpval2  26271  chpchtsum  26272  chpub  26273  efexple  26334  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ub  26533  rplogsumlem2  26538  dchrisumlema  26541  dchrisumlem3  26544  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0lema  26567  chpdifbndlem1  26606  chpdifbndlem2  26607  chpdifbnd  26608  selberg3lem1  26610  pntrsumo1  26618  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntpbnd  26641  pntibndlem2  26644  pntibndlem3  26645  pntibnd  26646  pntlemd  26647  pntlem3  26662  pntleml  26664  pnt2  26666  pnt  26667  abvcxp  26668  ostth2lem1  26671  padicabv  26683  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  ostth3  26691  ttgcontlem1  27155  blocnilem  29067  minvecolem4  29143  minvecolem5  29144  pjhthlem1  29654  eigposi  30099  xrge0iifhom  31789  cndprobprob  32305  hgt750lem  32531  unblimceq0lem  34613  unblimceq0  34614  knoppndvlem14  34632  knoppndvlem18  34636  knoppndvlem20  34638  tan2h  35696  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  itg2gt0cn  35759  ftc1anclem7  35783  ftc1anc  35785  dvasin  35788  areacirclem1  35792  areacirclem4  35795  areacirc  35797  geomcau  35844  blbnd  35872  prdsbnd2  35880  rrnequiv  35920  relogbcld  39908  logblebd  39911  3lexlogpow5ineq2  39991  3lexlogpow2ineq1  39994  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  metakunt29  40081  pell14qrrp  40598  pellfundex  40624  pellfundrp  40626  rmspecfund  40647  rmspecpos  40654  areaquad  40963  wwlemuld  41655  radcnvrat  41821  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  supxrgere  42762  supxrgelem  42766  xralrple2  42783  xralrple3  42803  sqrlearg  42981  sinaover2ne0  43299  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  stoweidlem25  43456  stoweidlem28  43459  stoweidlem42  43473  stoweidlem49  43480  wallispilem3  43498  wallispilem4  43499  wallispi  43501  wallispi2lem1  43502  stirlinglem5  43509  stirlinglem10  43514  fourierdlem4  43542  fourierdlem6  43544  fourierdlem7  43545  fourierdlem19  43557  fourierdlem24  43562  fourierdlem26  43564  fourierdlem30  43568  fourierdlem42  43580  fourierdlem51  43588  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem73  43610  fourierdlem75  43612  fourierdlem79  43616  fourierdlem92  43629  fourierdlem109  43646  fouriersw  43662  etransclem35  43700  qndenserrnbllem  43725  ioorrnopnlem  43735  hoiqssbllem1  44050  hoiqssbllem2  44051  iunhoiioolem  44103  pimrecltpos  44133  smfrec  44210  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  m1mod0mod1  44709  rege1logbrege0  45792  fldivexpfllog2  45799  fllog2  45802  resum2sqrp  45942  eenglngeehlnmlem2  45972  itschlc0xyqsol1  46000  inlinecirc02plem  46020  amgmwlem  46392