Theorem elrpd 13071

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151  0cc0 11152   < clt 11292  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-rp 13032

This theorem is referenced by:  mul2lt0rgt0  13135  mul2lt0bi  13138  xov1plusxeqvd  13534  zltaddlt1le  13541  sqn0rp  14163  ltexp2a  14202  expcan  14205  ltexp2  14206  leexp2a  14208  expnlbnd2  14269  discr  14275  01sqrexlem4  15280  01sqrexlem7  15283  rpsqrtcl  15299  absrpcl  15323  mulcn2  15628  fprodle  16028  rprisefaccl  16055  rpefcl  16136  eflt  16149  ef01bndlem  16216  stdbdmopn  24546  methaus  24548  nmrpcl  24648  nlmvscnlem1  24722  metnrmlem1a  24893  icopnfcnv  24986  evth  25004  lebnumlem1  25006  nmoleub2lem3  25161  ipcnlem1  25292  minveclem4  25479  pjthlem1  25484  vitalilem4  25659  mbfmulc2lem  25695  itg2gt0  25809  dveflem  26031  dvferm1lem  26036  dvferm2  26039  aaliou3lem3  26400  psercnlem1  26483  pserdvlem1  26485  pserdv  26487  reeff1olem  26504  pilem2  26510  pilem3  26511  tanrpcl  26560  cosordlem  26586  rplogcl  26660  logdivlti  26676  logdivlt  26677  logdivle  26678  recxpcl  26731  rpcxpcl  26732  mulcxp  26741  cxple2  26753  cxpsqrt  26759  cxpcn3  26805  loglesqrt  26818  atanlogaddlem  26970  atantan  26980  atanbnd  26983  rlimcnp  27022  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  cxp2limlem  27033  cxp2lim  27034  cxploglim2  27036  jensen  27046  harmonicubnd  27067  fsumharmonic  27069  lgamgulmlem2  27087  ftalem2  27131  basellem3  27140  basellem8  27145  chtrpcl  27232  fsumvma2  27272  chpval2  27276  chpchtsum  27277  chpub  27278  efexple  27339  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  rplogsumlem2  27543  dchrisumlema  27546  dchrisumlem3  27549  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0lema  27572  chpdifbndlem1  27611  chpdifbndlem2  27612  chpdifbnd  27613  selberg3lem1  27615  pntrsumo1  27623  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntpbnd  27646  pntibndlem2  27649  pntibndlem3  27650  pntibnd  27651  pntlemd  27652  pntlem3  27667  pntleml  27669  pnt2  27671  pnt  27672  abvcxp  27673  ostth2lem1  27676  padicabv  27688  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  ostth3  27696  ttgcontlem1  28913  blocnilem  30832  minvecolem4  30908  minvecolem5  30909  pjhthlem1  31419  eigposi  31864  2sqr3minply  33752  xrge0iifhom  33897  cndprobprob  34419  hgt750lem  34644  unblimceq0lem  36488  unblimceq0  36489  knoppndvlem14  36507  knoppndvlem18  36511  knoppndvlem20  36513  tan2h  37598  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2gt0cn  37661  ftc1anclem7  37685  ftc1anc  37687  dvasin  37690  areacirclem1  37694  areacirclem4  37697  areacirc  37699  geomcau  37745  blbnd  37773  prdsbnd2  37781  rrnequiv  37821  relogbcld  41954  logblebd  41957  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks6d1c7lem1  42161  metakunt29  42214  explt1d  42336  expeq1d  42337  pell14qrrp  42847  pellfundex  42873  pellfundrp  42875  rmspecfund  42896  rmspecpos  42904  areaquad  43204  wwlemuld  44145  radcnvrat  44309  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  supxrgere  45282  supxrgelem  45286  xralrple2  45303  xralrple3  45323  sqrlearg  45505  sinaover2ne0  45823  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  stoweidlem25  45980  stoweidlem28  45983  stoweidlem42  45997  stoweidlem49  46004  wallispilem3  46022  wallispilem4  46023  wallispi  46025  wallispi2lem1  46026  stirlinglem5  46033  stirlinglem10  46038  fourierdlem4  46066  fourierdlem6  46068  fourierdlem7  46069  fourierdlem19  46081  fourierdlem24  46086  fourierdlem26  46088  fourierdlem30  46092  fourierdlem42  46104  fourierdlem51  46112  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem73  46134  fourierdlem75  46136  fourierdlem79  46140  fourierdlem92  46153  fourierdlem109  46170  fouriersw  46186  etransclem35  46224  qndenserrnbllem  46249  ioorrnopnlem  46259  hoiqssbllem1  46577  hoiqssbllem2  46578  iunhoiioolem  46630  pimrecltpos  46663  smfrec  46744  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  m1mod0mod1  47293  rege1logbrege0  48407  fldivexpfllog2  48414  fllog2  48417  resum2sqrp  48557  eenglngeehlnmlem2  48587  itschlc0xyqsol1  48615  inlinecirc02plem  48635  amgmwlem  49032