Theorem elrpd 13034

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072  0cc0 11073   < clt 11216  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12994

This theorem is referenced by:  mul2lt0rgt0  13098  mul2lt0bi  13101  xov1plusxeqvd  13502  zltaddlt1le  13509  sqn0rp  14140  ltexp2a  14179  expcan  14182  ltexp2  14183  leexp2a  14185  expnlbnd2  14247  discr  14253  01sqrexlem4  15272  01sqrexlem7  15275  rpsqrtcl  15291  absrpcl  15315  mulcn2  15623  fprodle  16026  rprisefaccl  16053  rpefcl  16136  eflt  16149  ef01bndlem  16216  stdbdmopn  24578  methaus  24580  nmrpcl  24680  nlmvscnlem1  24746  metnrmlem1a  24919  icopnfcnv  25004  evth  25021  lebnumlem1  25023  nmoleub2lem3  25177  ipcnlem1  25307  minveclem4  25494  pjthlem1  25499  vitalilem4  25673  mbfmulc2lem  25709  itg2gt0  25822  dveflem  26041  dvferm1lem  26046  dvferm2  26049  aaliou3lem3  26408  psercnlem1  26488  pserdvlem1  26490  pserdv  26492  reeff1olem  26509  pilem2  26515  pilem3  26516  tanrpcl  26569  cosordlem  26595  rplogcl  26669  logdivlti  26685  logdivlt  26686  logdivle  26687  recxpcl  26740  rpcxpcl  26741  mulcxp  26750  cxple2  26762  cxpsqrt  26768  cxpcn3  26813  loglesqrt  26826  atanlogaddlem  26978  atantan  26988  atanbnd  26991  rlimcnp  27030  rlimcnp2  27031  efrlim  27034  cxp2limlem  27040  cxp2lim  27041  cxploglim2  27043  jensen  27053  harmonicubnd  27074  fsumharmonic  27076  lgamgulmlem2  27094  ftalem2  27138  basellem3  27147  basellem8  27152  chtrpcl  27239  fsumvma2  27278  chpval2  27282  chpchtsum  27283  chpub  27284  efexple  27345  chebbnd1lem2  27534  chebbnd1lem3  27535  chebbnd1  27536  chtppilimlem1  27537  chtppilimlem2  27538  chtppilim  27539  chebbnd2  27541  chto1lb  27542  chpchtlim  27543  chpo1ub  27544  rplogsumlem2  27549  dchrisumlema  27552  dchrisumlem3  27555  dchrvmasumlem2  27562  dchrvmasumiflem1  27565  dchrisum0lema  27578  chpdifbndlem1  27617  chpdifbndlem2  27618  chpdifbnd  27619  selberg3lem1  27621  pntrsumo1  27629  pntpbnd1a  27649  pntpbnd1  27650  pntpbnd2  27651  pntpbnd  27652  pntibndlem2  27655  pntibndlem3  27656  pntibnd  27657  pntlemd  27658  pntlem3  27673  pntleml  27675  pnt2  27677  pnt  27678  abvcxp  27679  ostth2lem1  27682  padicabv  27694  ostth2lem3  27699  ostth2lem4  27700  ostth2  27701  ostth3  27702  ttgcontlem1  29085  blocnilem  31007  minvecolem4  31083  minvecolem5  31084  pjhthlem1  31594  eigposi  32039  2sqr3minply  34077  xrge0iifhom  34234  cndprobprob  34735  hgt750lem  34945  unblimceq0lem  36944  unblimceq0  36945  knoppndvlem14  36963  knoppndvlem18  36967  knoppndvlem20  36969  tan2h  38111  mblfinlem3  38158  mblfinlem4  38159  itg2addnclem  38170  itg2gt0cn  38174  ftc1anclem7  38198  ftc1anc  38200  dvasin  38203  areacirclem1  38207  areacirclem4  38210  areacirc  38212  geomcau  38258  blbnd  38286  prdsbnd2  38294  rrnequiv  38334  relogbcld  42591  logblebd  42594  3lexlogpow5ineq2  42672  3lexlogpow2ineq1  42675  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1p1p3  42686  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p1p6  42690  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  aks6d1c7lem1  42797  explt1d  42932  expeq1d  42933  pell14qrrp  43437  pellfundex  43463  pellfundrp  43465  rmspecfund  43486  rmspecpos  43493  areaquad  43793  wwlemuld  44732  radcnvrat  44890  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  supxrgere  45909  supxrgelem  45913  xralrple2  45930  xralrple3  45949  sqrlearg  46129  sinaover2ne0  46442  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  stoweidlem25  46599  stoweidlem28  46602  stoweidlem42  46616  stoweidlem49  46623  wallispilem3  46641  wallispilem4  46642  wallispi  46644  wallispi2lem1  46645  stirlinglem5  46652  stirlinglem10  46657  fourierdlem4  46685  fourierdlem6  46687  fourierdlem7  46688  fourierdlem19  46700  fourierdlem24  46705  fourierdlem26  46707  fourierdlem30  46711  fourierdlem42  46723  fourierdlem51  46731  fourierdlem63  46743  fourierdlem64  46744  fourierdlem65  46745  fourierdlem73  46753  fourierdlem75  46755  fourierdlem79  46759  fourierdlem92  46772  fourierdlem109  46789  fouriersw  46805  etransclem35  46843  qndenserrnbllem  46868  ioorrnopnlem  46878  hoiqssbllem1  47196  hoiqssbllem2  47197  iunhoiioolem  47249  pimrecltpos  47282  smfrec  47363  smfmullem1  47365  smfmullem2  47366  smfmullem3  47367  m1mod0mod1  47954  rege1logbrege0  49180  fldivexpfllog2  49187  fllog2  49190  resum2sqrp  49330  eenglngeehlnmlem2  49360  itschlc0xyqsol1  49388  inlinecirc02plem  49408  amgmwlem  50423