Theorem elrpd 13161

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11199  0cc0 11200   < clt 11343  ℝ⁺crp 13120

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-rp 13121

This theorem is used by:  mul2lt0rgt0  13225  mul2lt0bi  13228  xov1plusxeqvd  13629  zltaddlt1le  13636  sqn0rp  14270  ltexp2a  14309  expcan  14312  ltexp2  14313  leexp2a  14315  expnlbnd2  14378  discr  14384  01sqrexlem4  15412  01sqrexlem7  15415  rpsqrtcl  15431  absrpcl  15455  mulcn2  15763  fprodle  16163  rprisefaccl  16190  rpefcl  16272  eflt  16285  ef01bndlem  16352  stdbdmopn  24837  methaus  24839  nmrpcl  24939  nlmvscnlem1  25005  metnrmlem1a  25178  icopnfcnv  25263  evth  25280  lebnumlem1  25282  nmoleub2lem3  25436  ipcnlem1  25566  minveclem4  25753  pjthlem1  25758  vitalilem4  25932  mbfmulc2lem  25968  itg2gt0  26081  dveflem  26299  dvferm1lem  26304  dvferm2  26307  aaliou3lem3  26671  psercnlem1  26752  pserdvlem1  26754  pserdv  26756  reeff1olem  26773  pilem2  26779  pilem3  26780  tanrpcl  26833  cosordlem  26858  rplogcl  26932  logdivlti  26948  logdivlt  26949  logdivle  26950  recxpcl  27003  rpcxpcl  27004  mulcxp  27013  cxple2  27025  cxpsqrt  27031  cxpcn3  27076  loglesqrt  27089  atanlogaddlem  27241  atantan  27251  atanbnd  27254  rlimcnp  27293  rlimcnp2  27294  efrlim  27297  cxp2limlem  27303  cxp2lim  27304  cxploglim2  27306  jensen  27316  harmonicubnd  27337  fsumharmonic  27339  lgamgulmlem2  27357  ftalem2  27401  basellem3  27410  basellem8  27415  chtrpcl  27502  fsumvma2  27541  chpval2  27545  chpchtsum  27546  chpub  27547  efexple  27608  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  chtppilimlem1  27800  chtppilimlem2  27801  chtppilim  27802  chebbnd2  27804  chto1lb  27805  chpchtlim  27806  chpo1ub  27807  rplogsumlem2  27812  dchrisumlema  27815  dchrisumlem3  27818  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0lema  27841  chpdifbndlem1  27880  chpdifbndlem2  27881  chpdifbnd  27882  selberg3lem1  27884  pntrsumo1  27892  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntpbnd  27915  pntibndlem2  27918  pntibndlem3  27919  pntibnd  27920  pntlemd  27921  pntlem3  27936  pntleml  27938  pnt2  27940  pnt  27941  abvcxp  27942  ostth2lem1  27945  padicabv  27957  ostth2lem3  27962  ostth2lem4  27963  ostth2  27964  ostth3  27965  ttgcontlem1  29462  blocnilem  31406  minvecolem4  31482  minvecolem5  31483  pjhthlem1  31993  eigposi  32438  2sqr3minply  34412  xrge0iifhom  34569  cndprobprob  35070  hgt750lem  35280  unblimceq0lem  37372  unblimceq0  37373  knoppndvlem14  37391  knoppndvlem18  37395  knoppndvlem20  37397  tan2h  38535  mblfinlem3  38577  mblfinlem4  38578  itg2addnclem  38589  itg2gt0cn  38593  ftc1anclem7  38617  ftc1anc  38619  dvasin  38622  areacirclem1  38626  areacirclem4  38629  areacirc  38631  geomcau  38693  blbnd  38721  prdsbnd2  38729  rrnequiv  38769  relogbcld  43024  logblebd  43027  3lexlogpow5ineq2  43105  3lexlogpow2ineq1  43108  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1p1p3  43119  aks4d1p1p2  43120  aks4d1p1p4  43121  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1p5  43125  aks4d1p1  43126  aks6d1c7lem1  43230  explt1d  43380  expeq1d  43381  pell14qrrp  43866  pellfundex  43892  pellfundrp  43894  rmspecfund  43915  rmspecpos  43922  areaquad  44217  wwlemuld  45155  radcnvrat  45297  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  supxrgere  46344  supxrgelem  46348  xralrple2  46365  xralrple3  46384  sqrlearg  46564  sinaover2ne0  46877  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnmul  46952  stoweidlem25  47034  stoweidlem28  47037  stoweidlem42  47051  stoweidlem49  47058  wallispilem3  47076  wallispilem4  47077  wallispi  47079  wallispi2lem1  47080  stirlinglem5  47087  stirlinglem10  47092  fourierdlem4  47120  fourierdlem6  47122  fourierdlem7  47123  fourierdlem19  47135  fourierdlem24  47140  fourierdlem26  47142  fourierdlem30  47146  fourierdlem42  47158  fourierdlem51  47166  fourierdlem63  47178  fourierdlem64  47179  fourierdlem65  47180  fourierdlem73  47188  fourierdlem75  47190  fourierdlem79  47194  fourierdlem92  47207  fourierdlem109  47224  fouriersw  47240  etransclem35  47278  qndenserrnbllem  47303  ioorrnopnlem  47313  hoiqssbllem1  47631  hoiqssbllem2  47632  iunhoiioolem  47684  pimrecltpos  47717  smfrec  47798  smfmullem1  47800  smfmullem2  47801  smfmullem3  47802  m1mod0mod1  48429  rege1logbrege0  49669  fldivexpfllog2  49676  fllog2  49679  resum2sqrp  49819  eenglngeehlnmlem2  49849  itschlc0xyqsol1  49877  inlinecirc02plem  49897  amgmwlem  50986