Theorem elrpd 13096

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  0cc0 11184   < clt 11324  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-rp 13058

This theorem is referenced by:  mul2lt0rgt0  13160  mul2lt0bi  13163  xov1plusxeqvd  13558  zltaddlt1le  13565  sqn0rp  14177  ltexp2a  14216  expcan  14219  ltexp2  14220  leexp2a  14222  expnlbnd2  14283  discr  14289  01sqrexlem4  15294  01sqrexlem7  15297  rpsqrtcl  15313  absrpcl  15337  mulcn2  15642  fprodle  16044  rprisefaccl  16071  rpefcl  16152  eflt  16165  ef01bndlem  16232  stdbdmopn  24552  methaus  24554  nmrpcl  24654  nlmvscnlem1  24728  metnrmlem1a  24899  icopnfcnv  24992  evth  25010  lebnumlem1  25012  nmoleub2lem3  25167  ipcnlem1  25298  minveclem4  25485  pjthlem1  25490  vitalilem4  25665  mbfmulc2lem  25701  itg2gt0  25815  dveflem  26037  dvferm1lem  26042  dvferm2  26045  aaliou3lem3  26404  psercnlem1  26487  pserdvlem1  26489  pserdv  26491  reeff1olem  26508  pilem2  26514  pilem3  26515  tanrpcl  26564  cosordlem  26590  rplogcl  26664  logdivlti  26680  logdivlt  26681  logdivle  26682  recxpcl  26735  rpcxpcl  26736  mulcxp  26745  cxple2  26757  cxpsqrt  26763  cxpcn3  26809  loglesqrt  26822  atanlogaddlem  26974  atantan  26984  atanbnd  26987  rlimcnp  27026  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  cxp2limlem  27037  cxp2lim  27038  cxploglim2  27040  jensen  27050  harmonicubnd  27071  fsumharmonic  27073  lgamgulmlem2  27091  ftalem2  27135  basellem3  27144  basellem8  27149  chtrpcl  27236  fsumvma2  27276  chpval2  27280  chpchtsum  27281  chpub  27282  efexple  27343  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  chtppilimlem2  27536  chtppilim  27537  chebbnd2  27539  chto1lb  27540  chpchtlim  27541  chpo1ub  27542  rplogsumlem2  27547  dchrisumlema  27550  dchrisumlem3  27553  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0lema  27576  chpdifbndlem1  27615  chpdifbndlem2  27616  chpdifbnd  27617  selberg3lem1  27619  pntrsumo1  27627  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntpbnd  27650  pntibndlem2  27653  pntibndlem3  27654  pntibnd  27655  pntlemd  27656  pntlem3  27671  pntleml  27673  pnt2  27675  pnt  27676  abvcxp  27677  ostth2lem1  27680  padicabv  27692  ostth2lem3  27697  ostth2lem4  27698  ostth2  27699  ostth3  27700  ttgcontlem1  28917  blocnilem  30836  minvecolem4  30912  minvecolem5  30913  pjhthlem1  31423  eigposi  31868  2sqr3minply  33738  xrge0iifhom  33883  cndprobprob  34403  hgt750lem  34628  unblimceq0lem  36472  unblimceq0  36473  knoppndvlem14  36491  knoppndvlem18  36495  knoppndvlem20  36497  tan2h  37572  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anc  37661  dvasin  37664  areacirclem1  37668  areacirclem4  37671  areacirc  37673  geomcau  37719  blbnd  37747  prdsbnd2  37755  rrnequiv  37795  relogbcld  41929  logblebd  41932  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks6d1c7lem1  42137  metakunt29  42190  explt1d  42310  expeq1d  42311  pell14qrrp  42816  pellfundex  42842  pellfundrp  42844  rmspecfund  42865  rmspecpos  42873  areaquad  43177  wwlemuld  44118  radcnvrat  44283  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  supxrgere  45248  supxrgelem  45252  xralrple2  45269  xralrple3  45289  sqrlearg  45471  sinaover2ne0  45789  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  stoweidlem25  45946  stoweidlem28  45949  stoweidlem42  45963  stoweidlem49  45970  wallispilem3  45988  wallispilem4  45989  wallispi  45991  wallispi2lem1  45992  stirlinglem5  45999  stirlinglem10  46004  fourierdlem4  46032  fourierdlem6  46034  fourierdlem7  46035  fourierdlem19  46047  fourierdlem24  46052  fourierdlem26  46054  fourierdlem30  46058  fourierdlem42  46070  fourierdlem51  46078  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem73  46100  fourierdlem75  46102  fourierdlem79  46106  fourierdlem92  46119  fourierdlem109  46136  fouriersw  46152  etransclem35  46190  qndenserrnbllem  46215  ioorrnopnlem  46225  hoiqssbllem1  46543  hoiqssbllem2  46544  iunhoiioolem  46596  pimrecltpos  46629  smfrec  46710  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  m1mod0mod1  47243  rege1logbrege0  48292  fldivexpfllog2  48299  fllog2  48302  resum2sqrp  48442  eenglngeehlnmlem2  48472  itschlc0xyqsol1  48500  inlinecirc02plem  48520  amgmwlem  48896