Theorem elrpd 12958

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  0cc0 11038   < clt 11178  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12918

This theorem is referenced by:  mul2lt0rgt0  13022  mul2lt0bi  13025  xov1plusxeqvd  13426  zltaddlt1le  13433  sqn0rp  14062  ltexp2a  14101  expcan  14104  ltexp2  14105  leexp2a  14107  expnlbnd2  14169  discr  14175  01sqrexlem4  15180  01sqrexlem7  15183  rpsqrtcl  15199  absrpcl  15223  mulcn2  15531  fprodle  15931  rprisefaccl  15958  rpefcl  16041  eflt  16054  ef01bndlem  16121  stdbdmopn  24477  methaus  24479  nmrpcl  24579  nlmvscnlem1  24645  metnrmlem1a  24818  icopnfcnv  24911  evth  24929  lebnumlem1  24931  nmoleub2lem3  25086  ipcnlem1  25216  minveclem4  25403  pjthlem1  25408  vitalilem4  25583  mbfmulc2lem  25619  itg2gt0  25732  dveflem  25954  dvferm1lem  25959  dvferm2  25962  aaliou3lem3  26323  psercnlem1  26406  pserdvlem1  26408  pserdv  26410  reeff1olem  26427  pilem2  26433  pilem3  26434  tanrpcl  26484  cosordlem  26510  rplogcl  26584  logdivlti  26600  logdivlt  26601  logdivle  26602  recxpcl  26655  rpcxpcl  26656  mulcxp  26665  cxple2  26677  cxpsqrt  26683  cxpcn3  26729  loglesqrt  26742  atanlogaddlem  26894  atantan  26904  atanbnd  26907  rlimcnp  26946  rlimcnp2  26947  efrlim  26950  efrlimOLD  26951  cxp2limlem  26957  cxp2lim  26958  cxploglim2  26960  jensen  26970  harmonicubnd  26991  fsumharmonic  26993  lgamgulmlem2  27011  ftalem2  27055  basellem3  27064  basellem8  27069  chtrpcl  27156  fsumvma2  27196  chpval2  27200  chpchtsum  27201  chpub  27202  efexple  27263  chebbnd1lem2  27452  chebbnd1lem3  27453  chebbnd1  27454  chtppilimlem1  27455  chtppilimlem2  27456  chtppilim  27457  chebbnd2  27459  chto1lb  27460  chpchtlim  27461  chpo1ub  27462  rplogsumlem2  27467  dchrisumlema  27470  dchrisumlem3  27473  dchrvmasumlem2  27480  dchrvmasumiflem1  27483  dchrisum0lema  27496  chpdifbndlem1  27535  chpdifbndlem2  27536  chpdifbnd  27537  selberg3lem1  27539  pntrsumo1  27547  pntpbnd1a  27567  pntpbnd1  27568  pntpbnd2  27569  pntpbnd  27570  pntibndlem2  27573  pntibndlem3  27574  pntibnd  27575  pntlemd  27576  pntlem3  27591  pntleml  27593  pnt2  27595  pnt  27596  abvcxp  27597  ostth2lem1  27600  padicabv  27612  ostth2lem3  27617  ostth2lem4  27618  ostth2  27619  ostth3  27620  ttgcontlem1  28973  blocnilem  30896  minvecolem4  30972  minvecolem5  30973  pjhthlem1  31483  eigposi  31928  2sqr3minply  33962  xrge0iifhom  34119  cndprobprob  34620  hgt750lem  34833  unblimceq0lem  36732  unblimceq0  36733  knoppndvlem14  36751  knoppndvlem18  36755  knoppndvlem20  36757  tan2h  37867  mblfinlem3  37914  mblfinlem4  37915  itg2addnclem  37926  itg2gt0cn  37930  ftc1anclem7  37954  ftc1anc  37956  dvasin  37959  areacirclem1  37963  areacirclem4  37966  areacirc  37968  geomcau  38014  blbnd  38042  prdsbnd2  38050  rrnequiv  38090  relogbcld  42347  logblebd  42350  3lexlogpow5ineq2  42429  3lexlogpow2ineq1  42432  3lexlogpow2ineq2  42433  3lexlogpow5ineq5  42434  aks4d1p1p3  42443  aks4d1p1p2  42444  aks4d1p1p4  42445  aks4d1p1p6  42447  aks4d1p1p7  42448  aks4d1p1p5  42449  aks4d1p1  42450  aks6d1c7lem1  42554  explt1d  42697  expeq1d  42698  pell14qrrp  43221  pellfundex  43247  pellfundrp  43249  rmspecfund  43270  rmspecpos  43277  areaquad  43577  wwlemuld  44516  radcnvrat  44674  binomcxplemdvbinom  44713  binomcxplemnotnn0  44716  supxrgere  45696  supxrgelem  45700  xralrple2  45717  xralrple3  45736  sqrlearg  45917  sinaover2ne0  46230  ioodvbdlimc1lem1  46293  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  dvnmul  46305  stoweidlem25  46387  stoweidlem28  46390  stoweidlem42  46404  stoweidlem49  46411  wallispilem3  46429  wallispilem4  46430  wallispi  46432  wallispi2lem1  46433  stirlinglem5  46440  stirlinglem10  46445  fourierdlem4  46473  fourierdlem6  46475  fourierdlem7  46476  fourierdlem19  46488  fourierdlem24  46493  fourierdlem26  46495  fourierdlem30  46499  fourierdlem42  46511  fourierdlem51  46519  fourierdlem63  46531  fourierdlem64  46532  fourierdlem65  46533  fourierdlem73  46541  fourierdlem75  46543  fourierdlem79  46547  fourierdlem92  46560  fourierdlem109  46577  fouriersw  46593  etransclem35  46631  qndenserrnbllem  46656  ioorrnopnlem  46666  hoiqssbllem1  46984  hoiqssbllem2  46985  iunhoiioolem  47037  pimrecltpos  47070  smfrec  47151  smfmullem1  47153  smfmullem2  47154  smfmullem3  47155  m1mod0mod1  47718  rege1logbrege0  48922  fldivexpfllog2  48929  fllog2  48932  resum2sqrp  49072  eenglngeehlnmlem2  49102  itschlc0xyqsol1  49130  inlinecirc02plem  49150  amgmwlem  50165